Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem76 Structured version   Visualization version   GIF version

Theorem fourierdlem76 41191
Description: Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem76.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem76.xre (𝜑𝑋 ∈ ℝ)
fourierdlem76.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem76.m (𝜑𝑀 ∈ ℕ)
fourierdlem76.v (𝜑𝑉 ∈ (𝑃𝑀))
fourierdlem76.fcn ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
fourierdlem76.r ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
fourierdlem76.l ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
fourierdlem76.a (𝜑𝐴 ∈ ℝ)
fourierdlem76.b (𝜑𝐵 ∈ ℝ)
fourierdlem76.altb (𝜑𝐴 < 𝐵)
fourierdlem76.ab (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem76.n0 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
fourierdlem76.c (𝜑𝐶 ∈ ℝ)
fourierdlem76.o 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
fourierdlem76.q 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
fourierdlem76.t 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
fourierdlem76.n 𝑁 = ((♯‘𝑇) − 1)
fourierdlem76.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
fourierdlem76.d 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
fourierdlem76.e 𝐸 = (((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) · ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2)))))
fourierdlem76.ch (𝜒 ↔ (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
Assertion
Ref Expression
fourierdlem76 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗))) ∧ (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))
Distinct variable groups:   𝐴,𝑠   𝐵,𝑠   𝐶,𝑠   𝐹,𝑠   𝐿,𝑠   𝑖,𝑀,𝑗   𝑚,𝑀,𝑝,𝑖   𝑓,𝑁   𝑄,𝑠   𝑅,𝑠   𝑆,𝑓   𝑆,𝑠   𝑇,𝑓   𝑖,𝑉,𝑗,𝑠   𝑉,𝑝   𝑖,𝑋,𝑗,𝑠   𝑚,𝑋,𝑝   𝜒,𝑠   𝜑,𝑓   𝜑,𝑖,𝑗,𝑠
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝜒(𝑓,𝑖,𝑗,𝑚,𝑝)   𝐴(𝑓,𝑖,𝑗,𝑚,𝑝)   𝐵(𝑓,𝑖,𝑗,𝑚,𝑝)   𝐶(𝑓,𝑖,𝑗,𝑚,𝑝)   𝐷(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝)   𝑃(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝)   𝑄(𝑓,𝑖,𝑗,𝑚,𝑝)   𝑅(𝑓,𝑖,𝑗,𝑚,𝑝)   𝑆(𝑖,𝑗,𝑚,𝑝)   𝑇(𝑖,𝑗,𝑚,𝑠,𝑝)   𝐸(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝)   𝐹(𝑓,𝑖,𝑗,𝑚,𝑝)   𝐿(𝑓,𝑖,𝑗,𝑚,𝑝)   𝑀(𝑓,𝑠)   𝑁(𝑖,𝑗,𝑚,𝑠,𝑝)   𝑂(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝)   𝑉(𝑓,𝑚)   𝑋(𝑓)

