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 39736
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 12217 . . . . . . . . . 10 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9 fourierdlem76.a . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ)
109rexrd 10049 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ*)
116, 10syl 17 . . . . . . . . . . . 12 (𝜒𝐴 ∈ ℝ*)
1211adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ*)
13 fourierdlem76.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℝ)
1413rexrd 10049 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ*)
156, 14syl 17 . . . . . . . . . . . 12 (𝜒𝐵 ∈ ℝ*)
1615adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ*)
17 elioore 12163 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
1817adantl 482 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
196, 9syl 17 . . . . . . . . . . . . 13 (𝜒𝐴 ∈ ℝ)
2019adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22 prfi 8195 . . . . . . . . . . . . . . . . . . . . 21 {𝐴, 𝐵} ∈ Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ∈ Fin)
24 fzfid 12728 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0...𝑀) ∈ Fin)
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2625rnmptfi 38860 . . . . . . . . . . . . . . . . . . . . 21 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27 infi 8144 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29 unfi 8187 . . . . . . . . . . . . . . . . . . . 20 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3023, 28, 29syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
3121, 30syl5eqel 2702 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ Fin)
32 prssg 4325 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
339, 13, 32syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
349, 13, 33mpbi2and 955 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35 inss2 3818 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36 ioossre 12193 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴(,)𝐵) ⊆ ℝ
3735, 36sstri 3597 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
3934, 38unssd 3773 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
4021, 39syl5eqss 3634 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ ℝ)
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18 𝑁 = ((#‘𝑇) − 1)
4331, 40, 41, 42fourierdlem36 39697 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
446, 43syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑆 Isom < , < ((0...𝑁), 𝑇))
45 isof1o 6538 . . . . . . . . . . . . . . . 16 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
46 f1of 6104 . . . . . . . . . . . . . . . 16 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15 (𝜒𝑆:(0...𝑁)⟶𝑇)
486, 40syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑇 ⊆ ℝ)
4947, 48fssd 6024 . . . . . . . . . . . . . 14 (𝜒𝑆:(0...𝑁)⟶ℝ)
5049adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51 simpllr 798 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
521, 51sylbi 207 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (0..^𝑁))
53 elfzofz 12442 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
5452, 53syl 17 . . . . . . . . . . . . . 14 (𝜒𝑗 ∈ (0...𝑁))
5554adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
5650, 55ffvelrnd 6326 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ)
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑆:(0...𝑁)⟶𝑇)
58 frn 6020 . . . . . . . . . . . . . . . . . 18 (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆𝑇)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑆𝑇)
609leidd 10554 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐴)
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴 < 𝐵)
629, 13, 61ltled 10145 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝐵)
639, 13, 9, 60, 62eliccd 39172 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐴[,]𝐵))
6413leidd 10554 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝐵)
659, 13, 13, 62, 64eliccd 39172 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (𝐴[,]𝐵))
66 prssg 4325 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
679, 13, 66syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
6863, 65, 67mpbi2and 955 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
6935, 8sstri 3597 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
7069a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
7168, 70unssd 3773 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
7221, 71syl5eqss 3634 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ⊆ (𝐴[,]𝐵))
7359, 72sstrd 3598 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
746, 73syl 17 . . . . . . . . . . . . . . 15 (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75 ffun 6015 . . . . . . . . . . . . . . . . 17 (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
7649, 75syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → Fun 𝑆)
77 fdm 6018 . . . . . . . . . . . . . . . . . . 19 (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom 𝑆 = (0...𝑁))
7978eqcomd 2627 . . . . . . . . . . . . . . . . 17 (𝜒 → (0...𝑁) = dom 𝑆)
8054, 79eleqtrd 2700 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ dom 𝑆)
81 fvelrn 6318 . . . . . . . . . . . . . . . 16 ((Fun 𝑆𝑗 ∈ dom 𝑆) → (𝑆𝑗) ∈ ran 𝑆)
8276, 80, 81syl2anc 692 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆𝑗) ∈ ran 𝑆)
8374, 82sseldd 3589 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ (𝐴[,]𝐵))
84 iccgelb 12188 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆𝑗))
8511, 15, 83, 84syl3anc 1323 . . . . . . . . . . . . 13 (𝜒𝐴 ≤ (𝑆𝑗))
8685adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆𝑗))
8756rexrd 10049 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) ∈ ℝ*)
88 fzofzp1 12522 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
8952, 88syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
9049, 89ffvelrnd 6326 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
9190rexrd 10049 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
9291adantr 481 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
93 simpr 477 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
94 ioogtlb 39163 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9587, 92, 93, 94syl3anc 1323 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆𝑗) < 𝑠)
9620, 56, 18, 86, 95lelttrd 10155 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
9790adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
986, 13syl 17 . . . . . . . . . . . . 13 (𝜒𝐵 ∈ ℝ)
9998adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100 iooltub 39181 . . . . . . . . . . . . 13 (((𝑆𝑗) ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10187, 92, 93, 100syl3anc 1323 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
10289, 79eleqtrd 2700 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103 fvelrn 6318 . . . . . . . . . . . . . . . 16 ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10476, 102, 103syl2anc 692 . . . . . . . . . . . . . . 15 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
10574, 104sseldd 3589 . . . . . . . . . . . . . 14 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106 iccleub 12187 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10711, 15, 105, 106syl3anc 1323 . . . . . . . . . . . . 13 (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108107adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
10918, 97, 99, 101, 108ltletrd 10157 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
11012, 16, 18, 96, 109eliood 39166 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
1118, 110sseldi 3586 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112 fourierdlem76.f . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶ℝ)
113112adantr 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114 fourierdlem76.xre . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
115114adantr 481 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
1169, 13iccssred 39173 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117116sselda 3588 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118115, 117readdcld 10029 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119113, 118ffvelrnd 6326 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
1207, 111, 119syl2anc 692 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121120recnd 10028 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122 fourierdlem76.c . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
123122recnd 10028 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1246, 123syl 17 . . . . . . . 8 (𝜒𝐶 ∈ ℂ)
125124adantr 481 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126121, 125subcld 10352 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127 ioossre 12193 . . . . . . . . 9 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128127a1i 11 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129128sselda 3588 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130129recnd 10028 . . . . . 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 10761 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143 2cnd 11053 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144130halfcld 11237 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145144sincld 14804 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146143, 145mulcld 10020 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
14717recnd 10028 . . . . . . . . . 10 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148147adantl 482 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149148halfcld 11237 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150149sincld 14804 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151 2ne0 11073 . . . . . . . 8 2 ≠ 0
152151a1i 11 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153 fourierdlem76.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
1546, 153syl 17 . . . . . . . . . 10 (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155154adantr 481 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156155, 111sseldd 3589 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157 fourierdlem44 39705 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158156, 141, 157syl2anc 692 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159143, 150, 152, 158mulne0d 10639 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160130, 146, 159divcld 10761 . . . . 5 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161 eqid 2621 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162 eqid 2621 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163141neneqd 2795 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164 velsn 4171 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
165163, 164sylnibr 319 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166130, 165eldifd 3571 . . . . . 6 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167 eqid 2621 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168 eqid 2621 . . . . . . 7 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169 elfzofz 12442 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171 pire 24148 . . . . . . . . . . . . . . . . . . . . 21 π ∈ ℝ
172171renegcli 10302 . . . . . . . . . . . . . . . . . . . 20 -π ∈ ℝ
173172a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -π ∈ ℝ)
174173, 114readdcld 10029 . . . . . . . . . . . . . . . . . 18 (𝜑 → (-π + 𝑋) ∈ ℝ)
175171a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → π ∈ ℝ)
176175, 114readdcld 10029 . . . . . . . . . . . . . . . . . 18 (𝜑 → (π + 𝑋) ∈ ℝ)
177174, 176iccssred 39173 . . . . . . . . . . . . . . . . 17 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178177adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℕ)
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19 (𝜑𝑉 ∈ (𝑃𝑀))
182179, 180, 181fourierdlem15 39676 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183182adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184183, 170ffvelrnd 6326 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185178, 184sseldd 3589 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
186114adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187185, 186resubcld 10418 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
18825fvmpt2 6258 . . . . . . . . . . . . . 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 6158 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
195194oveq1d 6630 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
196195cbvmptv 4720 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
19725, 196eqtri 2643 . . . . . . . . . . . . . . 15 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
198197a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
199 fveq2 6158 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
200199oveq1d 6630 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201200adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202 fzofzp1 12522 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203202adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204183, 203ffvelrnd 6326 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205178, 204sseldd 3589 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206205, 186resubcld 10418 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207198, 201, 203, 206fvmptd 6255 . . . . . . . . . . . . 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 39663 . . . . . . . . . . . . . . . . . 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 2928 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
217185, 205, 186, 216ltsub1dd 10599 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218217, 189, 2073brtr4d 4655 . . . . . . . . . . . 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 10049 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ∈ ℝ*)
226225adantr 481 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2276, 223, 205syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228227rexrd 10049 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
229228adantr 481 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
2306, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑋 ∈ ℝ)
231230adantr 481 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232 elioore 12163 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233232adantl 482 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234231, 233readdcld 10029 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
2356, 223, 189syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
236235oveq2d 6631 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
237230recnd 10028 . . . . . . . . . . . . . . . . . 18 (𝜒𝑋 ∈ ℂ)
238224recnd 10028 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉𝑖) ∈ ℂ)
239237, 238pncan3d 10355 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
240236, 239eqtr2d 2656 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
241240adantr 481 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
242193adantr 481 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
243193rexrd 10049 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) ∈ ℝ*)
244243adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
245211rexrd 10049 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246245adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
247 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
248 ioogtlb 39163 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
249244, 246, 247, 248syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
250242, 233, 231, 249ltadd2dd 10156 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
251241, 250eqbrtrd 4645 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
252211adantr 481 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253 iooltub 39181 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254244, 246, 247, 253syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255233, 252, 231, 254ltadd2dd 10156 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
2566, 223, 207syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257256oveq2d 6631 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258227recnd 10028 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259237, 258pncan3d 10355 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260257, 259eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261260adantr 481 . . . . . . . . . . . . . . 15 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262255, 261breqtrd 4649 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263226, 229, 234, 251, 262eliood 39166 . . . . . . . . . . . . 13 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
264 fvres 6174 . . . . . . . . . . . . 13 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265263, 264syl 17 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266265eqcomd 2627 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267266mpteq2dva 4714 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268 ioosscn 39162 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269268a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270 fourierdlem76.fcn . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
2716, 223, 270syl2anc 692 . . . . . . . . . . 11 (𝜒 → (𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272 ioosscn 39162 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273272a1i 11 . . . . . . . . . . 11 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274269, 271, 273, 237, 263fourierdlem23 39684 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275267, 274eqeltrd 2698 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2766, 112syl 17 . . . . . . . . . 10 (𝜒𝐹:ℝ⟶ℝ)
277 ioossre 12193 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278277a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279 eqid 2621 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280 ioossre 12193 . . . . . . . . . . 11 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281280a1i 11 . . . . . . . . . 10 (𝜒 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282233, 254ltned 10133 . . . . . . . . . 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 6631 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
287284, 286eleqtrd 2700 . . . . . . . . . 10 (𝜒𝐿 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
288211recnd 10028 . . . . . . . . . 10 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 39713 . . . . . . . . 9 (𝜒𝐿 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
29049, 54ffvelrnd 6326 . . . . . . . . 9 (𝜒 → (𝑆𝑗) ∈ ℝ)
291 elfzoelz 12427 . . . . . . . . . . . 12 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292 zre 11341 . . . . . . . . . . . 12 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
29352, 291, 2923syl 18 . . . . . . . . . . 11 (𝜒𝑗 ∈ ℝ)
294293ltp1d 10914 . . . . . . . . . 10 (𝜒𝑗 < (𝑗 + 1))
295 isorel 6541 . . . . . . . . . . 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 39694 . . . . . . . 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 6631 . . . . . . . . . . 11 (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305304fveq2d 6162 . . . . . . . . . 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 39671 . . . . . . . . . . . . . 14 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310309simpld 475 . . . . . . . . . . . . 13 (𝜒 → (𝑄𝑖) ≤ (𝑆𝑗))
311193, 290, 90, 310, 297lelttrd 10155 . . . . . . . . . . . 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 10151 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320306, 307, 308, 312, 319eliood 39166 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
321230, 90readdcld 10029 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322276, 321ffvelrnd 6326 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323322adantr 481 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324302, 305, 320, 323fvmptd 6255 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325324ifeq2da 4095 . . . . . . . 8 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326298resmptd 5421 . . . . . . . . 9 (𝜒 → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327326oveq1d 6630 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
328301, 325, 3273eltr3d 2712 . . . . . . 7 (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆‘(𝑗 + 1))))
329 ax-resscn 9953 . . . . . . . . 9 ℝ ⊆ ℂ
330128, 329syl6ss 3600 . . . . . . . 8 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
33190recnd 10028 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332168, 330, 124, 331constlimc 39292 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆‘(𝑗 + 1))))
333167, 168, 161, 121, 125, 328, 332sublimc 39320 . . . . . 6 (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆‘(𝑗 + 1))))
334330, 162, 331idlimc 39294 . . . . . 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 3256 . . . . . . 7 ((𝑆‘(𝑗 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0))
34190, 335, 340sylc 65 . . . . . 6 (𝜒 → (𝑆‘(𝑗 + 1)) ≠ 0)
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 39324 . . . . 5 (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆‘(𝑗 + 1))))
343 eqid 2621 . . . . . 6 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344143, 150mulcld 10020 . . . . . . 7 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345159neneqd 2795 . . . . . . . 8 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346 2re 11050 . . . . . . . . . . 11 2 ∈ ℝ
347346a1i 11 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
34817rehalfcld 11239 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349348resincld 14817 . . . . . . . . . . 11 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350349adantl 482 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351347, 350remulcld 10030 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352 elsng 4169 . . . . . . . . 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 3571 . . . . . 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 11053 . . . . . . . 8 (𝜒 → 2 ∈ ℂ)
359356, 330, 358, 331constlimc 39292 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆‘(𝑗 + 1))))
360348ad2antrl 763 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361 recn 9986 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362361sincld 14804 . . . . . . . . 9 (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363362adantl 482 . . . . . . . 8 ((𝜒𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364 eqid 2621 . . . . . . . . 9 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365 2cn 11051 . . . . . . . . . . 11 2 ∈ ℂ
366 eldifsn 4294 . . . . . . . . . . 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 39324 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆‘(𝑗 + 1))))
371 sinf 14798 . . . . . . . . . . . . . 14 sin:ℂ⟶ℂ
372371a1i 11 . . . . . . . . . . . . 13 (⊤ → sin:ℂ⟶ℂ)
373329a1i 11 . . . . . . . . . . . . 13 (⊤ → ℝ ⊆ ℂ)
374372, 373feqresmpt 6217 . . . . . . . . . . . 12 (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375374trud 1490 . . . . . . . . . . 11 (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376 resincncf 39423 . . . . . . . . . . 11 (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377375, 376eqeltrri 2695 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378377a1i 11 . . . . . . . . 9 (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
37990rehalfcld 11239 . . . . . . . . 9 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380 fveq2 6158 . . . . . . . . 9 (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381378, 379, 380cnmptlimc 23594 . . . . . . . 8 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆‘(𝑗 + 1)) / 2)))
382 fveq2 6158 . . . . . . . 8 (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383 fveq2 6158 . . . . . . . . 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 23597 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆‘(𝑗 + 1))))
386356, 357, 343, 143, 150, 359, 385mullimc 39284 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆‘(𝑗 + 1))))
387331halfcld 11237 . . . . . . . 8 (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388387sincld 14804 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389154, 105sseldd 3589 . . . . . . . 8 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390 fourierdlem44 39705 . . . . . . . 8 (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391389, 341, 390syl2anc 692 . . . . . . 7 (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392358, 388, 369, 391mulne0d 10639 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 39324 . . . . 5 (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆‘(𝑗 + 1))))
3942, 3, 4, 142, 160, 342, 393mullimc 39284 . . . 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 5362 . . . . . 6 (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
399 ioossicc 12217 . . . . . . . 8 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1)))
400 iccss 12199 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
40119, 98, 85, 107, 400syl22anc 1324 . . . . . . . 8 (𝜒 → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402399, 401syl5ss 3599 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403402resmptd 5421 . . . . . 6 (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404398, 403syl5eq 2667 . . . . 5 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405404oveq1d 6630 . . . 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 10132 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄𝑖))
409 fourierdlem76.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
4106, 223, 409syl2anc 692 . . . . . . . . . . 11 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)))
411240oveq2d 6631 . . . . . . . . . . 11 (𝜒 → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉𝑖)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
412410, 411eleqtrd 2700 . . . . . . . . . 10 (𝜒𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄𝑖))))
413193recnd 10028 . . . . . . . . . 10 (𝜒 → (𝑄𝑖) ∈ ℂ)
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 39713 . . . . . . . . 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 39693 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) ∈ (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
418 eqidd 2622 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419 oveq2 6623 . . . . . . . . . . . 12 (𝑠 = (𝑆𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆𝑗)))
420419fveq2d 6162 . . . . . . . . . . 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 10151 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄𝑖) < (𝑆𝑗))
43090adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431211adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432297adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
433314adantr 481 . . . . . . . . . . . 12 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434424, 430, 431, 432, 433ltletrd 10157 . . . . . . . . . . 11 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) < (𝑄‘(𝑖 + 1)))
435422, 423, 424, 429, 434eliood 39166 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝑆𝑗) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
436230, 290readdcld 10029 . . . . . . . . . . . 12 (𝜒 → (𝑋 + (𝑆𝑗)) ∈ ℝ)
437276, 436ffvelrnd 6326 . . . . . . . . . . 11 (𝜒 → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
438437adantr 481 . . . . . . . . . 10 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → (𝐹‘(𝑋 + (𝑆𝑗))) ∈ ℝ)
439418, 421, 435, 438fvmptd 6255 . . . . . . . . 9 ((𝜒 ∧ ¬ (𝑆𝑗) = (𝑄𝑖)) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗)) = (𝐹‘(𝑋 + (𝑆𝑗))))
440439ifeq2da 4095 . . . . . . . 8 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆𝑗))) = if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))))
441326oveq1d 6630 . . . . . . . 8 (𝜒 → (((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
442417, 440, 4413eltr3d 2712 . . . . . . 7 (𝜒 → if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑆𝑗)))
443290recnd 10028 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ ℂ)
444168, 330, 124, 443constlimc 39292 . . . . . . 7 (𝜒𝐶 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim (𝑆𝑗)))
445167, 168, 161, 121, 125, 442, 444sublimc 39320 . . . . . 6 (𝜒 → (if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim (𝑆𝑗)))
446330, 162, 443idlimc 39294 . . . . . 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 3256 . . . . . . 7 ((𝑆𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆𝑗) ∈ (𝐴[,]𝐵)) → (𝑆𝑗) ≠ 0))
45383, 447, 452sylc 65 . . . . . 6 (𝜒 → (𝑆𝑗) ≠ 0)
454161, 162, 2, 126, 166, 445, 446, 453, 141divlimc 39324 . . . . 5 (𝜒 → ((if((𝑆𝑗) = (𝑄𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆𝑗)))) − 𝐶) / (𝑆𝑗)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim (𝑆𝑗)))
455356, 330, 358, 443constlimc 39292 . . . . . . 7 (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim (𝑆𝑗)))
456348ad2antrl 763 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457162, 356, 364, 148, 368, 446, 455, 369, 152divlimc 39324 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim (𝑆𝑗)))
458290rehalfcld 11239 . . . . . . . . 9 (𝜒 → ((𝑆𝑗) / 2) ∈ ℝ)
459 fveq2 6158 . . . . . . . . 9 (𝑥 = ((𝑆𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆𝑗) / 2)))
460378, 458, 459cnmptlimc 23594 . . . . . . . 8 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim ((𝑆𝑗) / 2)))
461 fveq2 6158 . . . . . . . . 9 ((𝑠 / 2) = ((𝑆𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
462461ad2antll 764 . . . . . . . 8 ((𝜒 ∧ (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆𝑗) / 2)))
463456, 363, 457, 460, 382, 462limcco 23597 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim (𝑆𝑗)))
464356, 357, 343, 143, 150, 455, 463mullimc 39284 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim (𝑆𝑗)))
465443halfcld 11237 . . . . . . . 8 (𝜒 → ((𝑆𝑗) / 2) ∈ ℂ)
466465sincld 14804 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ∈ ℂ)
467154, 83sseldd 3589 . . . . . . . 8 (𝜒 → (𝑆𝑗) ∈ (-π[,]π))
468 fourierdlem44 39705 . . . . . . . 8 (((𝑆𝑗) ∈ (-π[,]π) ∧ (𝑆𝑗) ≠ 0) → (sin‘((𝑆𝑗) / 2)) ≠ 0)
469467, 453, 468syl2anc 692 . . . . . . 7 (𝜒 → (sin‘((𝑆𝑗) / 2)) ≠ 0)
470358, 466, 369, 469mulne0d 10639 . . . . . 6 (𝜒 → (2 · (sin‘((𝑆𝑗) / 2))) ≠ 0)
471162, 343, 3, 148, 355, 446, 464, 470, 159divlimc 39324 . . . . 5 (𝜒 → ((𝑆𝑗) / (2 · (sin‘((𝑆𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim (𝑆𝑗)))
4722, 3, 4, 142, 160, 454, 471mullimc 39284 . . . 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 6630 . . . 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 3588 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
479478, 266syldan 487 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480479mpteq2dva 4714 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481225adantr 481 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) ∈ ℝ*)
482228adantr 481 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
483230adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484483, 129readdcld 10029 . . . . . . . . . 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 10156 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
491485, 490eqbrtrd 4645 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
492211adantr 481 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493487, 488, 478, 253syl3anc 1323 . . . . . . . . . . . 12 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
49418, 492, 483, 493ltadd2dd 10156 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495260adantr 481 . . . . . . . . . . 11 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496494, 495breqtrd 4649 . . . . . . . . . 10 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497481, 482, 484, 491, 496eliood 39166 . . . . . . . . 9 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
498269, 271, 330, 237, 497fourierdlem23 39684 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499480, 498eqeltrd 2698 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500 ssid 3609 . . . . . . . . 9 ℂ ⊆ ℂ
501500a1i 11 . . . . . . . 8 (𝜒 → ℂ ⊆ ℂ)
502330, 124, 501constcncfg 39419 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503499, 502subcncf 39417 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504166ralrimiva 2962 . . . . . . . 8 (𝜒 → ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505 dfss3 3578 . . . . . . . 8 (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506504, 505sylibr 224 . . . . . . 7 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507 difssd 3722 . . . . . . 7 (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508506, 507idcncfg 39420 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509503, 508divcncf 23156 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510330, 501idcncfg 39420 . . . . . 6 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511355, 343fmptd 6351 . . . . . . 7 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512330, 358, 501constcncfg 39419 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513 sincn 24136 . . . . . . . . . . 11 sin ∈ (ℂ–cn→ℂ)
514513a1i 11 . . . . . . . . . 10 (𝜒 → sin ∈ (ℂ–cn→ℂ))
515367a1i 11 . . . . . . . . . . . 12 (𝜒 → 2 ∈ (ℂ ∖ {0}))
516330, 515, 507constcncfg 39419 . . . . . . . . . . 11 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517510, 516divcncf 23156 . . . . . . . . . 10 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518514, 517cncfmpt1f 22656 . . . . . . . . 9 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519512, 518mulcncf 23155 . . . . . . . 8 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520 cncffvrn 22641 . . . . . . . 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 23156 . . . . 5 (𝜒 → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524509, 523mulcncf 23155 . . . 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 2908  {crab 2912  cdif 3557  cun 3558  cin 3559  wss 3560  ifcif 4064  {csn 4155  {cpr 4157   class class class wbr 4623  cmpt 4683  dom cdm 5084  ran crn 5085  cres 5086  cio 5818  Fun wfun 5851  wf 5853  1-1-ontowf1o 5856  cfv 5857   Isom wiso 5858  (class class class)co 6615  𝑚 cmap 7817  Fincfn 7915  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901  *cxr 10033   < clt 10034  cle 10035  cmin 10226  -cneg 10227   / cdiv 10644  cn 10980  2c2 11030  cz 11337  (,)cioo 12133  [,)cico 12135  [,]cicc 12136  ...cfz 12284  ..^cfzo 12422  #chash 13073  sincsin 14738  πcpi 14741  t crest 16021  TopOpenctopn 16022  fldccnfld 19686  cnccncf 22619   lim climc 23566
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 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
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 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ioc 12138  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046  df-hash 13074  df-shft 13757  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-sum 14367  df-ef 14742  df-sin 14744  df-cos 14745  df-pi 14747  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lp 20880  df-perf 20881  df-cn 20971  df-cnp 20972  df-haus 21059  df-tx 21305  df-hmeo 21498  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-limc 23570  df-dv 23571
This theorem is referenced by:  fourierdlem86  39746
  Copyright terms: Public domain W3C validator