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 42452
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (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 2819 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3 eqid 2819 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4 eqid 2819 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5 simplll 773 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
61, 5sylbi 219 . . . . . . . . . 10 (𝜒𝜑)
76adantr 483 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8 ioossicc 12814 . . . . . . . . . 10 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9 fourierdlem76.a . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ)
109rexrd 10683 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ*)
116, 10syl 17 . . . . . . . . . . . 12 (𝜒𝐴 ∈ ℝ*)
1211adantr 483 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ*)
13 fourierdlem76.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℝ)
1413rexrd 10683 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ*)
156, 14syl 17 . . . . . . . . . . . 12 (𝜒𝐵 ∈ ℝ*)
1615adantr 483 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ*)
17 elioore 12760 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
1817adantl 484 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
196, 9syl 17 . . . . . . . . . . . . 13 (𝜒𝐴 ∈ ℝ)
2019adantr 483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22 prfi 8785 . . . . . . . . . . . . . . . . . . . . 21 {𝐴, 𝐵} ∈ Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ∈ Fin)
24 fzfid 13333 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0...𝑀) ∈ Fin)
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2625rnmptfi 41411 . . . . . . . . . . . . . . . . . . . . 21 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27 infi 8734 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29 unfi 8777 . . . . . . . . . . . . . . . . . . . 20 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3023, 28, 29syl2anc 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3121, 30eqeltrid 2915 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ Fin)
32 prssg 4744 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
339, 13, 32syl2anc 586 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
349, 13, 33mpbi2and 710 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35 inss2 4204 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36 ioossre 12790 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴(,)𝐵) ⊆ ℝ
3735, 36sstri 3974 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
3934, 38unssd 4160 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
4021, 39eqsstrid 4013 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ ℝ)
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18 𝑁 = ((♯‘𝑇) − 1)
4331, 40, 41, 42fourierdlem36 42413 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
446, 43syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑆 Isom < , < ((0...𝑁), 𝑇))
45 isof1o 7068 . . . . . . . . . . . . . . . 16 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
46 f1of 6608 . . . . . . . . . . . . . . . 16 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15 (𝜒𝑆:(0...𝑁)⟶𝑇)
486, 40syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑇 ⊆ ℝ)
4947, 48fssd 6521 . . . . . . . . . . . . . 14 (𝜒𝑆:(0...𝑁)⟶ℝ)
5049adantr 483 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51 simpllr 774 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
521, 51sylbi 219 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (0..^𝑁))
53 elfzofz 13045 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
5452, 53syl 17 . . . . . . . . . . . . . 14 (𝜒𝑗 ∈ (0...𝑁))
5554adantr 483 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
5650, 55ffvelrnd 6845 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ)
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑆:(0...𝑁)⟶𝑇)
58 frn 6513 . . . . . . . . . . . . . . . . . 18 (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆𝑇)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑆𝑇)
609leidd 11198 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐴)
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴 < 𝐵)
629, 13, 61ltled 10780 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐵)
639, 13, 9, 60, 62eliccd 41763 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐴[,]𝐵))
6413leidd 11198 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝐵)
659, 13, 13, 62, 64eliccd 41763 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (𝐴[,]𝐵))
66 prssg 4744 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
679, 13, 66syl2anc 586 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
6863, 65, 67mpbi2and 710 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
6935, 8sstri 3974 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
7069a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
7168, 70unssd 4160 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
7221, 71eqsstrid 4013 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ⊆ (𝐴[,]𝐵))
7359, 72sstrd 3975 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
746, 73syl 17 . . . . . . . . . . . . . . 15 (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75 ffun 6510 . . . . . . . . . . . . . . . . 17 (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
7649, 75syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → Fun 𝑆)
77 fdm 6515 . . . . . . . . . . . . . . . . . . 19 (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom 𝑆 = (0...𝑁))
7978eqcomd 2825 . . . . . . . . . . . . . . . . 17 (𝜒 → (0...𝑁) = dom 𝑆)
8054, 79eleqtrd 2913 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ dom 𝑆)
81 fvelrn 6837 . . . . . . . . . . . . . . . 16 ((Fun 𝑆𝑗 ∈ dom 𝑆) → (𝑆𝑗) ∈ ran 𝑆)
8276, 80, 81syl2anc 586 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆𝑗) ∈ ran 𝑆)
8374, 82sseldd 3966 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ (𝐴[,]𝐵))
84 iccgelb 12785 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆𝑗))
8511, 15, 83, 84syl3anc 1365 . . . . . . . . . . . . 13 (𝜒𝐴 ≤ (𝑆𝑗))
8685adantr 483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆𝑗))
8756rexrd 10683 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ*)
88 fzofzp1 13126 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
8952, 88syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
9049, 89ffvelrnd 6845 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
9190rexrd 10683 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
9291adantr 483 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
93 simpr 487 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
94 ioogtlb 41754 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9587, 92, 93, 94syl3anc 1365 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9620, 56, 18, 86, 95lelttrd 10790 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
9790adantr 483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
986, 13syl 17 . . . . . . . . . . . . 13 (𝜒𝐵 ∈ ℝ)
9998adantr 483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100 iooltub 41770 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10187, 92, 93, 100syl3anc 1365 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10289, 79eleqtrd 2913 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103 fvelrn 6837 . . . . . . . . . . . . . . . 16 ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10476, 102, 103syl2anc 586 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10574, 104sseldd 3966 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106 iccleub 12784 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10711, 15, 105, 106syl3anc 1365 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108107adantr 483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10918, 97, 99, 101, 108ltletrd 10792 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
11012, 16, 18, 96, 109eliood 41757 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
1118, 110sseldi 3963 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112 fourierdlem76.f . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶ℝ)
113112adantr 483 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114 fourierdlem76.xre . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
115114adantr 483 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
1169, 13iccssred 41764 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117116sselda 3965 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118115, 117readdcld 10662 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119113, 118ffvelrnd 6845 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
1207, 111, 119syl2anc 586 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121120recnd 10661 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122 fourierdlem76.c . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
123122recnd 10661 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1246, 123syl 17 . . . . . . . 8 (𝜒𝐶 ∈ ℂ)
125124adantr 483 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126121, 125subcld 10989 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127 ioossre 12790 . . . . . . . . 9 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128127a1i 11 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129128sselda 3965 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130129recnd 10661 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131 nne 3018 . . . . . . . . . . . 12 𝑠 ≠ 0 ↔ 𝑠 = 0)
132131biimpi 218 . . . . . . . . . . 11 𝑠 ≠ 0 → 𝑠 = 0)
133132eqcomd 2825 . . . . . . . . . 10 𝑠 ≠ 0 → 0 = 𝑠)
134133adantl 484 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135 simpr 487 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136135adantr 483 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137134, 136eqeltrd 2911 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138 fourierdlem76.n0 . . . . . . . . 9 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139138ad2antrr 724 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140137, 139condan 816 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
1417, 111, 140syl2anc 586 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142126, 130, 141divcld 11408 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143 2cnd 11707 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144130halfcld 11874 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145144sincld 15475 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146143, 145mulcld 10653 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
14717recnd 10661 . . . . . . . . . 10 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148147adantl 484 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149148halfcld 11874 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150149sincld 15475 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151 2ne0 11733 . . . . . . . 8 2 ≠ 0
152151a1i 11 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153 fourierdlem76.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
1546, 153syl 17 . . . . . . . . . 10 (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155154adantr 483 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156155, 111sseldd 3966 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157 fourierdlem44 42421 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158156, 141, 157syl2anc 586 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159143, 150, 152, 158mulne0d 11284 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160130, 146, 159divcld 11408 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161 eqid 2819 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162 eqid 2819 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163141neneqd 3019 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164 velsn 4575 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
165163, 164sylnibr 331 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166130, 165eldifd 3945 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167 eqid 2819 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168 eqid 2819 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169 elfzofz 13045 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169adantl 484 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171 pire 25036 . . . . . . . . . . . . . . . . . . . . 21 π ∈ ℝ
172171renegcli 10939 . . . . . . . . . . . . . . . . . . . 20 -π ∈ ℝ
173172a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -π ∈ ℝ)
174173, 114readdcld 10662 . . . . . . . . . . . . . . . . . 18 (𝜑 → (-π + 𝑋) ∈ ℝ)
175171a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → π ∈ ℝ)
176175, 114readdcld 10662 . . . . . . . . . . . . . . . . . 18 (𝜑 → (π + 𝑋) ∈ ℝ)
177174, 176iccssred 41764 . . . . . . . . . . . . . . . . 17 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178177adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℕ)
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19 (𝜑𝑉 ∈ (𝑃𝑀))
182179, 180, 181fourierdlem15 42392 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183182adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184183, 170ffvelrnd 6845 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185178, 184sseldd 3966 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
186114adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187185, 186resubcld 11060 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
18825fvmpt2 6772 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
189170, 187, 188syl2anc 586 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
190189, 187eqeltrd 2911 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
191190adantlr 713 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
192191adantr 483 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
1931, 192sylbi 219 . . . . . . . . 9 (𝜒 → (𝑄𝑖) ∈ ℝ)
194 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
195194oveq1d 7163 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
196195cbvmptv 5160 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
19725, 196eqtri 2842 . . . . . . . . . . . . . . 15 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
198197a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
199 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
200199oveq1d 7163 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201200adantl 484 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202 fzofzp1 13126 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203202adantl 484 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204183, 203ffvelrnd 6845 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205178, 204sseldd 3966 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206205, 186resubcld 11060 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207198, 201, 203, 206fvmptd 6768 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208207, 206eqeltrd 2911 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208adantlr 713 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210209adantr 483 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2111, 210sylbi 219 . . . . . . . . 9 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212179fourierdlem2 42379 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
213180, 212syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
214181, 213mpbid 234 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
215214simprrd 772 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
216215r19.21bi 3206 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
217185, 205, 186, 216ltsub1dd 11244 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218217, 189, 2073brtr4d 5089 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
219218adantlr 713 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
220219adantr 483 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2211, 220sylbi 219 . . . . . . . . 9 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2221biimpi 218 . . . . . . . . . . . . . . . . . 18 (𝜒 → (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
223222simplrd 768 . . . . . . . . . . . . . . . . 17 (𝜒𝑖 ∈ (0..^𝑀))
2246, 223, 185syl2anc 586 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) ∈ ℝ)
225224rexrd 10683 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ∈ ℝ*)
226225adantr 483 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2276, 223, 205syl2anc 586 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228227rexrd 10683 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
229228adantr 483 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
2306, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑋 ∈ ℝ)
231230adantr 483 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232 elioore 12760 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233232adantl 484 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234231, 233readdcld 10662 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
2356, 223, 189syl2anc 586 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
236235oveq2d 7164 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
237230recnd 10661 . . . . . . . . . . . . . . . . . 18 (𝜒𝑋 ∈ ℂ)
238224recnd 10661 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉𝑖) ∈ ℂ)
239237, 238pncan3d 10992 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
240236, 239eqtr2d 2855 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
241240adantr 483 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
242193adantr 483 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
243193rexrd 10683 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) ∈ ℝ*)
244243adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
245211rexrd 10683 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246245adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
247 simpr 487 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
248 ioogtlb 41754 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
249244, 246, 247, 248syl3anc 1365 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
250242, 233, 231, 249ltadd2dd 10791 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
251241, 250eqbrtrd 5079 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
252211adantr 483 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253 iooltub 41770 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254244, 246, 247, 253syl3anc 1365 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255233, 252, 231, 254ltadd2dd 10791 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
2566, 223, 207syl2anc 586 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257256oveq2d 7164 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258227recnd 10661 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259237, 258pncan3d 10992 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260257, 259eqtrd 2854 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261260adantr 483 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262255, 261breqtrd 5083 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263226, 229, 234, 251, 262eliood 41757 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
264 fvres 6682 . . . . . . . . . . . . 13 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265263, 264syl 17 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266265eqcomd 2825 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267266mpteq2dva 5152 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268 ioosscn 41753 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269268a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270 fourierdlem76.fcn . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
2716, 223, 270syl2anc 586 . . . . . . . . . . 11 (𝜒 → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272 ioosscn 41753 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273272a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274269, 271, 273, 237, 263fourierdlem23 42400 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275267, 274eqeltrd 2911 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2766, 112syl 17 . . . . . . . . . 10 (𝜒𝐹:ℝ⟶ℝ)
277 ioossre 12790 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278277a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279 eqid 2819 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280 ioossre 12790 . . . . . . . . . . 11 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281280a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282233, 254ltned 10768 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283 fourierdlem76.l . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
2846, 223, 283syl2anc 586 . . . . . . . . . . 11 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
285260eqcomd 2825 . . . . . . . . . . . 12 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286285oveq2d 7164 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
287284, 286eleqtrd 2913 . . . . . . . . . 10 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
288211recnd 10661 . . . . . . . . . 10 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 42429 . . . . . . . . 9 (𝜒𝐿 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
29049, 54ffvelrnd 6845 . . . . . . . . 9 (𝜒 → (𝑆𝑗) ∈ ℝ)
291 elfzoelz 13030 . . . . . . . . . . . 12 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292 zre 11977 . . . . . . . . . . . 12 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
29352, 291, 2923syl 18 . . . . . . . . . . 11 (𝜒𝑗 ∈ ℝ)
294293ltp1d 11562 . . . . . . . . . 10 (𝜒𝑗 < (𝑗 + 1))
295 isorel 7071 . . . . . . . . . . 11 ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
29644, 54, 89, 295syl12anc 834 . . . . . . . . . 10 (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
297294, 296mpbid 234 . . . . . . . . 9 (𝜒 → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
2981simprbi 499 . . . . . . . . 9 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
299 eqid 2819 . . . . . . . . 9 if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300 eqid 2819 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300fourierdlem33 42410 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
302 eqidd 2820 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303 simpr 487 . . . . . . . . . . . 12 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304303oveq2d 7164 . . . . . . . . . . 11 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305304fveq2d 6667 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
306243adantr 483 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) ∈ ℝ*)
307245adantr 483 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
30890adantr 483 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
309193, 211, 290, 90, 297, 298fourierdlem10 42387 . . . . . . . . . . . . . 14 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310309simpld 497 . . . . . . . . . . . . 13 (𝜒 → (𝑄𝑖) ≤ (𝑆𝑗))
311193, 290, 90, 310, 297lelttrd 10790 . . . . . . . . . . . 12 (𝜒 → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
312311adantr 483 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
313211adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
314309simprd 498 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
315314adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
316 neqne 3022 . . . . . . . . . . . . . 14 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317316necomd 3069 . . . . . . . . . . . . 13 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318317adantl 484 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319308, 313, 315, 318leneltd 10786 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320306, 307, 308, 312, 319eliood 41757 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
321230, 90readdcld 10662 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322276, 321ffvelrnd 6845 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323322adantr 483 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324302, 305, 320, 323fvmptd 6768 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325324ifeq2da 4496 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326298resmptd 5901 . . . . . . . . 9 (𝜒 → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327326oveq1d 7163 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
328301, 325, 3273eltr3d 2925 . . . . . . 7 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
329 ax-resscn 10586 . . . . . . . . 9 ℝ ⊆ ℂ
330128, 329sstrdi 3977 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
33190recnd 10661 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332168, 330, 124, 331constlimc 41889 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆‘(𝑗 + 1))))
333167, 168, 161, 121, 125, 328, 332sublimc 41917 . . . . . 6 (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆‘(𝑗 + 1))))
334330, 162, 331idlimc 41891 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆‘(𝑗 + 1))))
3356, 105jca 514 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336 eleq1 2898 . . . . . . . . . 10 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337336anbi2d 630 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338 neeq1 3076 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339337, 338imbi12d 347 . . . . . . . 8 (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340339, 140vtoclg 3566 . . . . . . 7 ((𝑆‘(𝑗 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0))
34190, 335, 340sylc 65 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ≠ 0)
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 41921 . . . . 5 (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆‘(𝑗 + 1))))
343 eqid 2819 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344143, 150mulcld 10653 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345159neneqd 3019 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346 2re 11703 . . . . . . . . . . 11 2 ∈ ℝ
347346a1i 11 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
34817rehalfcld 11876 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349348resincld 15488 . . . . . . . . . . 11 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350349adantl 484 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351347, 350remulcld 10663 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352 elsng 4573 . . . . . . . . 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 327 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355344, 354eldifd 3945 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356 eqid 2819 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357 eqid 2819 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358 2cnd 11707 . . . . . . . 8 (𝜒 → 2 ∈ ℂ)
359356, 330, 358, 331constlimc 41889 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆‘(𝑗 + 1))))
360348ad2antrl 726 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361 recn 10619 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362361sincld 15475 . . . . . . . . 9 (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363362adantl 484 . . . . . . . 8 ((𝜒𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364 eqid 2819 . . . . . . . . 9 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365 2cn 11704 . . . . . . . . . . 11 2 ∈ ℂ
366 eldifsn 4711 . . . . . . . . . . 11 (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367365, 151, 366mpbir2an 709 . . . . . . . . . 10 2 ∈ (ℂ ∖ {0})
368367a1i 11 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ (ℂ ∖ {0}))
369151a1i 11 . . . . . . . . 9 (𝜒 → 2 ≠ 0)
370162, 356, 364, 148, 368, 334, 359, 369, 152divlimc 41921 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆‘(𝑗 + 1))))
371 sinf 15469 . . . . . . . . . . . . . 14 sin:ℂ⟶ℂ
372371a1i 11 . . . . . . . . . . . . 13 (⊤ → sin:ℂ⟶ℂ)
373329a1i 11 . . . . . . . . . . . . 13 (⊤ → ℝ ⊆ ℂ)
374372, 373feqresmpt 6727 . . . . . . . . . . . 12 (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375374mptru 1537 . . . . . . . . . . 11 (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376 resincncf 42142 . . . . . . . . . . 11 (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377375, 376eqeltrri 2908 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378377a1i 11 . . . . . . . . 9 (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
37990rehalfcld 11876 . . . . . . . . 9 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380 fveq2 6663 . . . . . . . . 9 (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381378, 379, 380cnmptlimc 24480 . . . . . . . 8 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆‘(𝑗 + 1)) / 2)))
382 fveq2 6663 . . . . . . . 8 (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383 fveq2 6663 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384383ad2antll 727 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385360, 363, 370, 381, 382, 384limcco 24483 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆‘(𝑗 + 1))))
386356, 357, 343, 143, 150, 359, 385mullimc 41881 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆‘(𝑗 + 1))))
387331halfcld 11874 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388387sincld 15475 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389154, 105sseldd 3966 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390 fourierdlem44 42421 . . . . . . . 8 (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391389, 341, 390syl2anc 586 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392358, 388, 369, 391mulne0d 11284 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 41921 . . . . 5 (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆‘(𝑗 + 1))))
3942, 3, 4, 142, 160, 342, 393mullimc 41881 . . . 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 5842 . . . . . 6 (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
399 ioossicc 12814 . . . . . . . 8 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1)))
400 iccss 12796 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
40119, 98, 85, 107, 400syl22anc 836 . . . . . . . 8 (𝜒 → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402399, 401sstrid 3976 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403402resmptd 5901 . . . . . 6 (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404398, 403syl5eq 2866 . . . . 5 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405404oveq1d 7163 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆‘(𝑗 + 1))))
406394, 396, 4053eltr4d 2926 . . 3 (𝜒𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
4071, 406sylbir 237 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
408242, 249gtned 10767 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄𝑖))
409 fourierdlem76.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
4106, 223, 409syl2anc 586 . . . . . . . . . . 11 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
411240oveq2d 7164 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
412410, 411eleqtrd 2913 . . . . . . . . . 10 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
413193recnd 10661 . . . . . . . . . 10 (𝜒 → (𝑄𝑖) ∈ ℂ)
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 42429 . . . . . . . . 9 (𝜒𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄𝑖)))
415 eqid 2819 . . . . . . . . 9 if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)))
416 eqid 2819 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
417193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416fourierdlem32 42409 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
418 eqidd 2820 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419 oveq2 7156 . . . . . . . . . . . 12 (𝑠 = (𝑆𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆𝑗)))
420419fveq2d 6667 . . . . . . . . . . 11 (𝑠 = (𝑆𝑗) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
421420adantl 484 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) ∧ 𝑠 = (𝑆𝑗)) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
422243adantr 483 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ*)
423245adantr 483 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
424290adantr 483 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ℝ)
425193adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ)
426310adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ≤ (𝑆𝑗))
427 neqne 3022 . . . . . . . . . . . . 13 (¬ (𝑆𝑗) = (𝑄𝑖) → (𝑆𝑗) ≠ (𝑄𝑖))
428427adantl 484 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ≠ (𝑄𝑖))
429425, 424, 426, 428leneltd 10786 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) < (𝑆𝑗))
43090adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431211adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432297adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
433314adantr 483 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434424, 430, 431, 432, 433ltletrd 10792 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑄‘(𝑖 + 1)))
435422, 423, 424, 429, 434eliood 41757 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
436230, 290readdcld 10662 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆𝑗)) ∈ ℝ)
437276, 436ffvelrnd 6845 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
438437adantr 483 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
439418, 421, 435, 438fvmptd 6768 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)) = (𝐹‘(𝑋 + (𝑆𝑗))))
440439ifeq2da 4496 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))))
441326oveq1d 7163 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
442417, 440, 4413eltr3d 2925 . . . . . . 7 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
443290recnd 10661 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ ℂ)
444168, 330, 124, 443constlimc 41889 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆𝑗)))
445167, 168, 161, 121, 125, 442, 444sublimc 41917 . . . . . 6 (𝜒 → (if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆𝑗)))
446330, 162, 443idlimc 41891 . . . . . 6 (𝜒 → (𝑆𝑗) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆𝑗)))
4476, 83jca 514 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
448 eleq1 2898 . . . . . . . . . 10 (𝑠 = (𝑆𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
449448anbi2d 630 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵))))
450 neeq1 3076 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → (𝑠 ≠ 0 ↔ (𝑆𝑗) ≠ 0))
451449, 450imbi12d 347 . . . . . . . 8 (𝑠 = (𝑆𝑗) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0)))
452451, 140vtoclg 3566 . . . . . . 7 ((𝑆𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0))
45383, 447, 452sylc 65 . . . . . 6 (𝜒 → (𝑆𝑗) ≠ 0)
454161, 162, 2, 126, 166, 445, 446, 453, 141divlimc 41921 . . . . 5 (𝜒 → ((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆𝑗)))
455356, 330, 358, 443constlimc 41889 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆𝑗)))
456348ad2antrl 726 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457162, 356, 364, 148, 368, 446, 455, 369, 152divlimc 41921 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆𝑗)))
458290rehalfcld 11876 . . . . . . . . 9 (𝜒 → ((𝑆𝑗) / 2) ∈ ℝ)
459 fveq2 6663 . . . . . . . . 9 (𝑥 = ((𝑆𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆𝑗) / 2)))
460378, 458, 459cnmptlimc 24480 . . . . . . . 8 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆𝑗) / 2)))
461 fveq2 6663 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
462461ad2antll 727 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
463456, 363, 457, 460, 382, 462limcco 24483 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆𝑗)))
464356, 357, 343, 143, 150, 455, 463mullimc 41881 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆𝑗)))
465443halfcld 11874 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ℂ)
466465sincld 15475 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ℂ)
467154, 83sseldd 3966 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ (-π[,]π))
468 fourierdlem44 42421 . . . . . . . 8 (((𝑆𝑗) ∈ (-π[,]π) ∧ (𝑆𝑗) ≠ 0) → (sin‘((𝑆𝑗) / 2)) ≠ 0)
469467, 453, 468syl2anc 586 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ≠ 0)
470358, 466, 369, 469mulne0d 11284 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ≠ 0)
471162, 343, 3, 148, 355, 446, 464, 470, 159divlimc 41921 . . . . 5 (𝜒 → ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆𝑗)))
4722, 3, 4, 142, 160, 454, 471mullimc 41881 . . . 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 7163 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆𝑗)))
476472, 474, 4753eltr4d 2926 . . 3 (𝜒𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
4771, 476sylbir 237 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
478298sselda 3965 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
479478, 266syldan 593 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480479mpteq2dva 5152 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481225adantr 483 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) ∈ ℝ*)
482228adantr 483 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
483230adantr 483 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484483, 129readdcld 10662 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485240adantr 483 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
486193adantr 483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ)
487243adantr 483 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ*)
488245adantr 483 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
489487, 488, 478, 248syl3anc 1365 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) < 𝑠)
490486, 18, 483, 489ltadd2dd 10791 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
491485, 490eqbrtrd 5079 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
492211adantr 483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493487, 488, 478, 253syl3anc 1365 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
49418, 492, 483, 493ltadd2dd 10791 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495260adantr 483 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496494, 495breqtrd 5083 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497481, 482, 484, 491, 496eliood 41757 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
498269, 271, 330, 237, 497fourierdlem23 42400 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499480, 498eqeltrd 2911 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500 ssid 3987 . . . . . . . . 9 ℂ ⊆ ℂ
501500a1i 11 . . . . . . . 8 (𝜒 → ℂ ⊆ ℂ)
502330, 124, 501constcncfg 42138 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503499, 502subcncf 42136 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504166ralrimiva 3180 . . . . . . . 8 (𝜒 → ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505 dfss3 3954 . . . . . . . 8 (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506504, 505sylibr 236 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507 difssd 4107 . . . . . . 7 (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508506, 507idcncfg 42139 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509503, 508divcncf 24040 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510330, 501idcncfg 42139 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511355, 343fmptd 6871 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512330, 358, 501constcncfg 42138 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513 sincn 25024 . . . . . . . . . . 11 sin ∈ (ℂ–cn→ℂ)
514513a1i 11 . . . . . . . . . 10 (𝜒 → sin ∈ (ℂ–cn→ℂ))
515367a1i 11 . . . . . . . . . . . 12 (𝜒 → 2 ∈ (ℂ ∖ {0}))
516330, 515, 507constcncfg 42138 . . . . . . . . . . 11 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517510, 516divcncf 24040 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518514, 517cncfmpt1f 23513 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519512, 518mulcncf 24039 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520 cncffvrn 23498 . . . . . . . 8 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)) → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
521507, 519, 520syl2anc 586 . . . . . . 7 (𝜒 → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522511, 521mpbird 259 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523510, 522divcncf 24040 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524509, 523mulcncf 24039 . . . 4 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525404, 524eqeltrd 2911 . . 3 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
5261, 525sylbir 237 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527407, 477, 526jca31 517 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 208  wa 398   = wceq 1530  wtru 1531  wcel 2107  wne 3014  wral 3136  {crab 3140  cdif 3931  cun 3932  cin 3933  wss 3934  ifcif 4465  {csn 4559  {cpr 4561   class class class wbr 5057  cmpt 5137  dom cdm 5548  ran crn 5549  cres 5550  cio 6305  Fun wfun 6342  wf 6344  1-1-ontowf1o 6347  cfv 6348   Isom wiso 6349  (class class class)co 7148  m cmap 8398  Fincfn 8501  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  *cxr 10666   < clt 10667  cle 10668  cmin 10862  -cneg 10863   / cdiv 11289  cn 11630  2c2 11684  cz 11973  (,)cioo 12730  [,)cico 12732  [,]cicc 12733  ...cfz 12884  ..^cfzo 13025  chash 13682  sincsin 15409  πcpi 15412  t crest 16686  TopOpenctopn 16687  fldccnfld 20537  cnccncf 23476   lim climc 24452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-supp 7823  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ioc 12735  df-ico 12736  df-icc 12737  df-fz 12885  df-fzo 13026  df-fl 13154  df-mod 13230  df-seq 13362  df-exp 13422  df-fac 13626  df-bc 13655  df-hash 13683  df-shft 14418  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-sum 15035  df-ef 15413  df-sin 15415  df-cos 15416  df-pi 15418  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-fbas 20534  df-fg 20535  df-cnfld 20538  df-top 21494  df-topon 21511  df-topsp 21533  df-bases 21546  df-cld 21619  df-ntr 21620  df-cls 21621  df-nei 21698  df-lp 21736  df-perf 21737  df-cn 21827  df-cnp 21828  df-haus 21915  df-tx 22162  df-hmeo 22355  df-fil 22446  df-fm 22538  df-flim 22539  df-flf 22540  df-xms 22922  df-ms 22923  df-tms 22924  df-cncf 23478  df-limc 24456  df-dv 24457
This theorem is referenced by:  fourierdlem86  42462
  Copyright terms: Public domain W3C validator