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 39732
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 2621 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3 eqid 2621 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4 eqid 2621 . . . . 5 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5 simplll 797 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
61, 5sylbi 207 . . . . . . . . . 10 (𝜒𝜑)
76adantr 481 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8 ioossicc 12209 . . . . . . . . . 10 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9 fourierdlem76.a . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ)
109rexrd 10041 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ*)
116, 10syl 17 . . . . . . . . . . . 12 (𝜒𝐴 ∈ ℝ*)
1211adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ*)
13 fourierdlem76.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℝ)
1413rexrd 10041 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ*)
156, 14syl 17 . . . . . . . . . . . 12 (𝜒𝐵 ∈ ℝ*)
1615adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ*)
17 elioore 12155 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
1817adantl 482 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
196, 9syl 17 . . . . . . . . . . . . 13 (𝜒𝐴 ∈ ℝ)
2019adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22 prfi 8187 . . . . . . . . . . . . . . . . . . . . 21 {𝐴, 𝐵} ∈ Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ∈ Fin)
24 fzfid 12720 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0...𝑀) ∈ Fin)
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2625rnmptfi 38856 . . . . . . . . . . . . . . . . . . . . 21 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27 infi 8136 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29 unfi 8179 . . . . . . . . . . . . . . . . . . . 20 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3023, 28, 29syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3121, 30syl5eqel 2702 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ Fin)
32 prssg 4323 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
339, 13, 32syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
349, 13, 33mpbi2and 955 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35 inss2 3817 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36 ioossre 12185 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴(,)𝐵) ⊆ ℝ
3735, 36sstri 3596 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
3934, 38unssd 3772 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
4021, 39syl5eqss 3633 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ ℝ)
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18 𝑁 = ((#‘𝑇) − 1)
4331, 40, 41, 42fourierdlem36 39693 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
446, 43syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑆 Isom < , < ((0...𝑁), 𝑇))
45 isof1o 6533 . . . . . . . . . . . . . . . 16 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
46 f1of 6099 . . . . . . . . . . . . . . . 16 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15 (𝜒𝑆:(0...𝑁)⟶𝑇)
486, 40syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑇 ⊆ ℝ)
4947, 48fssd 6019 . . . . . . . . . . . . . 14 (𝜒𝑆:(0...𝑁)⟶ℝ)
5049adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51 simpllr 798 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
521, 51sylbi 207 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (0..^𝑁))
53 elfzofz 12434 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
5452, 53syl 17 . . . . . . . . . . . . . 14 (𝜒𝑗 ∈ (0...𝑁))
5554adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
5650, 55ffvelrnd 6321 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ)
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑆:(0...𝑁)⟶𝑇)
58 frn 6015 . . . . . . . . . . . . . . . . . 18 (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆𝑇)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑆𝑇)
609leidd 10546 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐴)
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴 < 𝐵)
629, 13, 61ltled 10137 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐵)
639, 13, 9, 60, 62eliccd 39168 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐴[,]𝐵))
6413leidd 10546 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝐵)
659, 13, 13, 62, 64eliccd 39168 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (𝐴[,]𝐵))
66 prssg 4323 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
679, 13, 66syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
6863, 65, 67mpbi2and 955 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
6935, 8sstri 3596 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
7069a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
7168, 70unssd 3772 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
7221, 71syl5eqss 3633 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ⊆ (𝐴[,]𝐵))
7359, 72sstrd 3597 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
746, 73syl 17 . . . . . . . . . . . . . . 15 (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75 ffun 6010 . . . . . . . . . . . . . . . . 17 (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
7649, 75syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → Fun 𝑆)
77 fdm 6013 . . . . . . . . . . . . . . . . . . 19 (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom 𝑆 = (0...𝑁))
7978eqcomd 2627 . . . . . . . . . . . . . . . . 17 (𝜒 → (0...𝑁) = dom 𝑆)
8054, 79eleqtrd 2700 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ dom 𝑆)
81 fvelrn 6313 . . . . . . . . . . . . . . . 16 ((Fun 𝑆𝑗 ∈ dom 𝑆) → (𝑆𝑗) ∈ ran 𝑆)
8276, 80, 81syl2anc 692 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆𝑗) ∈ ran 𝑆)
8374, 82sseldd 3588 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ (𝐴[,]𝐵))
84 iccgelb 12180 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆𝑗))
8511, 15, 83, 84syl3anc 1323 . . . . . . . . . . . . 13 (𝜒𝐴 ≤ (𝑆𝑗))
8685adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆𝑗))
8756rexrd 10041 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ*)
88 fzofzp1 12514 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
8952, 88syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
9049, 89ffvelrnd 6321 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
9190rexrd 10041 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
9291adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
93 simpr 477 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
94 ioogtlb 39159 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9587, 92, 93, 94syl3anc 1323 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9620, 56, 18, 86, 95lelttrd 10147 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
9790adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
986, 13syl 17 . . . . . . . . . . . . 13 (𝜒𝐵 ∈ ℝ)
9998adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100 iooltub 39177 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10187, 92, 93, 100syl3anc 1323 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10289, 79eleqtrd 2700 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103 fvelrn 6313 . . . . . . . . . . . . . . . 16 ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10476, 102, 103syl2anc 692 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10574, 104sseldd 3588 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106 iccleub 12179 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10711, 15, 105, 106syl3anc 1323 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108107adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10918, 97, 99, 101, 108ltletrd 10149 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
11012, 16, 18, 96, 109eliood 39162 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
1118, 110sseldi 3585 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112 fourierdlem76.f . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶ℝ)
113112adantr 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114 fourierdlem76.xre . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
115114adantr 481 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
1169, 13iccssred 39169 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117116sselda 3587 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118115, 117readdcld 10021 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119113, 118ffvelrnd 6321 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
1207, 111, 119syl2anc 692 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121120recnd 10020 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122 fourierdlem76.c . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
123122recnd 10020 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1246, 123syl 17 . . . . . . . 8 (𝜒𝐶 ∈ ℂ)
125124adantr 481 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126121, 125subcld 10344 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127 ioossre 12185 . . . . . . . . 9 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128127a1i 11 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129128sselda 3587 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130129recnd 10020 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131 nne 2794 . . . . . . . . . . . 12 𝑠 ≠ 0 ↔ 𝑠 = 0)
132131biimpi 206 . . . . . . . . . . 11 𝑠 ≠ 0 → 𝑠 = 0)
133132eqcomd 2627 . . . . . . . . . 10 𝑠 ≠ 0 → 0 = 𝑠)
134133adantl 482 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135 simpr 477 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136135adantr 481 . . . . . . . . 9 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137134, 136eqeltrd 2698 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138 fourierdlem76.n0 . . . . . . . . 9 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139138ad2antrr 761 . . . . . . . 8 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140137, 139condan 834 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
1417, 111, 140syl2anc 692 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142126, 130, 141divcld 10753 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143 2cnd 11045 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144130halfcld 11229 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145144sincld 14796 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146143, 145mulcld 10012 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
14717recnd 10020 . . . . . . . . . 10 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148147adantl 482 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149148halfcld 11229 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150149sincld 14796 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151 2ne0 11065 . . . . . . . 8 2 ≠ 0
152151a1i 11 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153 fourierdlem76.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
1546, 153syl 17 . . . . . . . . . 10 (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155154adantr 481 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156155, 111sseldd 3588 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157 fourierdlem44 39701 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158156, 141, 157syl2anc 692 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159143, 150, 152, 158mulne0d 10631 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160130, 146, 159divcld 10753 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161 eqid 2621 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162 eqid 2621 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163141neneqd 2795 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164 velsn 4169 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
165163, 164sylnibr 319 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166130, 165eldifd 3570 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167 eqid 2621 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168 eqid 2621 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169 elfzofz 12434 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171 pire 24131 . . . . . . . . . . . . . . . . . . . . 21 π ∈ ℝ
172171renegcli 10294 . . . . . . . . . . . . . . . . . . . 20 -π ∈ ℝ
173172a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -π ∈ ℝ)
174173, 114readdcld 10021 . . . . . . . . . . . . . . . . . 18 (𝜑 → (-π + 𝑋) ∈ ℝ)
175171a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → π ∈ ℝ)
176175, 114readdcld 10021 . . . . . . . . . . . . . . . . . 18 (𝜑 → (π + 𝑋) ∈ ℝ)
177174, 176iccssred 39169 . . . . . . . . . . . . . . . . 17 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178177adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℕ)
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19 (𝜑𝑉 ∈ (𝑃𝑀))
182179, 180, 181fourierdlem15 39672 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183182adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184183, 170ffvelrnd 6321 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185178, 184sseldd 3588 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
186114adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187185, 186resubcld 10410 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
18825fvmpt2 6253 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
189170, 187, 188syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
190189, 187eqeltrd 2698 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
191190adantlr 750 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
192191adantr 481 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
1931, 192sylbi 207 . . . . . . . . 9 (𝜒 → (𝑄𝑖) ∈ ℝ)
194 fveq2 6153 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
195194oveq1d 6625 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
196195cbvmptv 4715 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
19725, 196eqtri 2643 . . . . . . . . . . . . . . 15 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
198197a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
199 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
200199oveq1d 6625 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201200adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202 fzofzp1 12514 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203202adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204183, 203ffvelrnd 6321 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205178, 204sseldd 3588 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206205, 186resubcld 10410 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207198, 201, 203, 206fvmptd 6250 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208207, 206eqeltrd 2698 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208adantlr 750 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210209adantr 481 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2111, 210sylbi 207 . . . . . . . . 9 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212179fourierdlem2 39659 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
213180, 212syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
214181, 213mpbid 222 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
215214simprrd 796 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
216215r19.21bi 2927 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
217185, 205, 186, 216ltsub1dd 10591 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218217, 189, 2073brtr4d 4650 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
219218adantlr 750 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
220219adantr 481 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2211, 220sylbi 207 . . . . . . . . 9 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2221biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝜒 → (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
223222simplrd 792 . . . . . . . . . . . . . . . . 17 (𝜒𝑖 ∈ (0..^𝑀))
2246, 223, 185syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) ∈ ℝ)
225224rexrd 10041 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ∈ ℝ*)
226225adantr 481 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2276, 223, 205syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228227rexrd 10041 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
229228adantr 481 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
2306, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑋 ∈ ℝ)
231230adantr 481 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232 elioore 12155 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233232adantl 482 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234231, 233readdcld 10021 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
2356, 223, 189syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
236235oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
237230recnd 10020 . . . . . . . . . . . . . . . . . 18 (𝜒𝑋 ∈ ℂ)
238224recnd 10020 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉𝑖) ∈ ℂ)
239237, 238pncan3d 10347 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
240236, 239eqtr2d 2656 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
241240adantr 481 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
242193adantr 481 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
243193rexrd 10041 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) ∈ ℝ*)
244243adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
245211rexrd 10041 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246245adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
247 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
248 ioogtlb 39159 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
249244, 246, 247, 248syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
250242, 233, 231, 249ltadd2dd 10148 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
251241, 250eqbrtrd 4640 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
252211adantr 481 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253 iooltub 39177 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254244, 246, 247, 253syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255233, 252, 231, 254ltadd2dd 10148 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
2566, 223, 207syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257256oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258227recnd 10020 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259237, 258pncan3d 10347 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260257, 259eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261260adantr 481 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262255, 261breqtrd 4644 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263226, 229, 234, 251, 262eliood 39162 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
264 fvres 6169 . . . . . . . . . . . . 13 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265263, 264syl 17 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266265eqcomd 2627 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267266mpteq2dva 4709 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268 ioosscn 39158 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269268a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270 fourierdlem76.fcn . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
2716, 223, 270syl2anc 692 . . . . . . . . . . 11 (𝜒 → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272 ioosscn 39158 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273272a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274269, 271, 273, 237, 263fourierdlem23 39680 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275267, 274eqeltrd 2698 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2766, 112syl 17 . . . . . . . . . 10 (𝜒𝐹:ℝ⟶ℝ)
277 ioossre 12185 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278277a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279 eqid 2621 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280 ioossre 12185 . . . . . . . . . . 11 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281280a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282233, 254ltned 10125 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283 fourierdlem76.l . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
2846, 223, 283syl2anc 692 . . . . . . . . . . 11 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
285260eqcomd 2627 . . . . . . . . . . . 12 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286285oveq2d 6626 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
287284, 286eleqtrd 2700 . . . . . . . . . 10 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
288211recnd 10020 . . . . . . . . . 10 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 39709 . . . . . . . . 9 (𝜒𝐿 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
29049, 54ffvelrnd 6321 . . . . . . . . 9 (𝜒 → (𝑆𝑗) ∈ ℝ)
291 elfzoelz 12419 . . . . . . . . . . . 12 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292 zre 11333 . . . . . . . . . . . 12 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
29352, 291, 2923syl 18 . . . . . . . . . . 11 (𝜒𝑗 ∈ ℝ)
294293ltp1d 10906 . . . . . . . . . 10 (𝜒𝑗 < (𝑗 + 1))
295 isorel 6536 . . . . . . . . . . 11 ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
29644, 54, 89, 295syl12anc 1321 . . . . . . . . . 10 (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
297294, 296mpbid 222 . . . . . . . . 9 (𝜒 → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
2981simprbi 480 . . . . . . . . 9 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
299 eqid 2621 . . . . . . . . 9 if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300 eqid 2621 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300fourierdlem33 39690 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
302 eqidd 2622 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303 simpr 477 . . . . . . . . . . . 12 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304303oveq2d 6626 . . . . . . . . . . 11 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305304fveq2d 6157 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
306243adantr 481 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) ∈ ℝ*)
307245adantr 481 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
30890adantr 481 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
309193, 211, 290, 90, 297, 298fourierdlem10 39667 . . . . . . . . . . . . . 14 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310309simpld 475 . . . . . . . . . . . . 13 (𝜒 → (𝑄𝑖) ≤ (𝑆𝑗))
311193, 290, 90, 310, 297lelttrd 10147 . . . . . . . . . . . 12 (𝜒 → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
312311adantr 481 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄𝑖) < (𝑆‘(𝑗 + 1)))
313211adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
314309simprd 479 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
315314adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
316 neqne 2798 . . . . . . . . . . . . . 14 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317316necomd 2845 . . . . . . . . . . . . 13 (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318317adantl 482 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319308, 313, 315, 318leneltd 10143 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320306, 307, 308, 312, 319eliood 39162 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
321230, 90readdcld 10021 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322276, 321ffvelrnd 6321 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323322adantr 481 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324302, 305, 320, 323fvmptd 6250 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325324ifeq2da 4094 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326298resmptd 5416 . . . . . . . . 9 (𝜒 → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327326oveq1d 6625 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
328301, 325, 3273eltr3d 2712 . . . . . . 7 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
329 ax-resscn 9945 . . . . . . . . 9 ℝ ⊆ ℂ
330128, 329syl6ss 3599 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
33190recnd 10020 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332168, 330, 124, 331constlimc 39288 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆‘(𝑗 + 1))))
333167, 168, 161, 121, 125, 328, 332sublimc 39316 . . . . . 6 (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆‘(𝑗 + 1))))
334330, 162, 331idlimc 39290 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆‘(𝑗 + 1))))
3356, 105jca 554 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336 eleq1 2686 . . . . . . . . . 10 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337336anbi2d 739 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338 neeq1 2852 . . . . . . . . 9 (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339337, 338imbi12d 334 . . . . . . . 8 (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340339, 140vtoclg 3255 . . . . . . 7 ((𝑆‘(𝑗 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0))
34190, 335, 340sylc 65 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ≠ 0)
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 39320 . . . . 5 (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆‘(𝑗 + 1))))
343 eqid 2621 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344143, 150mulcld 10012 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345159neneqd 2795 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346 2re 11042 . . . . . . . . . . 11 2 ∈ ℝ
347346a1i 11 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
34817rehalfcld 11231 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349348resincld 14809 . . . . . . . . . . 11 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350349adantl 482 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351347, 350remulcld 10022 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352 elsng 4167 . . . . . . . . 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 315 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355344, 354eldifd 3570 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356 eqid 2621 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357 eqid 2621 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358 2cnd 11045 . . . . . . . 8 (𝜒 → 2 ∈ ℂ)
359356, 330, 358, 331constlimc 39288 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆‘(𝑗 + 1))))
360348ad2antrl 763 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361 recn 9978 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362361sincld 14796 . . . . . . . . 9 (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363362adantl 482 . . . . . . . 8 ((𝜒𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364 eqid 2621 . . . . . . . . 9 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365 2cn 11043 . . . . . . . . . . 11 2 ∈ ℂ
366 eldifsn 4292 . . . . . . . . . . 11 (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367365, 151, 366mpbir2an 954 . . . . . . . . . 10 2 ∈ (ℂ ∖ {0})
368367a1i 11 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ (ℂ ∖ {0}))
369151a1i 11 . . . . . . . . 9 (𝜒 → 2 ≠ 0)
370162, 356, 364, 148, 368, 334, 359, 369, 152divlimc 39320 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆‘(𝑗 + 1))))
371 sinf 14790 . . . . . . . . . . . . . 14 sin:ℂ⟶ℂ
372371a1i 11 . . . . . . . . . . . . 13 (⊤ → sin:ℂ⟶ℂ)
373329a1i 11 . . . . . . . . . . . . 13 (⊤ → ℝ ⊆ ℂ)
374372, 373feqresmpt 6212 . . . . . . . . . . . 12 (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375374trud 1490 . . . . . . . . . . 11 (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376 resincncf 39419 . . . . . . . . . . 11 (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377375, 376eqeltrri 2695 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378377a1i 11 . . . . . . . . 9 (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
37990rehalfcld 11231 . . . . . . . . 9 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380 fveq2 6153 . . . . . . . . 9 (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381378, 379, 380cnmptlimc 23577 . . . . . . . 8 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆‘(𝑗 + 1)) / 2)))
382 fveq2 6153 . . . . . . . 8 (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383 fveq2 6153 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384383ad2antll 764 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385360, 363, 370, 381, 382, 384limcco 23580 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆‘(𝑗 + 1))))
386356, 357, 343, 143, 150, 359, 385mullimc 39280 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆‘(𝑗 + 1))))
387331halfcld 11229 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388387sincld 14796 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389154, 105sseldd 3588 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390 fourierdlem44 39701 . . . . . . . 8 (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391389, 341, 390syl2anc 692 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392358, 388, 369, 391mulne0d 10631 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 39320 . . . . 5 (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆‘(𝑗 + 1))))
3942, 3, 4, 142, 160, 342, 393mullimc 39280 . . . 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 5357 . . . . . 6 (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
399 ioossicc 12209 . . . . . . . 8 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1)))
400 iccss 12191 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
40119, 98, 85, 107, 400syl22anc 1324 . . . . . . . 8 (𝜒 → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402399, 401syl5ss 3598 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403402resmptd 5416 . . . . . 6 (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404398, 403syl5eq 2667 . . . . 5 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405404oveq1d 6625 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆‘(𝑗 + 1))))
406394, 396, 4053eltr4d 2713 . . 3 (𝜒𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
4071, 406sylbir 225 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
408242, 249gtned 10124 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄𝑖))
409 fourierdlem76.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
4106, 223, 409syl2anc 692 . . . . . . . . . . 11 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
411240oveq2d 6626 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
412410, 411eleqtrd 2700 . . . . . . . . . 10 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
413193recnd 10020 . . . . . . . . . 10 (𝜒 → (𝑄𝑖) ∈ ℂ)
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 39709 . . . . . . . . 9 (𝜒𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄𝑖)))
415 eqid 2621 . . . . . . . . 9 if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)))
416 eqid 2621 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂfld) ↾t ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
417193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416fourierdlem32 39689 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
418 eqidd 2622 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419 oveq2 6618 . . . . . . . . . . . 12 (𝑠 = (𝑆𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆𝑗)))
420419fveq2d 6157 . . . . . . . . . . 11 (𝑠 = (𝑆𝑗) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
421420adantl 482 . . . . . . . . . 10 (((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) ∧ 𝑠 = (𝑆𝑗)) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆𝑗))))
422243adantr 481 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ*)
423245adantr 481 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
424290adantr 481 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ℝ)
425193adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ∈ ℝ)
426310adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) ≤ (𝑆𝑗))
427 neqne 2798 . . . . . . . . . . . . 13 (¬ (𝑆𝑗) = (𝑄𝑖) → (𝑆𝑗) ≠ (𝑄𝑖))
428427adantl 482 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ≠ (𝑄𝑖))
429425, 424, 426, 428leneltd 10143 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) < (𝑆𝑗))
43090adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431211adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432297adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
433314adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434424, 430, 431, 432, 433ltletrd 10149 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑄‘(𝑖 + 1)))
435422, 423, 424, 429, 434eliood 39162 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
436230, 290readdcld 10021 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆𝑗)) ∈ ℝ)
437276, 436ffvelrnd 6321 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
438437adantr 481 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
439418, 421, 435, 438fvmptd 6250 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)) = (𝐹‘(𝑋 + (𝑆𝑗))))
440439ifeq2da 4094 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))))
441326oveq1d 6625 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
442417, 440, 4413eltr3d 2712 . . . . . . 7 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
443290recnd 10020 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ ℂ)
444168, 330, 124, 443constlimc 39288 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆𝑗)))
445167, 168, 161, 121, 125, 442, 444sublimc 39316 . . . . . 6 (𝜒 → (if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆𝑗)))
446330, 162, 443idlimc 39290 . . . . . 6 (𝜒 → (𝑆𝑗) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim (𝑆𝑗)))
4476, 83jca 554 . . . . . . 7 (𝜒 → (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
448 eleq1 2686 . . . . . . . . . 10 (𝑠 = (𝑆𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆𝑗) ∈ (𝐴[,]𝐵)))
449448anbi2d 739 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → ((𝜑𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵))))
450 neeq1 2852 . . . . . . . . 9 (𝑠 = (𝑆𝑗) → (𝑠 ≠ 0 ↔ (𝑆𝑗) ≠ 0))
451449, 450imbi12d 334 . . . . . . . 8 (𝑠 = (𝑆𝑗) → (((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0)))
452451, 140vtoclg 3255 . . . . . . 7 ((𝑆𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0))
45383, 447, 452sylc 65 . . . . . 6 (𝜒 → (𝑆𝑗) ≠ 0)
454161, 162, 2, 126, 166, 445, 446, 453, 141divlimc 39320 . . . . 5 (𝜒 → ((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆𝑗)))
455356, 330, 358, 443constlimc 39288 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆𝑗)))
456348ad2antrl 763 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457162, 356, 364, 148, 368, 446, 455, 369, 152divlimc 39320 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆𝑗)))
458290rehalfcld 11231 . . . . . . . . 9 (𝜒 → ((𝑆𝑗) / 2) ∈ ℝ)
459 fveq2 6153 . . . . . . . . 9 (𝑥 = ((𝑆𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆𝑗) / 2)))
460378, 458, 459cnmptlimc 23577 . . . . . . . 8 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆𝑗) / 2)))
461 fveq2 6153 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
462461ad2antll 764 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
463456, 363, 457, 460, 382, 462limcco 23580 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆𝑗)))
464356, 357, 343, 143, 150, 455, 463mullimc 39280 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆𝑗)))
465443halfcld 11229 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ℂ)
466465sincld 14796 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ℂ)
467154, 83sseldd 3588 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ (-π[,]π))
468 fourierdlem44 39701 . . . . . . . 8 (((𝑆𝑗) ∈ (-π[,]π) ∧ (𝑆𝑗) ≠ 0) → (sin‘((𝑆𝑗) / 2)) ≠ 0)
469467, 453, 468syl2anc 692 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ≠ 0)
470358, 466, 369, 469mulne0d 10631 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ≠ 0)
471162, 343, 3, 148, 355, 446, 464, 470, 159divlimc 39320 . . . . 5 (𝜒 → ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆𝑗)))
4722, 3, 4, 142, 160, 454, 471mullimc 39280 . . . 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 6625 . . . 4 (𝜒 → ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim (𝑆𝑗)))
476472, 474, 4753eltr4d 2713 . . 3 (𝜒𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
4771, 476sylbir 225 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
478298sselda 3587 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
479478, 266syldan 487 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480479mpteq2dva 4709 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481225adantr 481 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) ∈ ℝ*)
482228adantr 481 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
483230adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484483, 129readdcld 10021 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485240adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
486193adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ)
487243adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) ∈ ℝ*)
488245adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
489487, 488, 478, 248syl3anc 1323 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄𝑖) < 𝑠)
490486, 18, 483, 489ltadd2dd 10148 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
491485, 490eqbrtrd 4640 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
492211adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493487, 488, 478, 253syl3anc 1323 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
49418, 492, 483, 493ltadd2dd 10148 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495260adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496494, 495breqtrd 4644 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497481, 482, 484, 491, 496eliood 39162 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
498269, 271, 330, 237, 497fourierdlem23 39680 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499480, 498eqeltrd 2698 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500 ssid 3608 . . . . . . . . 9 ℂ ⊆ ℂ
501500a1i 11 . . . . . . . 8 (𝜒 → ℂ ⊆ ℂ)
502330, 124, 501constcncfg 39415 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503499, 502subcncf 39413 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504166ralrimiva 2961 . . . . . . . 8 (𝜒 → ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505 dfss3 3577 . . . . . . . 8 (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506504, 505sylibr 224 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507 difssd 3721 . . . . . . 7 (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508506, 507idcncfg 39416 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509503, 508divcncf 23139 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510330, 501idcncfg 39416 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511355, 343fmptd 6346 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512330, 358, 501constcncfg 39415 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513 sincn 24119 . . . . . . . . . . 11 sin ∈ (ℂ–cn→ℂ)
514513a1i 11 . . . . . . . . . 10 (𝜒 → sin ∈ (ℂ–cn→ℂ))
515367a1i 11 . . . . . . . . . . . 12 (𝜒 → 2 ∈ (ℂ ∖ {0}))
516330, 515, 507constcncfg 39415 . . . . . . . . . . 11 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517510, 516divcncf 23139 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518514, 517cncfmpt1f 22639 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519512, 518mulcncf 23138 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520 cncffvrn 22624 . . . . . . . 8 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)) → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
521507, 519, 520syl2anc 692 . . . . . . 7 (𝜒 → ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522511, 521mpbird 247 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523510, 522divcncf 23139 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524509, 523mulcncf 23138 . . . 4 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525404, 524eqeltrd 2698 . . 3 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
5261, 525sylbir 225 . 2 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527407, 477, 526jca31 556 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 196  wa 384   = wceq 1480  wtru 1481  wcel 1987  wne 2790  wral 2907  {crab 2911  cdif 3556  cun 3557  cin 3558  wss 3559  ifcif 4063  {csn 4153  {cpr 4155   class class class wbr 4618  cmpt 4678  dom cdm 5079  ran crn 5080  cres 5081  cio 5813  Fun wfun 5846  wf 5848  1-1-ontowf1o 5851  cfv 5852   Isom wiso 5853  (class class class)co 6610  𝑚 cmap 7809  Fincfn 7907  cc 9886  cr 9887  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893  *cxr 10025   < clt 10026  cle 10027  cmin 10218  -cneg 10219   / cdiv 10636  cn 10972  2c2 11022  cz 11329  (,)cioo 12125  [,)cico 12127  [,]cicc 12128  ...cfz 12276  ..^cfzo 12414  #chash 13065  sincsin 14730  πcpi 14733  t crest 16013  TopOpenctopn 16014  fldccnfld 19678  cnccncf 22602   lim climc 23549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966  ax-addf 9967  ax-mulf 9968
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7861  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fsupp 8228  df-fi 8269  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-z 11330  df-dec 11446  df-uz 11640  df-q 11741  df-rp 11785  df-xneg 11898  df-xadd 11899  df-xmul 11900  df-ioo 12129  df-ioc 12130  df-ico 12131  df-icc 12132  df-fz 12277  df-fzo 12415  df-fl 12541  df-mod 12617  df-seq 12750  df-exp 12809  df-fac 13009  df-bc 13038  df-hash 13066  df-shft 13749  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-limsup 14144  df-clim 14161  df-rlim 14162  df-sum 14359  df-ef 14734  df-sin 14736  df-cos 14737  df-pi 14739  df-struct 15794  df-ndx 15795  df-slot 15796  df-base 15797  df-sets 15798  df-ress 15799  df-plusg 15886  df-mulr 15887  df-starv 15888  df-sca 15889  df-vsca 15890  df-ip 15891  df-tset 15892  df-ple 15893  df-ds 15896  df-unif 15897  df-hom 15898  df-cco 15899  df-rest 16015  df-topn 16016  df-0g 16034  df-gsum 16035  df-topgen 16036  df-pt 16037  df-prds 16040  df-xrs 16094  df-qtop 16099  df-imas 16100  df-xps 16102  df-mre 16178  df-mrc 16179  df-acs 16181  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-submnd 17268  df-mulg 17473  df-cntz 17682  df-cmn 18127  df-psmet 19670  df-xmet 19671  df-met 19672  df-bl 19673  df-mopn 19674  df-fbas 19675  df-fg 19676  df-cnfld 19679  df-top 20631  df-topon 20648  df-topsp 20661  df-bases 20674  df-cld 20746  df-ntr 20747  df-cls 20748  df-nei 20825  df-lp 20863  df-perf 20864  df-cn 20954  df-cnp 20955  df-haus 21042  df-tx 21288  df-hmeo 21481  df-fil 21573  df-fm 21665  df-flim 21666  df-flf 21667  df-xms 22048  df-ms 22049  df-tms 22050  df-cncf 22604  df-limc 23553  df-dv 23554
This theorem is referenced by:  fourierdlem86  39742
  Copyright terms: Public domain W3C validator