Proof of Theorem fourierdlem76
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem76.ch . . 3 (𝜒 ↔ (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
2 eqid 2825 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3 eqid 2825 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4 eqid 2825 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5 simplll 791 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
61, 5sylbi 209 . . . . . . . . . 10 (𝜒𝜑)
76adantr 474 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8 ioossicc 12554 . . . . . . . . . 10 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9 fourierdlem76.a . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ)
109rexrd 10413 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ*)
116, 10syl 17 . . . . . . . . . . . 12 (𝜒𝐴 ∈ ℝ*)
1211adantr 474 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ*)
13 fourierdlem76.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℝ)
1413rexrd 10413 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ*)
156, 14syl 17 . . . . . . . . . . . 12 (𝜒𝐵 ∈ ℝ*)
1615adantr 474 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ*)
17 elioore 12500 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
1817adantl 475 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
196, 9syl 17 . . . . . . . . . . . . 13 (𝜒𝐴 ∈ ℝ)
2019adantr 474 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22 prfi 8510 . . . . . . . . . . . . . . . . . . . . 21 {𝐴, 𝐵} ∈ Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ∈ Fin)
24 fzfid 13074 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0...𝑀) ∈ Fin)
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2625rnmptfi 40159 . . . . . . . . . . . . . . . . . . . . 21 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27 infi 8459 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29 unfi 8502 . . . . . . . . . . . . . . . . . . . 20 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3023, 28, 29syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3121, 30syl5eqel 2910 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ Fin)
32 prssg 4570 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
339, 13, 32syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
349, 13, 33mpbi2and 703 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35 inss2 4060 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36 ioossre 12530 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴(,)𝐵) ⊆ ℝ
3735, 36sstri 3836 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
3934, 38unssd 4018 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
4021, 39syl5eqss 3874 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ ℝ)
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18 𝑁 = ((♯‘𝑇) − 1)
4331, 40, 41, 42fourierdlem36 41152 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
446, 43syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑆 Isom < , < ((0...𝑁), 𝑇))
45 isof1o 6833 . . . . . . . . . . . . . . . 16 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
46 f1of 6382 . . . . . . . . . . . . . . . 16 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15 (𝜒𝑆:(0...𝑁)⟶𝑇)
486, 40syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑇 ⊆ ℝ)
4947, 48fssd 6296 . . . . . . . . . . . . . 14 (𝜒𝑆:(0...𝑁)⟶ℝ)
5049adantr 474 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51 simpllr 793 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
521, 51sylbi 209 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (0..^𝑁))
53 elfzofz 12787 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
5452, 53syl 17 . . . . . . . . . . . . . 14 (𝜒𝑗 ∈ (0...𝑁))
5554adantr 474 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
5650, 55ffvelrnd 6614 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ)
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑆:(0...𝑁)⟶𝑇)
58 frn 6288 . . . . . . . . . . . . . . . . . 18 (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆𝑇)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑆𝑇)
609leidd 10925 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐴)
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴 < 𝐵)
629, 13, 61ltled 10511 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐵)
639, 13, 9, 60, 62eliccd 40523 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐴[,]𝐵))
6413leidd 10925 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝐵)
659, 13, 13, 62, 64eliccd 40523 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (𝐴[,]𝐵))
66 prssg 4570 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
679, 13, 66syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
6863, 65, 67mpbi2and 703 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
6935, 8sstri 3836 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
7069a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
7168, 70unssd 4018 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
7221, 71syl5eqss 3874 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ⊆ (𝐴[,]𝐵))
7359, 72sstrd 3837 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
746, 73syl 17 . . . . . . . . . . . . . . 15 (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75 ffun 6285 . . . . . . . . . . . . . . . . 17 (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
7649, 75syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → Fun 𝑆)
77 fdm 6290 . . . . . . . . . . . . . . . . . . 19 (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom 𝑆 = (0...𝑁))
7978eqcomd 2831 . . . . . . . . . . . . . . . . 17 (𝜒 → (0...𝑁) = dom 𝑆)
8054, 79eleqtrd 2908 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ dom 𝑆)
81 fvelrn 6606 . . . . . . . . . . . . . . . 16 ((Fun 𝑆𝑗 ∈ dom 𝑆) → (𝑆𝑗) ∈ ran 𝑆)
8276, 80, 81syl2anc 579 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆𝑗) ∈ ran 𝑆)
8374, 82sseldd 3828 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ (𝐴[,]𝐵))
84 iccgelb 12525 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆𝑗))
8511, 15, 83, 84syl3anc 1494 . . . . . . . . . . . . 13 (𝜒𝐴 ≤ (𝑆𝑗))
8685adantr 474 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆𝑗))
8756rexrd 10413 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ*)
88 fzofzp1 12867 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
8952, 88syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
9049, 89ffvelrnd 6614 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
9190rexrd 10413 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
9291adantr 474 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
93 simpr 479 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
94 ioogtlb 40514 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9587, 92, 93, 94syl3anc 1494 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9620, 56, 18, 86, 95lelttrd 10521 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
9790adantr 474 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
986, 13syl 17 . . . . . . . . . . . . 13 (𝜒𝐵 ∈ ℝ)
9998adantr 474 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100 iooltub 40530 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10187, 92, 93, 100syl3anc 1494 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10289, 79eleqtrd 2908 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103 fvelrn 6606 . . . . . . . . . . . . . . . 16 ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10476, 102, 103syl2anc 579 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10574, 104sseldd 3828 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106 iccleub 12524 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10711, 15, 105, 106syl3anc 1494 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108107adantr 474 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10918, 97, 99, 101, 108ltletrd 10523 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
11012, 16, 18, 96, 109eliood 40517 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
1118, 110sseldi 3825 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112 fourierdlem76.f . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶ℝ)
113112adantr 474 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114 fourierdlem76.xre . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
115114adantr 474 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
1169, 13iccssred 40524 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117116sselda 3827 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118115, 117readdcld 10393 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119113, 118ffvelrnd 6614 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
1207, 111, 119syl2anc 579 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121120recnd 10392 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122 fourierdlem76.c . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
123122recnd 10392 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1246, 123syl 17 . . . . . . . 8 (𝜒𝐶 ∈ ℂ)
125124adantr 474 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126121, 125subcld 10720 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127 ioossre 12530 . . . . . . . . 9 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128127a1i 11 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129128sselda 3827 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130129recnd 10392 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131 nne 3003 . . . . . . . . . . . 12 𝑠 ≠ 0 ↔ 𝑠 = 0)
132131biimpi 208 . . . . . . . . . . 11 𝑠 ≠ 0 → 𝑠 = 0)
133132eqcomd 2831 . . . . . . . . . 10 𝑠 ≠ 0 → 0 = 𝑠)
134133adantl 475 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135 simpr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136135adantr 474 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137134, 136eqeltrd 2906 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138 fourierdlem76.n0 . . . . . . . . 9 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139138ad2antrr 717 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140137, 139condan 852 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
1417, 111, 140syl2anc 579 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142126, 130, 141divcld 11134 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143 2cnd 11436 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144130halfcld 11610 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145144sincld 15239 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146143, 145mulcld 10384 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
14717recnd 10392 . . . . . . . . . 10 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148147adantl 475 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149148halfcld 11610 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150149sincld 15239 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151 2ne0 11469 . . . . . . . 8 2 ≠ 0
152151a1i 11 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153 fourierdlem76.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
1546, 153syl 17 . . . . . . . . . 10 (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155154adantr 474 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156155, 111sseldd 3828 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157 fourierdlem44 41160 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158156, 141, 157syl2anc 579 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159143, 150, 152, 158mulne0d 11011 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160130, 146, 159divcld 11134 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161 eqid 2825 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162 eqid 2825 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163141neneqd 3004 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164 velsn 4415 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
165163, 164sylnibr 321 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166130, 165eldifd 3809 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167 eqid 2825 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168 eqid 2825 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169 elfzofz 12787 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171 pire 24617 . . . . . . . . . . . . . . . . . . . . 21 π ∈ ℝ
172171renegcli 10670 . . . . . . . . . . . . . . . . . . . 20 -π ∈ ℝ
173172a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -π ∈ ℝ)
174173, 114readdcld 10393 . . . . . . . . . . . . . . . . . 18 (𝜑 → (-π + 𝑋) ∈ ℝ)
175171a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → π ∈ ℝ)
176175, 114readdcld 10393 . . . . . . . . . . . . . . . . . 18 (𝜑 → (π + 𝑋) ∈ ℝ)
177174, 176iccssred 40524 . . . . . . . . . . . . . . . . 17 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178177adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℕ)
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19 (𝜑𝑉 ∈ (𝑃𝑀))
182179, 180, 181fourierdlem15 41131 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183182adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184183, 170ffvelrnd 6614 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185178, 184sseldd 3828 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
186114adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187185, 186resubcld 10789 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
18825fvmpt2 6543 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
189170, 187, 188syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
190189, 187eqeltrd 2906 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
191190adantlr 706 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
192191adantr 474 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
1931, 192sylbi 209 . . . . . . . . 9 (𝜒 → (𝑄𝑖) ∈ ℝ)
194 fveq2 6437 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
195194oveq1d 6925 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
196195cbvmptv 4975 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
19725, 196eqtri 2849 . . . . . . . . . . . . . . 15 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
198197a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
199 fveq2 6437 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
200199oveq1d 6925 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201200adantl 475 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202 fzofzp1 12867 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203202adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204183, 203ffvelrnd 6614 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205178, 204sseldd 3828 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206205, 186resubcld 10789 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207198, 201, 203, 206fvmptd 6539 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208207, 206eqeltrd 2906 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208adantlr 706 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210209adantr 474 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2111, 210sylbi 209 . . . . . . . . 9 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212179fourierdlem2 41118 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
213180, 212syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
214181, 213mpbid 224 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
215214simprrd 790 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
216215r19.21bi 3141 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
217185, 205, 186, 216ltsub1dd 10971 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218217, 189, 2073brtr4d 4907 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
219218adantlr 706 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
220219adantr 474 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2211, 220sylbi 209 . . . . . . . . 9 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2221biimpi 208 . . . . . . . . . . . . . . . . . 18 (𝜒 → (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
223222simplrd 786 . . . . . . . . . . . . . . . . 17 (𝜒𝑖 ∈ (0..^𝑀))
2246, 223, 185syl2anc 579 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) ∈ ℝ)
225224rexrd 10413 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ∈ ℝ*)
226225adantr 474 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2276, 223, 205syl2anc 579 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228227rexrd 10413 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
229228adantr 474 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
2306, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑋 ∈ ℝ)
231230adantr 474 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232 elioore 12500 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233232adantl 475 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234231, 233readdcld 10393 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
2356, 223, 189syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
236235oveq2d 6926 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
237230recnd 10392 . . . . . . . . . . . . . . . . . 18 (𝜒𝑋 ∈ ℂ)
238224recnd 10392 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉𝑖) ∈ ℂ)
239237, 238pncan3d 10723 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
240236, 239eqtr2d 2862 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
241240adantr 474 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
242193adantr 474 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
243193rexrd 10413 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) ∈ ℝ*)
244243adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
245211rexrd 10413 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246245adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
247 simpr 479 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
248 ioogtlb 40514 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
249244, 246, 247, 248syl3anc 1494 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
250242, 233, 231, 249ltadd2dd 10522 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
251241, 250eqbrtrd 4897 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
252211adantr 474 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253 iooltub 40530 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254244, 246, 247, 253syl3anc 1494 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255233, 252, 231, 254ltadd2dd 10522 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
2566, 223, 207syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257256oveq2d 6926 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258227recnd 10392 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259237, 258pncan3d 10723 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260257, 259eqtrd 2861 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261260adantr 474 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262255, 261breqtrd 4901 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263226, 229, 234, 251, 262eliood 40517 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
264 fvres 6456 . . . . . . . . . . . . 13 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265263, 264syl 17 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266265eqcomd 2831 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267266mpteq2dva 4969 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268 ioosscn 40513 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269268a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270 fourierdlem76.fcn . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
2716, 223, 270syl2anc 579 . . . . . . . . . . 11 (𝜒 → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272 ioosscn 40513 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273272a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274269, 271, 273, 237, 263fourierdlem23 41139 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275267, 274eqeltrd 2906 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2766, 112syl 17 . . . . . . . . . 10 (𝜒𝐹:ℝ⟶ℝ)
277 ioossre 12530 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278277a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279 eqid 2825 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280 ioossre 12530 . . . . . . . . . . 11 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281280a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282233, 254ltned 10499 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283 fourierdlem76.l . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
2846, 223, 283syl2anc 579 . . . . . . . . . . 11 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
285260eqcomd 2831 . . . . . . . . . . . 12 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286285oveq2d 6926 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
287284, 286eleqtrd 2908 . . . . . . . . . 10 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
288211recnd 10392 . . . . . . . . . 10 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 41168 . . . . . . . . 9 (𝜒𝐿 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
29049, 54ffvelrnd 6614 . . . . . . . . 9 (𝜒 → (𝑆𝑗) ∈ ℝ)
291 elfzoelz 12772 . . . . . . . . . . . 12 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292 zre 11715 . . . . . . . . . . . 12 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
29352, 291, 2923syl 18 . . . . . . . . . . 11 (𝜒𝑗 ∈ ℝ)
294293ltp1d 11291 . . . . . . . . . 10 (𝜒𝑗 < (𝑗 + 1))
295 isorel 6836 . . . . . . . . . . 11 ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
29644, 54, 89, 295syl12anc 870 . . . . . . . . . 10 (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
297294, 296mpbid 224 . . . . . . . . 9 (𝜒 → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
2981simprbi 492 . . . . . . . . 9 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
299 eqid 2825 . . . . . . . . 9 if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300 eqid 2825 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300fourierdlem33 41149 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
302 eqidd 2826 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303 simpr 479 . . . . . . . . . . . 12 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304303oveq2d 6926 . . . . . . . . . . 11 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305304fveq2d 6441 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
306243adantr 474 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) ∈ ℝ*)
307245adantr 474 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
30890adantr 474 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
309193, 211, 290, 90, 297, 298fourierdlem10 41126 . . . . . . . . . . . . . 14 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310309simpld 490 . . . . . . . . . . . . 13 (𝜒 → (𝑄𝑖) ≤ (𝑆𝑗))
311193, 290, 90, 310, 297lelttrd 10521 . . . . . . . . . . . 12 (𝜒 → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
312311adantr 474 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
313211adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
314309simprd 491 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
315314adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
316 neqne 3007 . . . . . . . . . . . . . 14 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317316necomd 3054 . . . . . . . . . . . . 13 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318317adantl 475 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319308, 313, 315, 318leneltd 10517 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320306, 307, 308, 312, 319eliood 40517 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
321230, 90readdcld 10393 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322276, 321ffvelrnd 6614 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323322adantr 474 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324302, 305, 320, 323fvmptd 6539 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325324ifeq2da 4339 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326298resmptd 5693 . . . . . . . . 9 (𝜒 → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327326oveq1d 6925 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
328301, 325, 3273eltr3d 2920 . . . . . . 7 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
329 ax-resscn 10316 . . . . . . . . 9 ℝ ⊆ ℂ
330128, 329syl6ss 3839 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
33190recnd 10392 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332168, 330, 124, 331constlimc 40649 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆‘(𝑗 + 1))))
333167, 168, 161, 121, 125, 328, 332sublimc 40677 . . . . . 6 (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆‘(𝑗 + 1))))
334330, 162, 331idlimc 40651 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆‘(𝑗 + 1))))
3356, 105jca 507 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336 eleq1 2894 . . . . . . . . . 10 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337336anbi2d 622 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338 neeq1 3061 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339337, 338imbi12d 336 . . . . . . . 8 (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340339, 140vtoclg 3482 . . . . . . 7 ((𝑆‘(𝑗 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0))
34190, 335, 340sylc 65 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ≠ 0)
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 40681 . . . . 5 (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆‘(𝑗 + 1))))
343 eqid 2825 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344143, 150mulcld 10384 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345159neneqd 3004 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346 2re 11432 . . . . . . . . . . 11 2 ∈ ℝ
347346a1i 11 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
34817rehalfcld 11612 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349348resincld 15252 . . . . . . . . . . 11 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350349adantl 475 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351347, 350remulcld 10394 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352 elsng 4413 . . . . . . . . 9 ((2 · (sin‘(𝑠 / 2))) ∈ ℝ → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
353351, 352syl 17 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
354345, 353mtbird 317 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355344, 354eldifd 3809 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356 eqid 2825 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357 eqid 2825 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358 2cnd 11436 . . . . . . . 8 (𝜒 → 2 ∈ ℂ)
359356, 330, 358, 331constlimc 40649 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆‘(𝑗 + 1))))
360348ad2antrl 719 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361 recn 10349 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362361sincld 15239 . . . . . . . . 9 (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363362adantl 475 . . . . . . . 8 ((𝜒𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364 eqid 2825 . . . . . . . . 9 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365 2cn 11433 . . . . . . . . . . 11 2 ∈ ℂ
366 eldifsn 4538 . . . . . . . . . . 11 (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367365, 151, 366mpbir2an 702 . . . . . . . . . 10 2 ∈ (ℂ ∖ {0})
368367a1i 11 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ (ℂ ∖ {0}))
369151a1i 11 . . . . . . . . 9 (𝜒 → 2 ≠ 0)
370162, 356, 364, 148, 368, 334, 359, 369, 152divlimc 40681 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆‘(𝑗 + 1))))
371 sinf 15233 . . . . . . . . . . . . . 14 sin:ℂ⟶ℂ
372371a1i 11 . . . . . . . . . . . . 13 (⊤ → sin:ℂ⟶ℂ)
373329a1i 11 . . . . . . . . . . . . 13 (⊤ → ℝ ⊆ ℂ)
374372, 373feqresmpt 6501 . . . . . . . . . . . 12 (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375374mptru 1664 . . . . . . . . . . 11 (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376 resincncf 40881 . . . . . . . . . . 11 (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377375, 376eqeltrri 2903 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378377a1i 11 . . . . . . . . 9 (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
37990rehalfcld 11612 . . . . . . . . 9 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380 fveq2 6437 . . . . . . . . 9 (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381378, 379, 380cnmptlimc 24060 . . . . . . . 8 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆‘(𝑗 + 1)) / 2)))
382 fveq2 6437 . . . . . . . 8 (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383 fveq2 6437 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384383ad2antll 720 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385360, 363, 370, 381, 382, 384limcco 24063 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆‘(𝑗 + 1))))
386356, 357, 343, 143, 150, 359, 385mullimc 40641 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆‘(𝑗 + 1))))
387331halfcld 11610 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388387sincld 15239 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389154, 105sseldd 3828 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390 fourierdlem44 41160 . . . . . . . 8 (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391389, 341, 390syl2anc 579 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392358, 388, 369, 391mulne0d 11011 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 40681 . . . . 5 (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆‘(𝑗 + 1))))
3942, 3, 4, 142, 160, 342, 393mullimc 40641 . . . 4 (𝜒 → (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆‘(𝑗 + 1))))
395 fourierdlem76.d . . . . 5 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
396395a1i 11 . . . 4 (𝜒𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))))
397 fourierdlem76.o . . . . . . 7 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
398397reseq1i 5629 . . . . . 6 (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
399 ioossicc 12554 . . . . . . . 8 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1)))
400 iccss 12536 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
40119, 98, 85, 107, 400syl22anc 872 . . . . . . . 8 (𝜒 → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402399, 401syl5ss 3838 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403402resmptd 5693 . . . . . 6 (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404398, 403syl5eq 2873 . . . . 5 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405404oveq1d 6925 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆‘(𝑗 + 1))))
406394, 396, 4053eltr4d 2921 . . 3 (𝜒𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
4071, 406sylbir 227 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
408242, 249gtned 10498 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄𝑖))
409 fourierdlem76.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
4106, 223, 409syl2anc 579 . . . . . . . . . . 11 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
411240oveq2d 6926 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
412410, 411eleqtrd 2908 . . . . . . . . . 10 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
413193recnd 10392 . . . . . . . . . 10 (𝜒 → (𝑄𝑖) ∈ ℂ)
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 41168 . . . . . . . . 9 (𝜒𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄𝑖)))
415 eqid 2825 . . . . . . . . 9 if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)))
416 eqid 2825 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
417193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416fourierdlem32 41148 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
418 eqidd 2826 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419 oveq2 6918 . . . . . . . . . . . 12 (𝑠 = (𝑆𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆𝑗)))
420419fveq2d 6441 . . . . . . . . . . 11 (𝑠 = (𝑆𝑗) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
421420adantl 475 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) ∧ 𝑠 = (𝑆𝑗)) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
422243adantr 474 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ*)
423245adantr 474 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
424290adantr 474 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ℝ)
425193adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ)
426310adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ≤ (𝑆𝑗))
427 neqne 3007 . . . . . . . . . . . . 13 (¬ (𝑆𝑗) = (𝑄𝑖) → (𝑆𝑗) ≠ (𝑄𝑖))
428427adantl 475 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ≠ (𝑄𝑖))
429425, 424, 426, 428leneltd 10517 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) < (𝑆𝑗))
43090adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431211adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432297adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
433314adantr 474 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434424, 430, 431, 432, 433ltletrd 10523 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑄‘(𝑖 + 1)))
435422, 423, 424, 429, 434eliood 40517 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
436230, 290readdcld 10393 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆𝑗)) ∈ ℝ)
437276, 436ffvelrnd 6614 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
438437adantr 474 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
439418, 421, 435, 438fvmptd 6539 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)) = (𝐹‘(𝑋 + (𝑆𝑗))))
440439ifeq2da 4339 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))))
441326oveq1d 6925 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
442417, 440, 4413eltr3d 2920 . . . . . . 7 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
443290recnd 10392 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ ℂ)
444168, 330, 124, 443constlimc 40649 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆𝑗)))
445167, 168, 161, 121, 125, 442, 444sublimc 40677 . . . . . 6 (𝜒 → (if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆𝑗)))
446330, 162, 443idlimc 40651 . . . . . 6 (𝜒 → (𝑆𝑗) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆𝑗)))
4476, 83jca 507 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
448 eleq1 2894 . . . . . . . . . 10 (𝑠 = (𝑆𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
449448anbi2d 622 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵))))
450 neeq1 3061 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → (𝑠 ≠ 0 ↔ (𝑆𝑗) ≠ 0))
451449, 450imbi12d 336 . . . . . . . 8 (𝑠 = (𝑆𝑗) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0)))
452451, 140vtoclg 3482 . . . . . . 7 ((𝑆𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0))
45383, 447, 452sylc 65 . . . . . 6 (𝜒 → (𝑆𝑗) ≠ 0)
454161, 162, 2, 126, 166, 445, 446, 453, 141divlimc 40681 . . . . 5 (𝜒 → ((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆𝑗)))
455356, 330, 358, 443constlimc 40649 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆𝑗)))
456348ad2antrl 719 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457162, 356, 364, 148, 368, 446, 455, 369, 152divlimc 40681 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆𝑗)))
458290rehalfcld 11612 . . . . . . . . 9 (𝜒 → ((𝑆𝑗) / 2) ∈ ℝ)
459 fveq2 6437 . . . . . . . . 9 (𝑥 = ((𝑆𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆𝑗) / 2)))
460378, 458, 459cnmptlimc 24060 . . . . . . . 8 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆𝑗) / 2)))
461 fveq2 6437 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
462461ad2antll 720 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
463456, 363, 457, 460, 382, 462limcco 24063 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆𝑗)))
464356, 357, 343, 143, 150, 455, 463mullimc 40641 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆𝑗)))
465443halfcld 11610 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ℂ)
466465sincld 15239 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ℂ)
467154, 83sseldd 3828 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ (-π[,]π))
468 fourierdlem44 41160 . . . . . . . 8 (((𝑆𝑗) ∈ (-π[,]π) ∧ (𝑆𝑗) ≠ 0) → (sin‘((𝑆𝑗) / 2)) ≠ 0)
469467, 453, 468syl2anc 579 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ≠ 0)
470358, 466, 369, 469mulne0d 11011 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ≠ 0)
471162, 343, 3, 148, 355, 446, 464, 470, 159divlimc 40681 . . . . 5 (𝜒 → ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆𝑗)))
4722, 3, 4, 142, 160, 454, 471mullimc 40641 . . . 4 (𝜒 → (((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) · ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2))))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆𝑗)))
473 fourierdlem76.e . . . . 5 𝐸 = (((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) · ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2)))))
474473a1i 11 . . . 4 (𝜒𝐸 = (((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) · ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2))))))
475404oveq1d 6925 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆𝑗)))
476472, 474, 4753eltr4d 2921 . . 3 (𝜒𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
4771, 476sylbir 227 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
478298sselda 3827 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
479478, 266syldan 585 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480479mpteq2dva 4969 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481225adantr 474 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) ∈ ℝ*)
482228adantr 474 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
483230adantr 474 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484483, 129readdcld 10393 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485240adantr 474 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
486193adantr 474 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ)
487243adantr 474 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ*)
488245adantr 474 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
489487, 488, 478, 248syl3anc 1494 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) < 𝑠)
490486, 18, 483, 489ltadd2dd 10522 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
491485, 490eqbrtrd 4897 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
492211adantr 474 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493487, 488, 478, 253syl3anc 1494 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
49418, 492, 483, 493ltadd2dd 10522 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495260adantr 474 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496494, 495breqtrd 4901 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497481, 482, 484, 491, 496eliood 40517 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
498269, 271, 330, 237, 497fourierdlem23 41139 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499480, 498eqeltrd 2906 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500 ssid 3848 . . . . . . . . 9 ℂ ⊆ ℂ
501500a1i 11 . . . . . . . 8 (𝜒 → ℂ ⊆ ℂ)
502330, 124, 501constcncfg 40877 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503499, 502subcncf 40875 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504166ralrimiva 3175 . . . . . . . 8 (𝜒 → ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505 dfss3 3816 . . . . . . . 8 (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506504, 505sylibr 226 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507 difssd 3967 . . . . . . 7 (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508506, 507idcncfg 40878 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509503, 508divcncf 23620 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510330, 501idcncfg 40878 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511355, 343fmptd 6638 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512330, 358, 501constcncfg 40877 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513 sincn 24604 . . . . . . . . . . 11 sin ∈ (ℂ–cn→ℂ)
514513a1i 11 . . . . . . . . . 10 (𝜒 → sin ∈ (ℂ–cn→ℂ))
515367a1i 11 . . . . . . . . . . . 12 (𝜒 → 2 ∈ (ℂ ∖ {0}))
516330, 515, 507constcncfg 40877 . . . . . . . . . . 11 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517510, 516divcncf 23620 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518514, 517cncfmpt1f 23093 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519512, 518mulcncf 23619 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520 cncffvrn 23078 . . . . . . . 8 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)) → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
521507, 519, 520syl2anc 579 . . . . . . 7 (𝜒 → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522511, 521mpbird 249 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523510, 522divcncf 23620 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524509, 523mulcncf 23619 . . . 4 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525404, 524eqeltrd 2906 . . 3 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
5261, 525sylbir 227 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527407, 477, 526jca31 510 1 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗))) ∧ (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1656  wtru 1657  wcel 2164  wne 2999  wral 3117  {crab 3121  cdif 3795  cun 3796  cin 3797  wss 3798  ifcif 4308  {csn 4399  {cpr 4401   class class class wbr 4875  cmpt 4954  dom cdm 5346  ran crn 5347  cres 5348  cio 6088  Fun wfun 6121  wf 6123  1-1-ontowf1o 6126  cfv 6127   Isom wiso 6128  (class class class)co 6910  𝑚 cmap 8127  Fincfn 8228  cc 10257  cr 10258  0cc0 10259  1c1 10260   + caddc 10262   · cmul 10264  *cxr 10397   < clt 10398  cle 10399  cmin 10592  -cneg 10593   / cdiv 11016  cn 11357  2c2 11413  cz 11711  (,)cioo 12470  [,)cico 12472  [,]cicc 12473  ...cfz 12626  ..^cfzo 12767  chash 13417  sincsin 15173  πcpi 15176  t crest 16441  TopOpenctopn 16442  fldccnfld 20113  cnccncf 23056   lim climc 24032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-inf2 8822  ax-cnex 10315  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335  ax-pre-mulgt0 10336  ax-pre-sup 10337  ax-addf 10338  ax-mulf 10339
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-fal 1670  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-iin 4745  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-of 7162  df-om 7332  df-1st 7433  df-2nd 7434  df-supp 7565  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-2o 7832  df-oadd 7835  df-er 8014  df-map 8129  df-pm 8130  df-ixp 8182  df-en 8229  df-dom 8230  df-sdom 8231  df-fin 8232  df-fsupp 8551  df-fi 8592  df-sup 8623  df-inf 8624  df-oi 8691  df-card 9085  df-cda 9312  df-pnf 10400  df-mnf 10401  df-xr 10402  df-ltxr 10403  df-le 10404  df-sub 10594  df-neg 10595  df-div 11017  df-nn 11358  df-2 11421  df-3 11422  df-4 11423  df-5 11424  df-6 11425  df-7 11426  df-8 11427  df-9 11428  df-n0 11626  df-z 11712  df-dec 11829  df-uz 11976  df-q 12079  df-rp 12120  df-xneg 12239  df-xadd 12240  df-xmul 12241  df-ioo 12474  df-ioc 12475  df-ico 12476  df-icc 12477  df-fz 12627  df-fzo 12768  df-fl 12895  df-mod 12971  df-seq 13103  df-exp 13162  df-fac 13361  df-bc 13390  df-hash 13418  df-shft 14191  df-cj 14223  df-re 14224  df-im 14225  df-sqrt 14359  df-abs 14360  df-limsup 14586  df-clim 14603  df-rlim 14604  df-sum 14801  df-ef 15177  df-sin 15179  df-cos 15180  df-pi 15182  df-struct 16231  df-ndx 16232  df-slot 16233  df-base 16235  df-sets 16236  df-ress 16237  df-plusg 16325  df-mulr 16326  df-starv 16327  df-sca 16328  df-vsca 16329  df-ip 16330  df-tset 16331  df-ple 16332  df-ds 16334  df-unif 16335  df-hom 16336  df-cco 16337  df-rest 16443  df-topn 16444  df-0g 16462  df-gsum 16463  df-topgen 16464  df-pt 16465  df-prds 16468  df-xrs 16522  df-qtop 16527  df-imas 16528  df-xps 16530  df-mre 16606  df-mrc 16607  df-acs 16609  df-mgm 17602  df-sgrp 17644  df-mnd 17655  df-submnd 17696  df-mulg 17902  df-cntz 18107  df-cmn 18555  df-psmet 20105  df-xmet 20106  df-met 20107  df-bl 20108  df-mopn 20109  df-fbas 20110  df-fg 20111  df-cnfld 20114  df-top 21076  df-topon 21093  df-topsp 21115  df-bases 21128  df-cld 21201  df-ntr 21202  df-cls 21203  df-nei 21280  df-lp 21318  df-perf 21319  df-cn 21409  df-cnp 21410  df-haus 21497  df-tx 21743  df-hmeo 21936  df-fil 22027  df-fm 22119  df-flim 22120  df-flf 22121  df-xms 22502  df-ms 22503  df-tms 22504  df-cncf 23058  df-limc 24036  df-dv 24037
This theorem is referenced by:  fourierdlem86  41201
  Copyright terms: Public domain W3C validator