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 40879
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 2813 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3 eqid 2813 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4 eqid 2813 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5 simplll 782 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
61, 5sylbi 208 . . . . . . . . . 10 (𝜒𝜑)
76adantr 468 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8 ioossicc 12480 . . . . . . . . . 10 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9 fourierdlem76.a . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ)
109rexrd 10377 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ*)
116, 10syl 17 . . . . . . . . . . . 12 (𝜒𝐴 ∈ ℝ*)
1211adantr 468 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ*)
13 fourierdlem76.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℝ)
1413rexrd 10377 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ*)
156, 14syl 17 . . . . . . . . . . . 12 (𝜒𝐵 ∈ ℝ*)
1615adantr 468 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ*)
17 elioore 12426 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
1817adantl 469 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
196, 9syl 17 . . . . . . . . . . . . 13 (𝜒𝐴 ∈ ℝ)
2019adantr 468 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22 prfi 8477 . . . . . . . . . . . . . . . . . . . . 21 {𝐴, 𝐵} ∈ Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ∈ Fin)
24 fzfid 12999 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0...𝑀) ∈ Fin)
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2625rnmptfi 39841 . . . . . . . . . . . . . . . . . . . . 21 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27 infi 8426 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29 unfi 8469 . . . . . . . . . . . . . . . . . . . 20 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3023, 28, 29syl2anc 575 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3121, 30syl5eqel 2896 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ Fin)
32 prssg 4547 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
339, 13, 32syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
349, 13, 33mpbi2and 694 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35 inss2 4037 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36 ioossre 12456 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴(,)𝐵) ⊆ ℝ
3735, 36sstri 3814 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
3934, 38unssd 3995 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
4021, 39syl5eqss 3853 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ ℝ)
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18 𝑁 = ((♯‘𝑇) − 1)
4331, 40, 41, 42fourierdlem36 40840 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
446, 43syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑆 Isom < , < ((0...𝑁), 𝑇))
45 isof1o 6800 . . . . . . . . . . . . . . . 16 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
46 f1of 6356 . . . . . . . . . . . . . . . 16 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15 (𝜒𝑆:(0...𝑁)⟶𝑇)
486, 40syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑇 ⊆ ℝ)
4947, 48fssd 6273 . . . . . . . . . . . . . 14 (𝜒𝑆:(0...𝑁)⟶ℝ)
5049adantr 468 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51 simpllr 784 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
521, 51sylbi 208 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (0..^𝑁))
53 elfzofz 12712 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
5452, 53syl 17 . . . . . . . . . . . . . 14 (𝜒𝑗 ∈ (0...𝑁))
5554adantr 468 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
5650, 55ffvelrnd 6585 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ)
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑆:(0...𝑁)⟶𝑇)
58 frn 6265 . . . . . . . . . . . . . . . . . 18 (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆𝑇)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑆𝑇)
609leidd 10882 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐴)
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴 < 𝐵)
629, 13, 61ltled 10473 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐵)
639, 13, 9, 60, 62eliccd 40211 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐴[,]𝐵))
6413leidd 10882 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝐵)
659, 13, 13, 62, 64eliccd 40211 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (𝐴[,]𝐵))
66 prssg 4547 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
679, 13, 66syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
6863, 65, 67mpbi2and 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
6935, 8sstri 3814 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
7069a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
7168, 70unssd 3995 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
7221, 71syl5eqss 3853 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ⊆ (𝐴[,]𝐵))
7359, 72sstrd 3815 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
746, 73syl 17 . . . . . . . . . . . . . . 15 (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75 ffun 6262 . . . . . . . . . . . . . . . . 17 (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
7649, 75syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → Fun 𝑆)
77 fdm 6267 . . . . . . . . . . . . . . . . . . 19 (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom 𝑆 = (0...𝑁))
7978eqcomd 2819 . . . . . . . . . . . . . . . . 17 (𝜒 → (0...𝑁) = dom 𝑆)
8054, 79eleqtrd 2894 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ dom 𝑆)
81 fvelrn 6577 . . . . . . . . . . . . . . . 16 ((Fun 𝑆𝑗 ∈ dom 𝑆) → (𝑆𝑗) ∈ ran 𝑆)
8276, 80, 81syl2anc 575 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆𝑗) ∈ ran 𝑆)
8374, 82sseldd 3806 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ (𝐴[,]𝐵))
84 iccgelb 12451 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆𝑗))
8511, 15, 83, 84syl3anc 1483 . . . . . . . . . . . . 13 (𝜒𝐴 ≤ (𝑆𝑗))
8685adantr 468 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆𝑗))
8756rexrd 10377 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ*)
88 fzofzp1 12792 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
8952, 88syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
9049, 89ffvelrnd 6585 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
9190rexrd 10377 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
9291adantr 468 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
93 simpr 473 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
94 ioogtlb 40202 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9587, 92, 93, 94syl3anc 1483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9620, 56, 18, 86, 95lelttrd 10483 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
9790adantr 468 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
986, 13syl 17 . . . . . . . . . . . . 13 (𝜒𝐵 ∈ ℝ)
9998adantr 468 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100 iooltub 40218 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10187, 92, 93, 100syl3anc 1483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10289, 79eleqtrd 2894 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103 fvelrn 6577 . . . . . . . . . . . . . . . 16 ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10476, 102, 103syl2anc 575 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10574, 104sseldd 3806 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106 iccleub 12450 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10711, 15, 105, 106syl3anc 1483 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108107adantr 468 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10918, 97, 99, 101, 108ltletrd 10485 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
11012, 16, 18, 96, 109eliood 40205 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
1118, 110sseldi 3803 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112 fourierdlem76.f . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶ℝ)
113112adantr 468 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114 fourierdlem76.xre . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
115114adantr 468 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
1169, 13iccssred 40212 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117116sselda 3805 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118115, 117readdcld 10357 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119113, 118ffvelrnd 6585 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
1207, 111, 119syl2anc 575 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121120recnd 10356 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122 fourierdlem76.c . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
123122recnd 10356 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1246, 123syl 17 . . . . . . . 8 (𝜒𝐶 ∈ ℂ)
125124adantr 468 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126121, 125subcld 10680 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127 ioossre 12456 . . . . . . . . 9 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128127a1i 11 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129128sselda 3805 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130129recnd 10356 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131 nne 2989 . . . . . . . . . . . 12 𝑠 ≠ 0 ↔ 𝑠 = 0)
132131biimpi 207 . . . . . . . . . . 11 𝑠 ≠ 0 → 𝑠 = 0)
133132eqcomd 2819 . . . . . . . . . 10 𝑠 ≠ 0 → 0 = 𝑠)
134133adantl 469 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135 simpr 473 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136135adantr 468 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137134, 136eqeltrd 2892 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138 fourierdlem76.n0 . . . . . . . . 9 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139138ad2antrr 708 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140137, 139condan 843 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
1417, 111, 140syl2anc 575 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142126, 130, 141divcld 11089 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143 2cnd 11380 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144130halfcld 11547 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145144sincld 15083 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146143, 145mulcld 10348 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
14717recnd 10356 . . . . . . . . . 10 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148147adantl 469 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149148halfcld 11547 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150149sincld 15083 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151 2ne0 11399 . . . . . . . 8 2 ≠ 0
152151a1i 11 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153 fourierdlem76.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
1546, 153syl 17 . . . . . . . . . 10 (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155154adantr 468 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156155, 111sseldd 3806 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157 fourierdlem44 40848 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158156, 141, 157syl2anc 575 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159143, 150, 152, 158mulne0d 10967 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160130, 146, 159divcld 11089 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161 eqid 2813 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162 eqid 2813 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163141neneqd 2990 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164 velsn 4393 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
165163, 164sylnibr 320 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166130, 165eldifd 3787 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167 eqid 2813 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168 eqid 2813 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169 elfzofz 12712 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171 pire 24431 . . . . . . . . . . . . . . . . . . . . 21 π ∈ ℝ
172171renegcli 10630 . . . . . . . . . . . . . . . . . . . 20 -π ∈ ℝ
173172a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -π ∈ ℝ)
174173, 114readdcld 10357 . . . . . . . . . . . . . . . . . 18 (𝜑 → (-π + 𝑋) ∈ ℝ)
175171a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → π ∈ ℝ)
176175, 114readdcld 10357 . . . . . . . . . . . . . . . . . 18 (𝜑 → (π + 𝑋) ∈ ℝ)
177174, 176iccssred 40212 . . . . . . . . . . . . . . . . 17 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178177adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℕ)
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19 (𝜑𝑉 ∈ (𝑃𝑀))
182179, 180, 181fourierdlem15 40819 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183182adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184183, 170ffvelrnd 6585 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185178, 184sseldd 3806 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
186114adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187185, 186resubcld 10746 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
18825fvmpt2 6515 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
189170, 187, 188syl2anc 575 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
190189, 187eqeltrd 2892 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
191190adantlr 697 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
192191adantr 468 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
1931, 192sylbi 208 . . . . . . . . 9 (𝜒 → (𝑄𝑖) ∈ ℝ)
194 fveq2 6411 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
195194oveq1d 6892 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
196195cbvmptv 4951 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
19725, 196eqtri 2835 . . . . . . . . . . . . . . 15 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
198197a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
199 fveq2 6411 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
200199oveq1d 6892 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201200adantl 469 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202 fzofzp1 12792 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203202adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204183, 203ffvelrnd 6585 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205178, 204sseldd 3806 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206205, 186resubcld 10746 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207198, 201, 203, 206fvmptd 6512 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208207, 206eqeltrd 2892 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208adantlr 697 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210209adantr 468 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2111, 210sylbi 208 . . . . . . . . 9 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212179fourierdlem2 40806 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
213180, 212syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
214181, 213mpbid 223 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
215214simprrd 781 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
216215r19.21bi 3127 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
217185, 205, 186, 216ltsub1dd 10927 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218217, 189, 2073brtr4d 4883 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
219218adantlr 697 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
220219adantr 468 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2211, 220sylbi 208 . . . . . . . . 9 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2221biimpi 207 . . . . . . . . . . . . . . . . . 18 (𝜒 → (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
223222simplrd 777 . . . . . . . . . . . . . . . . 17 (𝜒𝑖 ∈ (0..^𝑀))
2246, 223, 185syl2anc 575 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) ∈ ℝ)
225224rexrd 10377 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ∈ ℝ*)
226225adantr 468 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2276, 223, 205syl2anc 575 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228227rexrd 10377 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
229228adantr 468 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
2306, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑋 ∈ ℝ)
231230adantr 468 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232 elioore 12426 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233232adantl 469 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234231, 233readdcld 10357 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
2356, 223, 189syl2anc 575 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
236235oveq2d 6893 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
237230recnd 10356 . . . . . . . . . . . . . . . . . 18 (𝜒𝑋 ∈ ℂ)
238224recnd 10356 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉𝑖) ∈ ℂ)
239237, 238pncan3d 10683 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
240236, 239eqtr2d 2848 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
241240adantr 468 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
242193adantr 468 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
243193rexrd 10377 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) ∈ ℝ*)
244243adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
245211rexrd 10377 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246245adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
247 simpr 473 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
248 ioogtlb 40202 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
249244, 246, 247, 248syl3anc 1483 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
250242, 233, 231, 249ltadd2dd 10484 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
251241, 250eqbrtrd 4873 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
252211adantr 468 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253 iooltub 40218 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254244, 246, 247, 253syl3anc 1483 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255233, 252, 231, 254ltadd2dd 10484 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
2566, 223, 207syl2anc 575 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257256oveq2d 6893 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258227recnd 10356 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259237, 258pncan3d 10683 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260257, 259eqtrd 2847 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261260adantr 468 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262255, 261breqtrd 4877 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263226, 229, 234, 251, 262eliood 40205 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
264 fvres 6430 . . . . . . . . . . . . 13 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265263, 264syl 17 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266265eqcomd 2819 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267266mpteq2dva 4945 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268 ioosscn 40201 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269268a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270 fourierdlem76.fcn . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
2716, 223, 270syl2anc 575 . . . . . . . . . . 11 (𝜒 → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272 ioosscn 40201 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273272a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274269, 271, 273, 237, 263fourierdlem23 40827 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275267, 274eqeltrd 2892 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2766, 112syl 17 . . . . . . . . . 10 (𝜒𝐹:ℝ⟶ℝ)
277 ioossre 12456 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278277a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279 eqid 2813 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280 ioossre 12456 . . . . . . . . . . 11 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281280a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282233, 254ltned 10461 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283 fourierdlem76.l . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
2846, 223, 283syl2anc 575 . . . . . . . . . . 11 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
285260eqcomd 2819 . . . . . . . . . . . 12 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286285oveq2d 6893 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
287284, 286eleqtrd 2894 . . . . . . . . . 10 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
288211recnd 10356 . . . . . . . . . 10 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 40856 . . . . . . . . 9 (𝜒𝐿 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
29049, 54ffvelrnd 6585 . . . . . . . . 9 (𝜒 → (𝑆𝑗) ∈ ℝ)
291 elfzoelz 12697 . . . . . . . . . . . 12 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292 zre 11650 . . . . . . . . . . . 12 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
29352, 291, 2923syl 18 . . . . . . . . . . 11 (𝜒𝑗 ∈ ℝ)
294293ltp1d 11242 . . . . . . . . . 10 (𝜒𝑗 < (𝑗 + 1))
295 isorel 6803 . . . . . . . . . . 11 ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
29644, 54, 89, 295syl12anc 856 . . . . . . . . . 10 (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
297294, 296mpbid 223 . . . . . . . . 9 (𝜒 → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
2981simprbi 486 . . . . . . . . 9 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
299 eqid 2813 . . . . . . . . 9 if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300 eqid 2813 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300fourierdlem33 40837 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
302 eqidd 2814 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303 simpr 473 . . . . . . . . . . . 12 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304303oveq2d 6893 . . . . . . . . . . 11 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305304fveq2d 6415 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
306243adantr 468 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) ∈ ℝ*)
307245adantr 468 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
30890adantr 468 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
309193, 211, 290, 90, 297, 298fourierdlem10 40814 . . . . . . . . . . . . . 14 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310309simpld 484 . . . . . . . . . . . . 13 (𝜒 → (𝑄𝑖) ≤ (𝑆𝑗))
311193, 290, 90, 310, 297lelttrd 10483 . . . . . . . . . . . 12 (𝜒 → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
312311adantr 468 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
313211adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
314309simprd 485 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
315314adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
316 neqne 2993 . . . . . . . . . . . . . 14 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317316necomd 3040 . . . . . . . . . . . . 13 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318317adantl 469 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319308, 313, 315, 318leneltd 10479 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320306, 307, 308, 312, 319eliood 40205 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
321230, 90readdcld 10357 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322276, 321ffvelrnd 6585 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323322adantr 468 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324302, 305, 320, 323fvmptd 6512 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325324ifeq2da 4317 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326298resmptd 5664 . . . . . . . . 9 (𝜒 → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327326oveq1d 6892 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
328301, 325, 3273eltr3d 2906 . . . . . . 7 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
329 ax-resscn 10281 . . . . . . . . 9 ℝ ⊆ ℂ
330128, 329syl6ss 3817 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
33190recnd 10356 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332168, 330, 124, 331constlimc 40337 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆‘(𝑗 + 1))))
333167, 168, 161, 121, 125, 328, 332sublimc 40365 . . . . . 6 (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆‘(𝑗 + 1))))
334330, 162, 331idlimc 40339 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆‘(𝑗 + 1))))
3356, 105jca 503 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336 eleq1 2880 . . . . . . . . . 10 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337336anbi2d 616 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338 neeq1 3047 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339337, 338imbi12d 335 . . . . . . . 8 (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340339, 140vtoclg 3466 . . . . . . 7 ((𝑆‘(𝑗 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0))
34190, 335, 340sylc 65 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ≠ 0)
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 40369 . . . . 5 (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆‘(𝑗 + 1))))
343 eqid 2813 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344143, 150mulcld 10348 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345159neneqd 2990 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346 2re 11377 . . . . . . . . . . 11 2 ∈ ℝ
347346a1i 11 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
34817rehalfcld 11549 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349348resincld 15096 . . . . . . . . . . 11 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350349adantl 469 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351347, 350remulcld 10358 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352 elsng 4391 . . . . . . . . 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 316 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355344, 354eldifd 3787 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356 eqid 2813 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357 eqid 2813 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358 2cnd 11380 . . . . . . . 8 (𝜒 → 2 ∈ ℂ)
359356, 330, 358, 331constlimc 40337 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆‘(𝑗 + 1))))
360348ad2antrl 710 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361 recn 10314 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362361sincld 15083 . . . . . . . . 9 (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363362adantl 469 . . . . . . . 8 ((𝜒𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364 eqid 2813 . . . . . . . . 9 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365 2cn 11378 . . . . . . . . . . 11 2 ∈ ℂ
366 eldifsn 4515 . . . . . . . . . . 11 (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367365, 151, 366mpbir2an 693 . . . . . . . . . 10 2 ∈ (ℂ ∖ {0})
368367a1i 11 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ (ℂ ∖ {0}))
369151a1i 11 . . . . . . . . 9 (𝜒 → 2 ≠ 0)
370162, 356, 364, 148, 368, 334, 359, 369, 152divlimc 40369 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆‘(𝑗 + 1))))
371 sinf 15077 . . . . . . . . . . . . . 14 sin:ℂ⟶ℂ
372371a1i 11 . . . . . . . . . . . . 13 (⊤ → sin:ℂ⟶ℂ)
373329a1i 11 . . . . . . . . . . . . 13 (⊤ → ℝ ⊆ ℂ)
374372, 373feqresmpt 6474 . . . . . . . . . . . 12 (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375374mptru 1645 . . . . . . . . . . 11 (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376 resincncf 40569 . . . . . . . . . . 11 (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377375, 376eqeltrri 2889 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378377a1i 11 . . . . . . . . 9 (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
37990rehalfcld 11549 . . . . . . . . 9 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380 fveq2 6411 . . . . . . . . 9 (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381378, 379, 380cnmptlimc 23874 . . . . . . . 8 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆‘(𝑗 + 1)) / 2)))
382 fveq2 6411 . . . . . . . 8 (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383 fveq2 6411 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384383ad2antll 711 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385360, 363, 370, 381, 382, 384limcco 23877 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆‘(𝑗 + 1))))
386356, 357, 343, 143, 150, 359, 385mullimc 40329 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆‘(𝑗 + 1))))
387331halfcld 11547 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388387sincld 15083 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389154, 105sseldd 3806 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390 fourierdlem44 40848 . . . . . . . 8 (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391389, 341, 390syl2anc 575 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392358, 388, 369, 391mulne0d 10967 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 40369 . . . . 5 (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆‘(𝑗 + 1))))
3942, 3, 4, 142, 160, 342, 393mullimc 40329 . . . 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 5600 . . . . . 6 (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
399 ioossicc 12480 . . . . . . . 8 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1)))
400 iccss 12462 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
40119, 98, 85, 107, 400syl22anc 858 . . . . . . . 8 (𝜒 → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402399, 401syl5ss 3816 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403402resmptd 5664 . . . . . 6 (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404398, 403syl5eq 2859 . . . . 5 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405404oveq1d 6892 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆‘(𝑗 + 1))))
406394, 396, 4053eltr4d 2907 . . 3 (𝜒𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
4071, 406sylbir 226 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
408242, 249gtned 10460 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄𝑖))
409 fourierdlem76.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
4106, 223, 409syl2anc 575 . . . . . . . . . . 11 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
411240oveq2d 6893 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
412410, 411eleqtrd 2894 . . . . . . . . . 10 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
413193recnd 10356 . . . . . . . . . 10 (𝜒 → (𝑄𝑖) ∈ ℂ)
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 40856 . . . . . . . . 9 (𝜒𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄𝑖)))
415 eqid 2813 . . . . . . . . 9 if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)))
416 eqid 2813 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
417193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416fourierdlem32 40836 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
418 eqidd 2814 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419 oveq2 6885 . . . . . . . . . . . 12 (𝑠 = (𝑆𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆𝑗)))
420419fveq2d 6415 . . . . . . . . . . 11 (𝑠 = (𝑆𝑗) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
421420adantl 469 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) ∧ 𝑠 = (𝑆𝑗)) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
422243adantr 468 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ*)
423245adantr 468 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
424290adantr 468 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ℝ)
425193adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ)
426310adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ≤ (𝑆𝑗))
427 neqne 2993 . . . . . . . . . . . . 13 (¬ (𝑆𝑗) = (𝑄𝑖) → (𝑆𝑗) ≠ (𝑄𝑖))
428427adantl 469 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ≠ (𝑄𝑖))
429425, 424, 426, 428leneltd 10479 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) < (𝑆𝑗))
43090adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431211adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432297adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
433314adantr 468 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434424, 430, 431, 432, 433ltletrd 10485 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑄‘(𝑖 + 1)))
435422, 423, 424, 429, 434eliood 40205 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
436230, 290readdcld 10357 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆𝑗)) ∈ ℝ)
437276, 436ffvelrnd 6585 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
438437adantr 468 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
439418, 421, 435, 438fvmptd 6512 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)) = (𝐹‘(𝑋 + (𝑆𝑗))))
440439ifeq2da 4317 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))))
441326oveq1d 6892 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
442417, 440, 4413eltr3d 2906 . . . . . . 7 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
443290recnd 10356 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ ℂ)
444168, 330, 124, 443constlimc 40337 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆𝑗)))
445167, 168, 161, 121, 125, 442, 444sublimc 40365 . . . . . 6 (𝜒 → (if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆𝑗)))
446330, 162, 443idlimc 40339 . . . . . 6 (𝜒 → (𝑆𝑗) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆𝑗)))
4476, 83jca 503 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
448 eleq1 2880 . . . . . . . . . 10 (𝑠 = (𝑆𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
449448anbi2d 616 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵))))
450 neeq1 3047 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → (𝑠 ≠ 0 ↔ (𝑆𝑗) ≠ 0))
451449, 450imbi12d 335 . . . . . . . 8 (𝑠 = (𝑆𝑗) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0)))
452451, 140vtoclg 3466 . . . . . . 7 ((𝑆𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0))
45383, 447, 452sylc 65 . . . . . 6 (𝜒 → (𝑆𝑗) ≠ 0)
454161, 162, 2, 126, 166, 445, 446, 453, 141divlimc 40369 . . . . 5 (𝜒 → ((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆𝑗)))
455356, 330, 358, 443constlimc 40337 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆𝑗)))
456348ad2antrl 710 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457162, 356, 364, 148, 368, 446, 455, 369, 152divlimc 40369 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆𝑗)))
458290rehalfcld 11549 . . . . . . . . 9 (𝜒 → ((𝑆𝑗) / 2) ∈ ℝ)
459 fveq2 6411 . . . . . . . . 9 (𝑥 = ((𝑆𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆𝑗) / 2)))
460378, 458, 459cnmptlimc 23874 . . . . . . . 8 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆𝑗) / 2)))
461 fveq2 6411 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
462461ad2antll 711 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
463456, 363, 457, 460, 382, 462limcco 23877 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆𝑗)))
464356, 357, 343, 143, 150, 455, 463mullimc 40329 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆𝑗)))
465443halfcld 11547 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ℂ)
466465sincld 15083 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ℂ)
467154, 83sseldd 3806 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ (-π[,]π))
468 fourierdlem44 40848 . . . . . . . 8 (((𝑆𝑗) ∈ (-π[,]π) ∧ (𝑆𝑗) ≠ 0) → (sin‘((𝑆𝑗) / 2)) ≠ 0)
469467, 453, 468syl2anc 575 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ≠ 0)
470358, 466, 369, 469mulne0d 10967 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ≠ 0)
471162, 343, 3, 148, 355, 446, 464, 470, 159divlimc 40369 . . . . 5 (𝜒 → ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆𝑗)))
4722, 3, 4, 142, 160, 454, 471mullimc 40329 . . . 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 6892 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆𝑗)))
476472, 474, 4753eltr4d 2907 . . 3 (𝜒𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
4771, 476sylbir 226 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
478298sselda 3805 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
479478, 266syldan 581 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480479mpteq2dva 4945 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481225adantr 468 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) ∈ ℝ*)
482228adantr 468 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
483230adantr 468 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484483, 129readdcld 10357 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485240adantr 468 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
486193adantr 468 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ)
487243adantr 468 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ*)
488245adantr 468 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
489487, 488, 478, 248syl3anc 1483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) < 𝑠)
490486, 18, 483, 489ltadd2dd 10484 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
491485, 490eqbrtrd 4873 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
492211adantr 468 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493487, 488, 478, 253syl3anc 1483 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
49418, 492, 483, 493ltadd2dd 10484 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495260adantr 468 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496494, 495breqtrd 4877 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497481, 482, 484, 491, 496eliood 40205 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
498269, 271, 330, 237, 497fourierdlem23 40827 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499480, 498eqeltrd 2892 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500 ssid 3827 . . . . . . . . 9 ℂ ⊆ ℂ
501500a1i 11 . . . . . . . 8 (𝜒 → ℂ ⊆ ℂ)
502330, 124, 501constcncfg 40565 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503499, 502subcncf 40563 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504166ralrimiva 3161 . . . . . . . 8 (𝜒 → ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505 dfss3 3794 . . . . . . . 8 (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506504, 505sylibr 225 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507 difssd 3944 . . . . . . 7 (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508506, 507idcncfg 40566 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509503, 508divcncf 23434 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510330, 501idcncfg 40566 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511355, 343fmptd 6609 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512330, 358, 501constcncfg 40565 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513 sincn 24418 . . . . . . . . . . 11 sin ∈ (ℂ–cn→ℂ)
514513a1i 11 . . . . . . . . . 10 (𝜒 → sin ∈ (ℂ–cn→ℂ))
515367a1i 11 . . . . . . . . . . . 12 (𝜒 → 2 ∈ (ℂ ∖ {0}))
516330, 515, 507constcncfg 40565 . . . . . . . . . . 11 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517510, 516divcncf 23434 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518514, 517cncfmpt1f 22933 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519512, 518mulcncf 23433 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520 cncffvrn 22918 . . . . . . . 8 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)) → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
521507, 519, 520syl2anc 575 . . . . . . 7 (𝜒 → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522511, 521mpbird 248 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523510, 522divcncf 23434 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524509, 523mulcncf 23433 . . . 4 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525404, 524eqeltrd 2892 . . 3 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
5261, 525sylbir 226 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527407, 477, 526jca31 506 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 197  wa 384   = wceq 1637  wtru 1638  wcel 2157  wne 2985  wral 3103  {crab 3107  cdif 3773  cun 3774  cin 3775  wss 3776  ifcif 4286  {csn 4377  {cpr 4379   class class class wbr 4851  cmpt 4930  dom cdm 5318  ran crn 5319  cres 5320  cio 6065  Fun wfun 6098  wf 6100  1-1-ontowf1o 6103  cfv 6104   Isom wiso 6105  (class class class)co 6877  𝑚 cmap 8095  Fincfn 8195  cc 10222  cr 10223  0cc0 10224  1c1 10225   + caddc 10227   · cmul 10229  *cxr 10361   < clt 10362  cle 10363  cmin 10554  -cneg 10555   / cdiv 10972  cn 11308  2c2 11359  cz 11646  (,)cioo 12396  [,)cico 12398  [,]cicc 12399  ...cfz 12552  ..^cfzo 12692  chash 13340  sincsin 15017  πcpi 15020  t crest 16289  TopOpenctopn 16290  fldccnfld 19957  cnccncf 22896   lim climc 23846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302  ax-addf 10303  ax-mulf 10304
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-iin 4722  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-om 7299  df-1st 7401  df-2nd 7402  df-supp 7533  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-er 7982  df-map 8097  df-pm 8098  df-ixp 8149  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-fsupp 8518  df-fi 8559  df-sup 8590  df-inf 8591  df-oi 8657  df-card 9051  df-cda 9278  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-4 11369  df-5 11370  df-6 11371  df-7 11372  df-8 11373  df-9 11374  df-n0 11563  df-z 11647  df-dec 11763  df-uz 11908  df-q 12011  df-rp 12050  df-xneg 12165  df-xadd 12166  df-xmul 12167  df-ioo 12400  df-ioc 12401  df-ico 12402  df-icc 12403  df-fz 12553  df-fzo 12693  df-fl 12820  df-mod 12896  df-seq 13028  df-exp 13087  df-fac 13284  df-bc 13313  df-hash 13341  df-shft 14033  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-limsup 14428  df-clim 14445  df-rlim 14446  df-sum 14643  df-ef 15021  df-sin 15023  df-cos 15024  df-pi 15026  df-struct 16073  df-ndx 16074  df-slot 16075  df-base 16077  df-sets 16078  df-ress 16079  df-plusg 16169  df-mulr 16170  df-starv 16171  df-sca 16172  df-vsca 16173  df-ip 16174  df-tset 16175  df-ple 16176  df-ds 16178  df-unif 16179  df-hom 16180  df-cco 16181  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17954  df-cmn 18399  df-psmet 19949  df-xmet 19950  df-met 19951  df-bl 19952  df-mopn 19953  df-fbas 19954  df-fg 19955  df-cnfld 19958  df-top 20916  df-topon 20933  df-topsp 20955  df-bases 20968  df-cld 21041  df-ntr 21042  df-cls 21043  df-nei 21120  df-lp 21158  df-perf 21159  df-cn 21249  df-cnp 21250  df-haus 21337  df-tx 21583  df-hmeo 21776  df-fil 21867  df-fm 21959  df-flim 21960  df-flf 21961  df-xms 22342  df-ms 22343  df-tms 22344  df-cncf 22898  df-limc 23850  df-dv 23851
This theorem is referenced by:  fourierdlem86  40889
  Copyright terms: Public domain W3C validator