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 44497
Description: Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem76.f (πœ‘ β†’ 𝐹:β„βŸΆβ„)
fourierdlem76.xre (πœ‘ β†’ 𝑋 ∈ ℝ)
fourierdlem76.p 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (-Ο€ + 𝑋) ∧ (π‘β€˜π‘š) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem76.m (πœ‘ β†’ 𝑀 ∈ β„•)
fourierdlem76.v (πœ‘ β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
fourierdlem76.fcn ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
fourierdlem76.r ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
fourierdlem76.l ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
fourierdlem76.a (πœ‘ β†’ 𝐴 ∈ ℝ)
fourierdlem76.b (πœ‘ β†’ 𝐡 ∈ ℝ)
fourierdlem76.altb (πœ‘ β†’ 𝐴 < 𝐡)
fourierdlem76.ab (πœ‘ β†’ (𝐴[,]𝐡) βŠ† (-Ο€[,]Ο€))
fourierdlem76.n0 (πœ‘ β†’ Β¬ 0 ∈ (𝐴[,]𝐡))
fourierdlem76.c (πœ‘ β†’ 𝐢 ∈ ℝ)
fourierdlem76.o 𝑂 = (𝑠 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
fourierdlem76.q 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
fourierdlem76.t 𝑇 = ({𝐴, 𝐡} βˆͺ (ran 𝑄 ∩ (𝐴(,)𝐡)))
fourierdlem76.n 𝑁 = ((β™―β€˜π‘‡) βˆ’ 1)
fourierdlem76.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
fourierdlem76.d 𝐷 = (((if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1))))) βˆ’ 𝐢) / (π‘†β€˜(𝑗 + 1))) Β· ((π‘†β€˜(𝑗 + 1)) / (2 Β· (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)))))
fourierdlem76.e 𝐸 = (((if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, (πΉβ€˜(𝑋 + (π‘†β€˜π‘—)))) βˆ’ 𝐢) / (π‘†β€˜π‘—)) Β· ((π‘†β€˜π‘—) / (2 Β· (sinβ€˜((π‘†β€˜π‘—) / 2)))))
fourierdlem76.ch (πœ’ ↔ (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))))
Assertion
Ref Expression
fourierdlem76 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((𝐷 ∈ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜π‘—))) ∧ (𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚)))
Distinct variable groups:   𝐴,𝑠   𝐡,𝑠   𝐢,𝑠   𝐹,𝑠   𝐿,𝑠   𝑖,𝑀,𝑗   π‘š,𝑀,𝑝,𝑖   𝑓,𝑁   𝑄,𝑠   𝑅,𝑠   𝑆,𝑓   𝑆,𝑠   𝑇,𝑓   𝑖,𝑉,𝑗,𝑠   𝑉,𝑝   𝑖,𝑋,𝑗,𝑠   π‘š,𝑋,𝑝   πœ’,𝑠   πœ‘,𝑓   πœ‘,𝑖,𝑗,𝑠
Allowed substitution hints:   πœ‘(π‘š,𝑝)   πœ’(𝑓,𝑖,𝑗,π‘š,𝑝)   𝐴(𝑓,𝑖,𝑗,π‘š,𝑝)   𝐡(𝑓,𝑖,𝑗,π‘š,𝑝)   𝐢(𝑓,𝑖,𝑗,π‘š,𝑝)   𝐷(𝑓,𝑖,𝑗,π‘š,𝑠,𝑝)   𝑃(𝑓,𝑖,𝑗,π‘š,𝑠,𝑝)   𝑄(𝑓,𝑖,𝑗,π‘š,𝑝)   𝑅(𝑓,𝑖,𝑗,π‘š,𝑝)   𝑆(𝑖,𝑗,π‘š,𝑝)   𝑇(𝑖,𝑗,π‘š,𝑠,𝑝)   𝐸(𝑓,𝑖,𝑗,π‘š,𝑠,𝑝)   𝐹(𝑓,𝑖,𝑗,π‘š,𝑝)   𝐿(𝑓,𝑖,𝑗,π‘š,𝑝)   𝑀(𝑓,𝑠)   𝑁(𝑖,𝑗,π‘š,𝑠,𝑝)   𝑂(𝑓,𝑖,𝑗,π‘š,𝑠,𝑝)   𝑉(𝑓,π‘š)   𝑋(𝑓)

Proof of Theorem fourierdlem76
Dummy variable π‘₯ is distinct from all other variables.
StepHypRef Expression
1 fourierdlem76.ch . . 3 (πœ’ ↔ (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))))
2 eqid 2737 . . . . 5 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠)) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠))
3 eqid 2737 . . . . 5 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))
4 eqid 2737 . . . . 5 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
5 simplll 774 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ πœ‘)
61, 5sylbi 216 . . . . . . . . . 10 (πœ’ β†’ πœ‘)
76adantr 482 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ πœ‘)
8 ioossicc 13357 . . . . . . . . . 10 (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡)
9 fourierdlem76.a . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ∈ ℝ)
109rexrd 11212 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴 ∈ ℝ*)
116, 10syl 17 . . . . . . . . . . . 12 (πœ’ β†’ 𝐴 ∈ ℝ*)
1211adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝐴 ∈ ℝ*)
13 fourierdlem76.b . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐡 ∈ ℝ)
1413rexrd 11212 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ ℝ*)
156, 14syl 17 . . . . . . . . . . . 12 (πœ’ β†’ 𝐡 ∈ ℝ*)
1615adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝐡 ∈ ℝ*)
17 elioore 13301 . . . . . . . . . . . 12 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) β†’ 𝑠 ∈ ℝ)
1817adantl 483 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ ℝ)
196, 9syl 17 . . . . . . . . . . . . 13 (πœ’ β†’ 𝐴 ∈ ℝ)
2019adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝐴 ∈ ℝ)
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19 𝑇 = ({𝐴, 𝐡} βˆͺ (ran 𝑄 ∩ (𝐴(,)𝐡)))
22 prfi 9273 . . . . . . . . . . . . . . . . . . . . 21 {𝐴, 𝐡} ∈ Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ {𝐴, 𝐡} ∈ Fin)
24 fzfid 13885 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (0...𝑀) ∈ Fin)
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
2625rnmptfi 43462 . . . . . . . . . . . . . . . . . . . . 21 ((0...𝑀) ∈ Fin β†’ ran 𝑄 ∈ Fin)
27 infi 9219 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∈ Fin β†’ (ran 𝑄 ∩ (𝐴(,)𝐡)) ∈ Fin)
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (ran 𝑄 ∩ (𝐴(,)𝐡)) ∈ Fin)
29 unfi 9123 . . . . . . . . . . . . . . . . . . . 20 (({𝐴, 𝐡} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐡)) ∈ Fin) β†’ ({𝐴, 𝐡} βˆͺ (ran 𝑄 ∩ (𝐴(,)𝐡))) ∈ Fin)
3023, 28, 29syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ({𝐴, 𝐡} βˆͺ (ran 𝑄 ∩ (𝐴(,)𝐡))) ∈ Fin)
3121, 30eqeltrid 2842 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑇 ∈ Fin)
32 prssg 4784 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ↔ {𝐴, 𝐡} βŠ† ℝ))
339, 13, 32syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ↔ {𝐴, 𝐡} βŠ† ℝ))
349, 13, 33mpbi2and 711 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ {𝐴, 𝐡} βŠ† ℝ)
35 inss2 4194 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑄 ∩ (𝐴(,)𝐡)) βŠ† (𝐴(,)𝐡)
36 ioossre 13332 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴(,)𝐡) βŠ† ℝ
3735, 36sstri 3958 . . . . . . . . . . . . . . . . . . . . 21 (ran 𝑄 ∩ (𝐴(,)𝐡)) βŠ† ℝ
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (ran 𝑄 ∩ (𝐴(,)𝐡)) βŠ† ℝ)
3934, 38unssd 4151 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ({𝐴, 𝐡} βˆͺ (ran 𝑄 ∩ (𝐴(,)𝐡))) βŠ† ℝ)
4021, 39eqsstrid 3997 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑇 βŠ† ℝ)
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18 𝑁 = ((β™―β€˜π‘‡) βˆ’ 1)
4331, 40, 41, 42fourierdlem36 44458 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑆 Isom < , < ((0...𝑁), 𝑇))
446, 43syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ 𝑆 Isom < , < ((0...𝑁), 𝑇))
45 isof1o 7273 . . . . . . . . . . . . . . . 16 (𝑆 Isom < , < ((0...𝑁), 𝑇) β†’ 𝑆:(0...𝑁)–1-1-onto→𝑇)
46 f1of 6789 . . . . . . . . . . . . . . . 16 (𝑆:(0...𝑁)–1-1-onto→𝑇 β†’ 𝑆:(0...𝑁)βŸΆπ‘‡)
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑆:(0...𝑁)βŸΆπ‘‡)
486, 40syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑇 βŠ† ℝ)
4947, 48fssd 6691 . . . . . . . . . . . . . 14 (πœ’ β†’ 𝑆:(0...𝑁)βŸΆβ„)
5049adantr 482 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑆:(0...𝑁)βŸΆβ„)
51 simpllr 775 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑗 ∈ (0..^𝑁))
521, 51sylbi 216 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑗 ∈ (0..^𝑁))
53 elfzofz 13595 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑁) β†’ 𝑗 ∈ (0...𝑁))
5452, 53syl 17 . . . . . . . . . . . . . 14 (πœ’ β†’ 𝑗 ∈ (0...𝑁))
5554adantr 482 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑗 ∈ (0...𝑁))
5650, 55ffvelcdmd 7041 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘†β€˜π‘—) ∈ ℝ)
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑆:(0...𝑁)βŸΆπ‘‡)
58 frn 6680 . . . . . . . . . . . . . . . . . 18 (𝑆:(0...𝑁)βŸΆπ‘‡ β†’ ran 𝑆 βŠ† 𝑇)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ran 𝑆 βŠ† 𝑇)
609leidd 11728 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐴 ≀ 𝐴)
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐴 < 𝐡)
629, 13, 61ltled 11310 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐴 ≀ 𝐡)
639, 13, 9, 60, 62eliccd 43816 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐴 ∈ (𝐴[,]𝐡))
6413leidd 11728 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐡 ≀ 𝐡)
659, 13, 13, 62, 64eliccd 43816 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐡 ∈ (𝐴[,]𝐡))
66 prssg 4784 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((𝐴 ∈ (𝐴[,]𝐡) ∧ 𝐡 ∈ (𝐴[,]𝐡)) ↔ {𝐴, 𝐡} βŠ† (𝐴[,]𝐡)))
679, 13, 66syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐴 ∈ (𝐴[,]𝐡) ∧ 𝐡 ∈ (𝐴[,]𝐡)) ↔ {𝐴, 𝐡} βŠ† (𝐴[,]𝐡)))
6863, 65, 67mpbi2and 711 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ {𝐴, 𝐡} βŠ† (𝐴[,]𝐡))
6935, 8sstri 3958 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑄 ∩ (𝐴(,)𝐡)) βŠ† (𝐴[,]𝐡)
7069a1i 11 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (ran 𝑄 ∩ (𝐴(,)𝐡)) βŠ† (𝐴[,]𝐡))
7168, 70unssd 4151 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ({𝐴, 𝐡} βˆͺ (ran 𝑄 ∩ (𝐴(,)𝐡))) βŠ† (𝐴[,]𝐡))
7221, 71eqsstrid 3997 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑇 βŠ† (𝐴[,]𝐡))
7359, 72sstrd 3959 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ran 𝑆 βŠ† (𝐴[,]𝐡))
746, 73syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ ran 𝑆 βŠ† (𝐴[,]𝐡))
75 ffun 6676 . . . . . . . . . . . . . . . . 17 (𝑆:(0...𝑁)βŸΆβ„ β†’ Fun 𝑆)
7649, 75syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ Fun 𝑆)
77 fdm 6682 . . . . . . . . . . . . . . . . . . 19 (𝑆:(0...𝑁)βŸΆβ„ β†’ dom 𝑆 = (0...𝑁))
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ dom 𝑆 = (0...𝑁))
7978eqcomd 2743 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (0...𝑁) = dom 𝑆)
8054, 79eleqtrd 2840 . . . . . . . . . . . . . . . 16 (πœ’ β†’ 𝑗 ∈ dom 𝑆)
81 fvelrn 7032 . . . . . . . . . . . . . . . 16 ((Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆) β†’ (π‘†β€˜π‘—) ∈ ran 𝑆)
8276, 80, 81syl2anc 585 . . . . . . . . . . . . . . 15 (πœ’ β†’ (π‘†β€˜π‘—) ∈ ran 𝑆)
8374, 82sseldd 3950 . . . . . . . . . . . . . 14 (πœ’ β†’ (π‘†β€˜π‘—) ∈ (𝐴[,]𝐡))
84 iccgelb 13327 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ (π‘†β€˜π‘—) ∈ (𝐴[,]𝐡)) β†’ 𝐴 ≀ (π‘†β€˜π‘—))
8511, 15, 83, 84syl3anc 1372 . . . . . . . . . . . . 13 (πœ’ β†’ 𝐴 ≀ (π‘†β€˜π‘—))
8685adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝐴 ≀ (π‘†β€˜π‘—))
8756rexrd 11212 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘†β€˜π‘—) ∈ ℝ*)
88 fzofzp1 13676 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) β†’ (𝑗 + 1) ∈ (0...𝑁))
8952, 88syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (𝑗 + 1) ∈ (0...𝑁))
9049, 89ffvelcdmd 7041 . . . . . . . . . . . . . . 15 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ∈ ℝ)
9190rexrd 11212 . . . . . . . . . . . . . 14 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ∈ ℝ*)
9291adantr 482 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘†β€˜(𝑗 + 1)) ∈ ℝ*)
93 simpr 486 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))))
94 ioogtlb 43807 . . . . . . . . . . . . 13 (((π‘†β€˜π‘—) ∈ ℝ* ∧ (π‘†β€˜(𝑗 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘†β€˜π‘—) < 𝑠)
9587, 92, 93, 94syl3anc 1372 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘†β€˜π‘—) < 𝑠)
9620, 56, 18, 86, 95lelttrd 11320 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝐴 < 𝑠)
9790adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘†β€˜(𝑗 + 1)) ∈ ℝ)
986, 13syl 17 . . . . . . . . . . . . 13 (πœ’ β†’ 𝐡 ∈ ℝ)
9998adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝐡 ∈ ℝ)
100 iooltub 43822 . . . . . . . . . . . . 13 (((π‘†β€˜π‘—) ∈ ℝ* ∧ (π‘†β€˜(𝑗 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 < (π‘†β€˜(𝑗 + 1)))
10187, 92, 93, 100syl3anc 1372 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 < (π‘†β€˜(𝑗 + 1)))
10289, 79eleqtrd 2840 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (𝑗 + 1) ∈ dom 𝑆)
103 fvelrn 7032 . . . . . . . . . . . . . . . 16 ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) β†’ (π‘†β€˜(𝑗 + 1)) ∈ ran 𝑆)
10476, 102, 103syl2anc 585 . . . . . . . . . . . . . . 15 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ∈ ran 𝑆)
10574, 104sseldd 3950 . . . . . . . . . . . . . 14 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ∈ (𝐴[,]𝐡))
106 iccleub 13326 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ (π‘†β€˜(𝑗 + 1)) ∈ (𝐴[,]𝐡)) β†’ (π‘†β€˜(𝑗 + 1)) ≀ 𝐡)
10711, 15, 105, 106syl3anc 1372 . . . . . . . . . . . . 13 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ≀ 𝐡)
108107adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘†β€˜(𝑗 + 1)) ≀ 𝐡)
10918, 97, 99, 101, 108ltletrd 11322 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 < 𝐡)
11012, 16, 18, 96, 109eliood 43810 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ (𝐴(,)𝐡))
1118, 110sselid 3947 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ (𝐴[,]𝐡))
112 fourierdlem76.f . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
113112adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ 𝐹:β„βŸΆβ„)
114 fourierdlem76.xre . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ ℝ)
115114adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ 𝑋 ∈ ℝ)
1169, 13iccssred 13358 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
117116sselda 3949 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ 𝑠 ∈ ℝ)
118115, 117readdcld 11191 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ (𝑋 + 𝑠) ∈ ℝ)
119113, 118ffvelcdmd 7041 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
1207, 111, 119syl2anc 585 . . . . . . . 8 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
121120recnd 11190 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
122 fourierdlem76.c . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ ℝ)
123122recnd 11190 . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ β„‚)
1246, 123syl 17 . . . . . . . 8 (πœ’ β†’ 𝐢 ∈ β„‚)
125124adantr 482 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝐢 ∈ β„‚)
126121, 125subcld 11519 . . . . . 6 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) ∈ β„‚)
127 ioossre 13332 . . . . . . . . 9 ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ℝ
128127a1i 11 . . . . . . . 8 (πœ’ β†’ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ℝ)
129128sselda 3949 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ ℝ)
130129recnd 11190 . . . . . 6 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ β„‚)
131 nne 2948 . . . . . . . . . . . 12 (Β¬ 𝑠 β‰  0 ↔ 𝑠 = 0)
132131biimpi 215 . . . . . . . . . . 11 (Β¬ 𝑠 β‰  0 β†’ 𝑠 = 0)
133132eqcomd 2743 . . . . . . . . . 10 (Β¬ 𝑠 β‰  0 β†’ 0 = 𝑠)
134133adantl 483 . . . . . . . . 9 (((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) ∧ Β¬ 𝑠 β‰  0) β†’ 0 = 𝑠)
135 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ 𝑠 ∈ (𝐴[,]𝐡))
136135adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) ∧ Β¬ 𝑠 β‰  0) β†’ 𝑠 ∈ (𝐴[,]𝐡))
137134, 136eqeltrd 2838 . . . . . . . 8 (((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) ∧ Β¬ 𝑠 β‰  0) β†’ 0 ∈ (𝐴[,]𝐡))
138 fourierdlem76.n0 . . . . . . . . 9 (πœ‘ β†’ Β¬ 0 ∈ (𝐴[,]𝐡))
139138ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) ∧ Β¬ 𝑠 β‰  0) β†’ Β¬ 0 ∈ (𝐴[,]𝐡))
140137, 139condan 817 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ 𝑠 β‰  0)
1417, 111, 140syl2anc 585 . . . . . 6 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 β‰  0)
142126, 130, 141divcld 11938 . . . . 5 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) ∈ β„‚)
143 2cnd 12238 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 2 ∈ β„‚)
144130halfcld 12405 . . . . . . . 8 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑠 / 2) ∈ β„‚)
145144sincld 16019 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (sinβ€˜(𝑠 / 2)) ∈ β„‚)
146143, 145mulcld 11182 . . . . . 6 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ β„‚)
14717recnd 11190 . . . . . . . . . 10 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) β†’ 𝑠 ∈ β„‚)
148147adantl 483 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ β„‚)
149148halfcld 12405 . . . . . . . 8 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑠 / 2) ∈ β„‚)
150149sincld 16019 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (sinβ€˜(𝑠 / 2)) ∈ β„‚)
151 2ne0 12264 . . . . . . . 8 2 β‰  0
152151a1i 11 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 2 β‰  0)
153 fourierdlem76.ab . . . . . . . . . . 11 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† (-Ο€[,]Ο€))
1546, 153syl 17 . . . . . . . . . 10 (πœ’ β†’ (𝐴[,]𝐡) βŠ† (-Ο€[,]Ο€))
155154adantr 482 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝐴[,]𝐡) βŠ† (-Ο€[,]Ο€))
156155, 111sseldd 3950 . . . . . . . 8 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
157 fourierdlem44 44466 . . . . . . . 8 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ 𝑠 β‰  0) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
158156, 141, 157syl2anc 585 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
159143, 150, 152, 158mulne0d 11814 . . . . . 6 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) β‰  0)
160130, 146, 159divcld 11938 . . . . 5 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ β„‚)
161 eqid 2737 . . . . . 6 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢))
162 eqid 2737 . . . . . 6 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝑠)
163141neneqd 2949 . . . . . . . 8 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ Β¬ 𝑠 = 0)
164 velsn 4607 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
165163, 164sylnibr 329 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ Β¬ 𝑠 ∈ {0})
166130, 165eldifd 3926 . . . . . 6 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ (β„‚ βˆ– {0}))
167 eqid 2737 . . . . . . 7 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))
168 eqid 2737 . . . . . . 7 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝐢) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝐢)
169 elfzofz 13595 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) β†’ 𝑖 ∈ (0...𝑀))
170169adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑖 ∈ (0...𝑀))
171 pire 25831 . . . . . . . . . . . . . . . . . . . . 21 Ο€ ∈ ℝ
172171renegcli 11469 . . . . . . . . . . . . . . . . . . . 20 -Ο€ ∈ ℝ
173172a1i 11 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ -Ο€ ∈ ℝ)
174173, 114readdcld 11191 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (-Ο€ + 𝑋) ∈ ℝ)
175171a1i 11 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Ο€ ∈ ℝ)
176175, 114readdcld 11191 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (Ο€ + 𝑋) ∈ ℝ)
177174, 176iccssred 13358 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((-Ο€ + 𝑋)[,](Ο€ + 𝑋)) βŠ† ℝ)
178177adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((-Ο€ + 𝑋)[,](Ο€ + 𝑋)) βŠ† ℝ)
179 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (-Ο€ + 𝑋) ∧ (π‘β€˜π‘š) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑀 ∈ β„•)
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
182179, 180, 181fourierdlem15 44437 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑉:(0...𝑀)⟢((-Ο€ + 𝑋)[,](Ο€ + 𝑋)))
183182adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑉:(0...𝑀)⟢((-Ο€ + 𝑋)[,](Ο€ + 𝑋)))
184183, 170ffvelcdmd 7041 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) ∈ ((-Ο€ + 𝑋)[,](Ο€ + 𝑋)))
185178, 184sseldd 3950 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) ∈ ℝ)
186114adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑋 ∈ ℝ)
187185, 186resubcld 11590 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ∈ ℝ)
18825fvmpt2 6964 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0...𝑀) ∧ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ∈ ℝ) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
189170, 187, 188syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
190189, 187eqeltrd 2838 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) ∈ ℝ)
191190adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) ∈ ℝ)
192191adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) ∈ ℝ)
1931, 192sylbi 216 . . . . . . . . 9 (πœ’ β†’ (π‘„β€˜π‘–) ∈ ℝ)
194 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 β†’ (π‘‰β€˜π‘–) = (π‘‰β€˜π‘—))
195194oveq1d 7377 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) = ((π‘‰β€˜π‘—) βˆ’ 𝑋))
196195cbvmptv 5223 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋))
19725, 196eqtri 2765 . . . . . . . . . . . . . . 15 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋))
198197a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋)))
199 fveq2 6847 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑖 + 1) β†’ (π‘‰β€˜π‘—) = (π‘‰β€˜(𝑖 + 1)))
200199oveq1d 7377 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) β†’ ((π‘‰β€˜π‘—) βˆ’ 𝑋) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
201200adantl 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) β†’ ((π‘‰β€˜π‘—) βˆ’ 𝑋) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
202 fzofzp1 13676 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) β†’ (𝑖 + 1) ∈ (0...𝑀))
203202adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑖 + 1) ∈ (0...𝑀))
204183, 203ffvelcdmd 7041 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ((-Ο€ + 𝑋)[,](Ο€ + 𝑋)))
205178, 204sseldd 3950 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ)
206205, 186resubcld 11590 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋) ∈ ℝ)
207198, 201, 203, 206fvmptd 6960 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜(𝑖 + 1)) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
208207, 206eqeltrd 2838 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
209208adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
210209adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
2111, 210sylbi 216 . . . . . . . . 9 (πœ’ β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
212179fourierdlem2 44424 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ β„• β†’ (𝑉 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘‰β€˜0) = (-Ο€ + 𝑋) ∧ (π‘‰β€˜π‘€) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1))))))
213180, 212syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝑉 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘‰β€˜0) = (-Ο€ + 𝑋) ∧ (π‘‰β€˜π‘€) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1))))))
214181, 213mpbid 231 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘‰β€˜0) = (-Ο€ + 𝑋) ∧ (π‘‰β€˜π‘€) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1)))))
215214simprrd 773 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1)))
216215r19.21bi 3237 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1)))
217185, 205, 186, 216ltsub1dd 11774 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) < ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
218217, 189, 2073brtr4d 5142 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)))
219218adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)))
220219adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)))
2211, 220sylbi 216 . . . . . . . . 9 (πœ’ β†’ (π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)))
2221biimpi 215 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))))
223222simplrd 769 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 𝑖 ∈ (0..^𝑀))
2246, 223, 185syl2anc 585 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘‰β€˜π‘–) ∈ ℝ)
225224rexrd 11212 . . . . . . . . . . . . . . 15 (πœ’ β†’ (π‘‰β€˜π‘–) ∈ ℝ*)
226225adantr 482 . . . . . . . . . . . . . 14 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) ∈ ℝ*)
2276, 223, 205syl2anc 585 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ)
228227rexrd 11212 . . . . . . . . . . . . . . 15 (πœ’ β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ*)
229228adantr 482 . . . . . . . . . . . . . 14 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ*)
2306, 114syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ 𝑋 ∈ ℝ)
231230adantr 482 . . . . . . . . . . . . . . 15 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑋 ∈ ℝ)
232 elioore 13301 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) β†’ 𝑠 ∈ ℝ)
233232adantl 483 . . . . . . . . . . . . . . 15 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ℝ)
234231, 233readdcld 11191 . . . . . . . . . . . . . 14 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) ∈ ℝ)
2356, 223, 189syl2anc 585 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
236235oveq2d 7378 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (𝑋 + (π‘„β€˜π‘–)) = (𝑋 + ((π‘‰β€˜π‘–) βˆ’ 𝑋)))
237230recnd 11190 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ 𝑋 ∈ β„‚)
238224recnd 11190 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (π‘‰β€˜π‘–) ∈ β„‚)
239237, 238pncan3d 11522 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (𝑋 + ((π‘‰β€˜π‘–) βˆ’ 𝑋)) = (π‘‰β€˜π‘–))
240236, 239eqtr2d 2778 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘‰β€˜π‘–) = (𝑋 + (π‘„β€˜π‘–)))
241240adantr 482 . . . . . . . . . . . . . . 15 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) = (𝑋 + (π‘„β€˜π‘–)))
242193adantr 482 . . . . . . . . . . . . . . . 16 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) ∈ ℝ)
243193rexrd 11212 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (π‘„β€˜π‘–) ∈ ℝ*)
244243adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) ∈ ℝ*)
245211rexrd 11212 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ*)
246245adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ*)
247 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
248 ioogtlb 43807 . . . . . . . . . . . . . . . . 17 (((π‘„β€˜π‘–) ∈ ℝ* ∧ (π‘„β€˜(𝑖 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) < 𝑠)
249244, 246, 247, 248syl3anc 1372 . . . . . . . . . . . . . . . 16 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) < 𝑠)
250242, 233, 231, 249ltadd2dd 11321 . . . . . . . . . . . . . . 15 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + (π‘„β€˜π‘–)) < (𝑋 + 𝑠))
251241, 250eqbrtrd 5132 . . . . . . . . . . . . . 14 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) < (𝑋 + 𝑠))
252211adantr 482 . . . . . . . . . . . . . . . 16 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
253 iooltub 43822 . . . . . . . . . . . . . . . . 17 (((π‘„β€˜π‘–) ∈ ℝ* ∧ (π‘„β€˜(𝑖 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 < (π‘„β€˜(𝑖 + 1)))
254244, 246, 247, 253syl3anc 1372 . . . . . . . . . . . . . . . 16 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 < (π‘„β€˜(𝑖 + 1)))
255233, 252, 231, 254ltadd2dd 11321 . . . . . . . . . . . . . . 15 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) < (𝑋 + (π‘„β€˜(𝑖 + 1))))
2566, 223, 207syl2anc 585 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (π‘„β€˜(𝑖 + 1)) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
257256oveq2d 7378 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (𝑋 + (π‘„β€˜(𝑖 + 1))) = (𝑋 + ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋)))
258227recnd 11190 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (π‘‰β€˜(𝑖 + 1)) ∈ β„‚)
259237, 258pncan3d 11522 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (𝑋 + ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋)) = (π‘‰β€˜(𝑖 + 1)))
260257, 259eqtrd 2777 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (𝑋 + (π‘„β€˜(𝑖 + 1))) = (π‘‰β€˜(𝑖 + 1)))
261260adantr 482 . . . . . . . . . . . . . . 15 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + (π‘„β€˜(𝑖 + 1))) = (π‘‰β€˜(𝑖 + 1)))
262255, 261breqtrd 5136 . . . . . . . . . . . . . 14 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) < (π‘‰β€˜(𝑖 + 1)))
263226, 229, 234, 251, 262eliood 43810 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) ∈ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))
264 fvres 6866 . . . . . . . . . . . . 13 ((𝑋 + 𝑠) ∈ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) β†’ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
265263, 264syl 17 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
266265eqcomd 2743 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠)))
267266mpteq2dva 5210 . . . . . . . . . 10 (πœ’ β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠))))
268 ioosscn 13333 . . . . . . . . . . . 12 ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) βŠ† β„‚
269268a1i 11 . . . . . . . . . . 11 (πœ’ β†’ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) βŠ† β„‚)
270 fourierdlem76.fcn . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
2716, 223, 270syl2anc 585 . . . . . . . . . . 11 (πœ’ β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
272 ioosscn 13333 . . . . . . . . . . . 12 ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† β„‚
273272a1i 11 . . . . . . . . . . 11 (πœ’ β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† β„‚)
274269, 271, 273, 237, 263fourierdlem23 44445 . . . . . . . . . 10 (πœ’ β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
275267, 274eqeltrd 2838 . . . . . . . . 9 (πœ’ β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
2766, 112syl 17 . . . . . . . . . 10 (πœ’ β†’ 𝐹:β„βŸΆβ„)
277 ioossre 13332 . . . . . . . . . . 11 ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† ℝ
278277a1i 11 . . . . . . . . . 10 (πœ’ β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† ℝ)
279 eqid 2737 . . . . . . . . . 10 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))
280 ioossre 13332 . . . . . . . . . . 11 ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) βŠ† ℝ
281280a1i 11 . . . . . . . . . 10 (πœ’ β†’ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) βŠ† ℝ)
282233, 254ltned 11298 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 β‰  (π‘„β€˜(𝑖 + 1)))
283 fourierdlem76.l . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
2846, 223, 283syl2anc 585 . . . . . . . . . . 11 (πœ’ β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
285260eqcomd 2743 . . . . . . . . . . . 12 (πœ’ β†’ (π‘‰β€˜(𝑖 + 1)) = (𝑋 + (π‘„β€˜(𝑖 + 1))))
286285oveq2d 7378 . . . . . . . . . . 11 (πœ’ β†’ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (𝑋 + (π‘„β€˜(𝑖 + 1)))))
287284, 286eleqtrd 2840 . . . . . . . . . 10 (πœ’ β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (𝑋 + (π‘„β€˜(𝑖 + 1)))))
288211recnd 11190 . . . . . . . . . 10 (πœ’ β†’ (π‘„β€˜(𝑖 + 1)) ∈ β„‚)
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 44474 . . . . . . . . 9 (πœ’ β†’ 𝐿 ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
29049, 54ffvelcdmd 7041 . . . . . . . . 9 (πœ’ β†’ (π‘†β€˜π‘—) ∈ ℝ)
291 elfzoelz 13579 . . . . . . . . . . . 12 (𝑗 ∈ (0..^𝑁) β†’ 𝑗 ∈ β„€)
292 zre 12510 . . . . . . . . . . . 12 (𝑗 ∈ β„€ β†’ 𝑗 ∈ ℝ)
29352, 291, 2923syl 18 . . . . . . . . . . 11 (πœ’ β†’ 𝑗 ∈ ℝ)
294293ltp1d 12092 . . . . . . . . . 10 (πœ’ β†’ 𝑗 < (𝑗 + 1))
295 isorel 7276 . . . . . . . . . . 11 ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) β†’ (𝑗 < (𝑗 + 1) ↔ (π‘†β€˜π‘—) < (π‘†β€˜(𝑗 + 1))))
29644, 54, 89, 295syl12anc 836 . . . . . . . . . 10 (πœ’ β†’ (𝑗 < (𝑗 + 1) ↔ (π‘†β€˜π‘—) < (π‘†β€˜(𝑗 + 1))))
297294, 296mpbid 231 . . . . . . . . 9 (πœ’ β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝑗 + 1)))
2981simprbi 498 . . . . . . . . 9 (πœ’ β†’ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
299 eqid 2737 . . . . . . . . 9 if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜(𝑗 + 1)))) = if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜(𝑗 + 1))))
300 eqid 2737 . . . . . . . . 9 ((TopOpenβ€˜β„‚fld) β†Ύt (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βˆͺ {(π‘„β€˜(𝑖 + 1))})) = ((TopOpenβ€˜β„‚fld) β†Ύt (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βˆͺ {(π‘„β€˜(𝑖 + 1))}))
301193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300fourierdlem33 44455 . . . . . . . 8 (πœ’ β†’ if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜(𝑗 + 1)))) ∈ (((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
302 eqidd 2738 . . . . . . . . . 10 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))))
303 simpr 486 . . . . . . . . . . . 12 (((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) ∧ 𝑠 = (π‘†β€˜(𝑗 + 1))) β†’ 𝑠 = (π‘†β€˜(𝑗 + 1)))
304303oveq2d 7378 . . . . . . . . . . 11 (((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) ∧ 𝑠 = (π‘†β€˜(𝑗 + 1))) β†’ (𝑋 + 𝑠) = (𝑋 + (π‘†β€˜(𝑗 + 1))))
305304fveq2d 6851 . . . . . . . . . 10 (((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) ∧ 𝑠 = (π‘†β€˜(𝑗 + 1))) β†’ (πΉβ€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1)))))
306243adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘„β€˜π‘–) ∈ ℝ*)
307245adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ*)
30890adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘†β€˜(𝑗 + 1)) ∈ ℝ)
309193, 211, 290, 90, 297, 298fourierdlem10 44432 . . . . . . . . . . . . . 14 (πœ’ β†’ ((π‘„β€˜π‘–) ≀ (π‘†β€˜π‘—) ∧ (π‘†β€˜(𝑗 + 1)) ≀ (π‘„β€˜(𝑖 + 1))))
310309simpld 496 . . . . . . . . . . . . 13 (πœ’ β†’ (π‘„β€˜π‘–) ≀ (π‘†β€˜π‘—))
311193, 290, 90, 310, 297lelttrd 11320 . . . . . . . . . . . 12 (πœ’ β†’ (π‘„β€˜π‘–) < (π‘†β€˜(𝑗 + 1)))
312311adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘„β€˜π‘–) < (π‘†β€˜(𝑗 + 1)))
313211adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
314309simprd 497 . . . . . . . . . . . . 13 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ≀ (π‘„β€˜(𝑖 + 1)))
315314adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘†β€˜(𝑗 + 1)) ≀ (π‘„β€˜(𝑖 + 1)))
316 neqne 2952 . . . . . . . . . . . . . 14 (Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)) β†’ (π‘†β€˜(𝑗 + 1)) β‰  (π‘„β€˜(𝑖 + 1)))
317316necomd 3000 . . . . . . . . . . . . 13 (Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)) β†’ (π‘„β€˜(𝑖 + 1)) β‰  (π‘†β€˜(𝑗 + 1)))
318317adantl 483 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘„β€˜(𝑖 + 1)) β‰  (π‘†β€˜(𝑗 + 1)))
319308, 313, 315, 318leneltd 11316 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘†β€˜(𝑗 + 1)) < (π‘„β€˜(𝑖 + 1)))
320306, 307, 308, 312, 319eliood 43810 . . . . . . . . . 10 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (π‘†β€˜(𝑗 + 1)) ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
321230, 90readdcld 11191 . . . . . . . . . . . 12 (πœ’ β†’ (𝑋 + (π‘†β€˜(𝑗 + 1))) ∈ ℝ)
322276, 321ffvelcdmd 7041 . . . . . . . . . . 11 (πœ’ β†’ (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1)))) ∈ ℝ)
323322adantr 482 . . . . . . . . . 10 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1)))) ∈ ℝ)
324302, 305, 320, 323fvmptd 6960 . . . . . . . . 9 ((πœ’ ∧ Β¬ (π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1))) β†’ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜(𝑗 + 1))) = (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1)))))
325324ifeq2da 4523 . . . . . . . 8 (πœ’ β†’ if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜(𝑗 + 1)))) = if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1))))))
326298resmptd 5999 . . . . . . . . 9 (πœ’ β†’ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))))
327326oveq1d 7377 . . . . . . . 8 (πœ’ β†’ (((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜(𝑗 + 1))) = ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
328301, 325, 3273eltr3d 2852 . . . . . . 7 (πœ’ β†’ if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1))))) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
329 ax-resscn 11115 . . . . . . . . 9 ℝ βŠ† β„‚
330128, 329sstrdi 3961 . . . . . . . 8 (πœ’ β†’ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† β„‚)
33190recnd 11190 . . . . . . . 8 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ∈ β„‚)
332168, 330, 124, 331constlimc 43939 . . . . . . 7 (πœ’ β†’ 𝐢 ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝐢) limβ„‚ (π‘†β€˜(𝑗 + 1))))
333167, 168, 161, 121, 125, 328, 332sublimc 43967 . . . . . 6 (πœ’ β†’ (if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1))))) βˆ’ 𝐢) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) limβ„‚ (π‘†β€˜(𝑗 + 1))))
334330, 162, 331idlimc 43941 . . . . . 6 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝑠) limβ„‚ (π‘†β€˜(𝑗 + 1))))
3356, 105jca 513 . . . . . . 7 (πœ’ β†’ (πœ‘ ∧ (π‘†β€˜(𝑗 + 1)) ∈ (𝐴[,]𝐡)))
336 eleq1 2826 . . . . . . . . . 10 (𝑠 = (π‘†β€˜(𝑗 + 1)) β†’ (𝑠 ∈ (𝐴[,]𝐡) ↔ (π‘†β€˜(𝑗 + 1)) ∈ (𝐴[,]𝐡)))
337336anbi2d 630 . . . . . . . . 9 (𝑠 = (π‘†β€˜(𝑗 + 1)) β†’ ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) ↔ (πœ‘ ∧ (π‘†β€˜(𝑗 + 1)) ∈ (𝐴[,]𝐡))))
338 neeq1 3007 . . . . . . . . 9 (𝑠 = (π‘†β€˜(𝑗 + 1)) β†’ (𝑠 β‰  0 ↔ (π‘†β€˜(𝑗 + 1)) β‰  0))
339337, 338imbi12d 345 . . . . . . . 8 (𝑠 = (π‘†β€˜(𝑗 + 1)) β†’ (((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ 𝑠 β‰  0) ↔ ((πœ‘ ∧ (π‘†β€˜(𝑗 + 1)) ∈ (𝐴[,]𝐡)) β†’ (π‘†β€˜(𝑗 + 1)) β‰  0)))
340339, 140vtoclg 3528 . . . . . . 7 ((π‘†β€˜(𝑗 + 1)) ∈ ℝ β†’ ((πœ‘ ∧ (π‘†β€˜(𝑗 + 1)) ∈ (𝐴[,]𝐡)) β†’ (π‘†β€˜(𝑗 + 1)) β‰  0))
34190, 335, 340sylc 65 . . . . . 6 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) β‰  0)
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 43971 . . . . 5 (πœ’ β†’ ((if((π‘†β€˜(𝑗 + 1)) = (π‘„β€˜(𝑖 + 1)), 𝐿, (πΉβ€˜(𝑋 + (π‘†β€˜(𝑗 + 1))))) βˆ’ 𝐢) / (π‘†β€˜(𝑗 + 1))) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠)) limβ„‚ (π‘†β€˜(𝑗 + 1))))
343 eqid 2737 . . . . . 6 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2))))
344143, 150mulcld 11182 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ β„‚)
345159neneqd 2949 . . . . . . . 8 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ Β¬ (2 Β· (sinβ€˜(𝑠 / 2))) = 0)
346 2re 12234 . . . . . . . . . . 11 2 ∈ ℝ
347346a1i 11 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 2 ∈ ℝ)
34817rehalfcld 12407 . . . . . . . . . . . 12 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) β†’ (𝑠 / 2) ∈ ℝ)
349348resincld 16032 . . . . . . . . . . 11 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) β†’ (sinβ€˜(𝑠 / 2)) ∈ ℝ)
350349adantl 483 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (sinβ€˜(𝑠 / 2)) ∈ ℝ)
351347, 350remulcld 11192 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ ℝ)
352 elsng 4605 . . . . . . . . 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 325 . . . . . . 7 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ Β¬ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ {0})
355344, 354eldifd 3926 . . . . . 6 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ (β„‚ βˆ– {0}))
356 eqid 2737 . . . . . . 7 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 2)
357 eqid 2737 . . . . . . 7 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (sinβ€˜(𝑠 / 2))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (sinβ€˜(𝑠 / 2)))
358 2cnd 12238 . . . . . . . 8 (πœ’ β†’ 2 ∈ β„‚)
359356, 330, 358, 331constlimc 43939 . . . . . . 7 (πœ’ β†’ 2 ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 2) limβ„‚ (π‘†β€˜(𝑗 + 1))))
360348ad2antrl 727 . . . . . . . 8 ((πœ’ ∧ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ∧ (𝑠 / 2) β‰  ((π‘†β€˜(𝑗 + 1)) / 2))) β†’ (𝑠 / 2) ∈ ℝ)
361 recn 11148 . . . . . . . . . 10 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ β„‚)
362361sincld 16019 . . . . . . . . 9 (π‘₯ ∈ ℝ β†’ (sinβ€˜π‘₯) ∈ β„‚)
363362adantl 483 . . . . . . . 8 ((πœ’ ∧ π‘₯ ∈ ℝ) β†’ (sinβ€˜π‘₯) ∈ β„‚)
364 eqid 2737 . . . . . . . . 9 (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / 2))
365 2cn 12235 . . . . . . . . . . 11 2 ∈ β„‚
366 eldifsn 4752 . . . . . . . . . . 11 (2 ∈ (β„‚ βˆ– {0}) ↔ (2 ∈ β„‚ ∧ 2 β‰  0))
367365, 151, 366mpbir2an 710 . . . . . . . . . 10 2 ∈ (β„‚ βˆ– {0})
368367a1i 11 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 2 ∈ (β„‚ βˆ– {0}))
369151a1i 11 . . . . . . . . 9 (πœ’ β†’ 2 β‰  0)
370162, 356, 364, 148, 368, 334, 359, 369, 152divlimc 43971 . . . . . . . 8 (πœ’ β†’ ((π‘†β€˜(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / 2)) limβ„‚ (π‘†β€˜(𝑗 + 1))))
371 sinf 16013 . . . . . . . . . . . . . 14 sin:β„‚βŸΆβ„‚
372371a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ sin:β„‚βŸΆβ„‚)
373329a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ ℝ βŠ† β„‚)
374372, 373feqresmpt 6916 . . . . . . . . . . . 12 (⊀ β†’ (sin β†Ύ ℝ) = (π‘₯ ∈ ℝ ↦ (sinβ€˜π‘₯)))
375374mptru 1549 . . . . . . . . . . 11 (sin β†Ύ ℝ) = (π‘₯ ∈ ℝ ↦ (sinβ€˜π‘₯))
376 resincncf 44190 . . . . . . . . . . 11 (sin β†Ύ ℝ) ∈ (ℝ–cn→ℝ)
377375, 376eqeltrri 2835 . . . . . . . . . 10 (π‘₯ ∈ ℝ ↦ (sinβ€˜π‘₯)) ∈ (ℝ–cn→ℝ)
378377a1i 11 . . . . . . . . 9 (πœ’ β†’ (π‘₯ ∈ ℝ ↦ (sinβ€˜π‘₯)) ∈ (ℝ–cn→ℝ))
37990rehalfcld 12407 . . . . . . . . 9 (πœ’ β†’ ((π‘†β€˜(𝑗 + 1)) / 2) ∈ ℝ)
380 fveq2 6847 . . . . . . . . 9 (π‘₯ = ((π‘†β€˜(𝑗 + 1)) / 2) β†’ (sinβ€˜π‘₯) = (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)))
381378, 379, 380cnmptlimc 25270 . . . . . . . 8 (πœ’ β†’ (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)) ∈ ((π‘₯ ∈ ℝ ↦ (sinβ€˜π‘₯)) limβ„‚ ((π‘†β€˜(𝑗 + 1)) / 2)))
382 fveq2 6847 . . . . . . . 8 (π‘₯ = (𝑠 / 2) β†’ (sinβ€˜π‘₯) = (sinβ€˜(𝑠 / 2)))
383 fveq2 6847 . . . . . . . . 9 ((𝑠 / 2) = ((π‘†β€˜(𝑗 + 1)) / 2) β†’ (sinβ€˜(𝑠 / 2)) = (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)))
384383ad2antll 728 . . . . . . . 8 ((πœ’ ∧ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ∧ (𝑠 / 2) = ((π‘†β€˜(𝑗 + 1)) / 2))) β†’ (sinβ€˜(𝑠 / 2)) = (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)))
385360, 363, 370, 381, 382, 384limcco 25273 . . . . . . 7 (πœ’ β†’ (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (sinβ€˜(𝑠 / 2))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
386356, 357, 343, 143, 150, 359, 385mullimc 43931 . . . . . 6 (πœ’ β†’ (2 Β· (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
387331halfcld 12405 . . . . . . . 8 (πœ’ β†’ ((π‘†β€˜(𝑗 + 1)) / 2) ∈ β„‚)
388387sincld 16019 . . . . . . 7 (πœ’ β†’ (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)) ∈ β„‚)
389154, 105sseldd 3950 . . . . . . . 8 (πœ’ β†’ (π‘†β€˜(𝑗 + 1)) ∈ (-Ο€[,]Ο€))
390 fourierdlem44 44466 . . . . . . . 8 (((π‘†β€˜(𝑗 + 1)) ∈ (-Ο€[,]Ο€) ∧ (π‘†β€˜(𝑗 + 1)) β‰  0) β†’ (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)) β‰  0)
391389, 341, 390syl2anc 585 . . . . . . 7 (πœ’ β†’ (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)) β‰  0)
392358, 388, 369, 391mulne0d 11814 . . . . . 6 (πœ’ β†’ (2 Β· (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2))) β‰  0)
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 43971 . . . . 5 (πœ’ β†’ ((π‘†β€˜(𝑗 + 1)) / (2 Β· (sinβ€˜((π‘†β€˜(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
3942, 3, 4, 142, 160, 342, 393mullimc 43931 . . . 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 5938 . . . . . 6 (𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))))
399 ioossicc 13357 . . . . . . . 8 ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘†β€˜π‘—)[,](π‘†β€˜(𝑗 + 1)))
400 iccss 13339 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ (𝐴 ≀ (π‘†β€˜π‘—) ∧ (π‘†β€˜(𝑗 + 1)) ≀ 𝐡)) β†’ ((π‘†β€˜π‘—)[,](π‘†β€˜(𝑗 + 1))) βŠ† (𝐴[,]𝐡))
40119, 98, 85, 107, 400syl22anc 838 . . . . . . . 8 (πœ’ β†’ ((π‘†β€˜π‘—)[,](π‘†β€˜(𝑗 + 1))) βŠ† (𝐴[,]𝐡))
402399, 401sstrid 3960 . . . . . . 7 (πœ’ β†’ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† (𝐴[,]𝐡))
403402resmptd 5999 . . . . . 6 (πœ’ β†’ ((𝑠 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
404398, 403eqtrid 2789 . . . . 5 (πœ’ β†’ (𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
405404oveq1d 7377 . . . 4 (πœ’ β†’ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜(𝑗 + 1))) = ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
406394, 396, 4053eltr4d 2853 . . 3 (πœ’ β†’ 𝐷 ∈ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
4071, 406sylbir 234 . 2 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝐷 ∈ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
408242, 249gtned 11297 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 β‰  (π‘„β€˜π‘–))
409 fourierdlem76.r . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
4106, 223, 409syl2anc 585 . . . . . . . . . . 11 (πœ’ β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
411240oveq2d 7378 . . . . . . . . . . 11 (πœ’ β†’ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (𝑋 + (π‘„β€˜π‘–))))
412410, 411eleqtrd 2840 . . . . . . . . . 10 (πœ’ β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (𝑋 + (π‘„β€˜π‘–))))
413193recnd 11190 . . . . . . . . . 10 (πœ’ β†’ (π‘„β€˜π‘–) ∈ β„‚)
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 44474 . . . . . . . . 9 (πœ’ β†’ 𝑅 ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘„β€˜π‘–)))
415 eqid 2737 . . . . . . . . 9 if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜π‘—))) = if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜π‘—)))
416 eqid 2737 . . . . . . . . 9 ((TopOpenβ€˜β„‚fld) β†Ύt ((π‘„β€˜π‘–)[,)(π‘„β€˜(𝑖 + 1)))) = ((TopOpenβ€˜β„‚fld) β†Ύt ((π‘„β€˜π‘–)[,)(π‘„β€˜(𝑖 + 1))))
417193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416fourierdlem32 44454 . . . . . . . 8 (πœ’ β†’ if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜π‘—))) ∈ (((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜π‘—)))
418 eqidd 2738 . . . . . . . . . 10 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))))
419 oveq2 7370 . . . . . . . . . . . 12 (𝑠 = (π‘†β€˜π‘—) β†’ (𝑋 + 𝑠) = (𝑋 + (π‘†β€˜π‘—)))
420419fveq2d 6851 . . . . . . . . . . 11 (𝑠 = (π‘†β€˜π‘—) β†’ (πΉβ€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + (π‘†β€˜π‘—))))
421420adantl 483 . . . . . . . . . 10 (((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) ∧ 𝑠 = (π‘†β€˜π‘—)) β†’ (πΉβ€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + (π‘†β€˜π‘—))))
422243adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘„β€˜π‘–) ∈ ℝ*)
423245adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ*)
424290adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘†β€˜π‘—) ∈ ℝ)
425193adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘„β€˜π‘–) ∈ ℝ)
426310adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘„β€˜π‘–) ≀ (π‘†β€˜π‘—))
427 neqne 2952 . . . . . . . . . . . . 13 (Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–) β†’ (π‘†β€˜π‘—) β‰  (π‘„β€˜π‘–))
428427adantl 483 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘†β€˜π‘—) β‰  (π‘„β€˜π‘–))
429425, 424, 426, 428leneltd 11316 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘„β€˜π‘–) < (π‘†β€˜π‘—))
43090adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘†β€˜(𝑗 + 1)) ∈ ℝ)
431211adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
432297adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝑗 + 1)))
433314adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘†β€˜(𝑗 + 1)) ≀ (π‘„β€˜(𝑖 + 1)))
434424, 430, 431, 432, 433ltletrd 11322 . . . . . . . . . . 11 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘†β€˜π‘—) < (π‘„β€˜(𝑖 + 1)))
435422, 423, 424, 429, 434eliood 43810 . . . . . . . . . 10 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (π‘†β€˜π‘—) ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
436230, 290readdcld 11191 . . . . . . . . . . . 12 (πœ’ β†’ (𝑋 + (π‘†β€˜π‘—)) ∈ ℝ)
437276, 436ffvelcdmd 7041 . . . . . . . . . . 11 (πœ’ β†’ (πΉβ€˜(𝑋 + (π‘†β€˜π‘—))) ∈ ℝ)
438437adantr 482 . . . . . . . . . 10 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ (πΉβ€˜(𝑋 + (π‘†β€˜π‘—))) ∈ ℝ)
439418, 421, 435, 438fvmptd 6960 . . . . . . . . 9 ((πœ’ ∧ Β¬ (π‘†β€˜π‘—) = (π‘„β€˜π‘–)) β†’ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜π‘—)) = (πΉβ€˜(𝑋 + (π‘†β€˜π‘—))))
440439ifeq2da 4523 . . . . . . . 8 (πœ’ β†’ if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))β€˜(π‘†β€˜π‘—))) = if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, (πΉβ€˜(𝑋 + (π‘†β€˜π‘—)))))
441326oveq1d 7377 . . . . . . . 8 (πœ’ β†’ (((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜π‘—)) = ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘†β€˜π‘—)))
442417, 440, 4413eltr3d 2852 . . . . . . 7 (πœ’ β†’ if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, (πΉβ€˜(𝑋 + (π‘†β€˜π‘—)))) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘†β€˜π‘—)))
443290recnd 11190 . . . . . . . 8 (πœ’ β†’ (π‘†β€˜π‘—) ∈ β„‚)
444168, 330, 124, 443constlimc 43939 . . . . . . 7 (πœ’ β†’ 𝐢 ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝐢) limβ„‚ (π‘†β€˜π‘—)))
445167, 168, 161, 121, 125, 442, 444sublimc 43967 . . . . . 6 (πœ’ β†’ (if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, (πΉβ€˜(𝑋 + (π‘†β€˜π‘—)))) βˆ’ 𝐢) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) limβ„‚ (π‘†β€˜π‘—)))
446330, 162, 443idlimc 43941 . . . . . 6 (πœ’ β†’ (π‘†β€˜π‘—) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝑠) limβ„‚ (π‘†β€˜π‘—)))
4476, 83jca 513 . . . . . . 7 (πœ’ β†’ (πœ‘ ∧ (π‘†β€˜π‘—) ∈ (𝐴[,]𝐡)))
448 eleq1 2826 . . . . . . . . . 10 (𝑠 = (π‘†β€˜π‘—) β†’ (𝑠 ∈ (𝐴[,]𝐡) ↔ (π‘†β€˜π‘—) ∈ (𝐴[,]𝐡)))
449448anbi2d 630 . . . . . . . . 9 (𝑠 = (π‘†β€˜π‘—) β†’ ((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) ↔ (πœ‘ ∧ (π‘†β€˜π‘—) ∈ (𝐴[,]𝐡))))
450 neeq1 3007 . . . . . . . . 9 (𝑠 = (π‘†β€˜π‘—) β†’ (𝑠 β‰  0 ↔ (π‘†β€˜π‘—) β‰  0))
451449, 450imbi12d 345 . . . . . . . 8 (𝑠 = (π‘†β€˜π‘—) β†’ (((πœ‘ ∧ 𝑠 ∈ (𝐴[,]𝐡)) β†’ 𝑠 β‰  0) ↔ ((πœ‘ ∧ (π‘†β€˜π‘—) ∈ (𝐴[,]𝐡)) β†’ (π‘†β€˜π‘—) β‰  0)))
452451, 140vtoclg 3528 . . . . . . 7 ((π‘†β€˜π‘—) ∈ (𝐴[,]𝐡) β†’ ((πœ‘ ∧ (π‘†β€˜π‘—) ∈ (𝐴[,]𝐡)) β†’ (π‘†β€˜π‘—) β‰  0))
45383, 447, 452sylc 65 . . . . . 6 (πœ’ β†’ (π‘†β€˜π‘—) β‰  0)
454161, 162, 2, 126, 166, 445, 446, 453, 141divlimc 43971 . . . . 5 (πœ’ β†’ ((if((π‘†β€˜π‘—) = (π‘„β€˜π‘–), 𝑅, (πΉβ€˜(𝑋 + (π‘†β€˜π‘—)))) βˆ’ 𝐢) / (π‘†β€˜π‘—)) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠)) limβ„‚ (π‘†β€˜π‘—)))
455356, 330, 358, 443constlimc 43939 . . . . . . 7 (πœ’ β†’ 2 ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 2) limβ„‚ (π‘†β€˜π‘—)))
456348ad2antrl 727 . . . . . . . 8 ((πœ’ ∧ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ∧ (𝑠 / 2) β‰  ((π‘†β€˜π‘—) / 2))) β†’ (𝑠 / 2) ∈ ℝ)
457162, 356, 364, 148, 368, 446, 455, 369, 152divlimc 43971 . . . . . . . 8 (πœ’ β†’ ((π‘†β€˜π‘—) / 2) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / 2)) limβ„‚ (π‘†β€˜π‘—)))
458290rehalfcld 12407 . . . . . . . . 9 (πœ’ β†’ ((π‘†β€˜π‘—) / 2) ∈ ℝ)
459 fveq2 6847 . . . . . . . . 9 (π‘₯ = ((π‘†β€˜π‘—) / 2) β†’ (sinβ€˜π‘₯) = (sinβ€˜((π‘†β€˜π‘—) / 2)))
460378, 458, 459cnmptlimc 25270 . . . . . . . 8 (πœ’ β†’ (sinβ€˜((π‘†β€˜π‘—) / 2)) ∈ ((π‘₯ ∈ ℝ ↦ (sinβ€˜π‘₯)) limβ„‚ ((π‘†β€˜π‘—) / 2)))
461 fveq2 6847 . . . . . . . . 9 ((𝑠 / 2) = ((π‘†β€˜π‘—) / 2) β†’ (sinβ€˜(𝑠 / 2)) = (sinβ€˜((π‘†β€˜π‘—) / 2)))
462461ad2antll 728 . . . . . . . 8 ((πœ’ ∧ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ∧ (𝑠 / 2) = ((π‘†β€˜π‘—) / 2))) β†’ (sinβ€˜(𝑠 / 2)) = (sinβ€˜((π‘†β€˜π‘—) / 2)))
463456, 363, 457, 460, 382, 462limcco 25273 . . . . . . 7 (πœ’ β†’ (sinβ€˜((π‘†β€˜π‘—) / 2)) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (sinβ€˜(𝑠 / 2))) limβ„‚ (π‘†β€˜π‘—)))
464356, 357, 343, 143, 150, 455, 463mullimc 43931 . . . . . 6 (πœ’ β†’ (2 Β· (sinβ€˜((π‘†β€˜π‘—) / 2))) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) limβ„‚ (π‘†β€˜π‘—)))
465443halfcld 12405 . . . . . . . 8 (πœ’ β†’ ((π‘†β€˜π‘—) / 2) ∈ β„‚)
466465sincld 16019 . . . . . . 7 (πœ’ β†’ (sinβ€˜((π‘†β€˜π‘—) / 2)) ∈ β„‚)
467154, 83sseldd 3950 . . . . . . . 8 (πœ’ β†’ (π‘†β€˜π‘—) ∈ (-Ο€[,]Ο€))
468 fourierdlem44 44466 . . . . . . . 8 (((π‘†β€˜π‘—) ∈ (-Ο€[,]Ο€) ∧ (π‘†β€˜π‘—) β‰  0) β†’ (sinβ€˜((π‘†β€˜π‘—) / 2)) β‰  0)
469467, 453, 468syl2anc 585 . . . . . . 7 (πœ’ β†’ (sinβ€˜((π‘†β€˜π‘—) / 2)) β‰  0)
470358, 466, 369, 469mulne0d 11814 . . . . . 6 (πœ’ β†’ (2 Β· (sinβ€˜((π‘†β€˜π‘—) / 2))) β‰  0)
471162, 343, 3, 148, 355, 446, 464, 470, 159divlimc 43971 . . . . 5 (πœ’ β†’ ((π‘†β€˜π‘—) / (2 Β· (sinβ€˜((π‘†β€˜π‘—) / 2)))) ∈ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) limβ„‚ (π‘†β€˜π‘—)))
4722, 3, 4, 142, 160, 454, 471mullimc 43931 . . . 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 7377 . . . 4 (πœ’ β†’ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜π‘—)) = ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) limβ„‚ (π‘†β€˜π‘—)))
476472, 474, 4753eltr4d 2853 . . 3 (πœ’ β†’ 𝐸 ∈ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜π‘—)))
4771, 476sylbir 234 . 2 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝐸 ∈ ((𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜π‘—)))
478298sselda 3949 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
479478, 266syldan 592 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠)))
480479mpteq2dva 5210 . . . . . . . 8 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠))))
481225adantr 482 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘‰β€˜π‘–) ∈ ℝ*)
482228adantr 482 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ*)
483230adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑋 ∈ ℝ)
484483, 129readdcld 11191 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑋 + 𝑠) ∈ ℝ)
485240adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘‰β€˜π‘–) = (𝑋 + (π‘„β€˜π‘–)))
486193adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘„β€˜π‘–) ∈ ℝ)
487243adantr 482 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘„β€˜π‘–) ∈ ℝ*)
488245adantr 482 . . . . . . . . . . . . 13 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ*)
489487, 488, 478, 248syl3anc 1372 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘„β€˜π‘–) < 𝑠)
490486, 18, 483, 489ltadd2dd 11321 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑋 + (π‘„β€˜π‘–)) < (𝑋 + 𝑠))
491485, 490eqbrtrd 5132 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘‰β€˜π‘–) < (𝑋 + 𝑠))
492211adantr 482 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
493487, 488, 478, 253syl3anc 1372 . . . . . . . . . . . 12 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ 𝑠 < (π‘„β€˜(𝑖 + 1)))
49418, 492, 483, 493ltadd2dd 11321 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑋 + 𝑠) < (𝑋 + (π‘„β€˜(𝑖 + 1))))
495260adantr 482 . . . . . . . . . . 11 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑋 + (π‘„β€˜(𝑖 + 1))) = (π‘‰β€˜(𝑖 + 1)))
496494, 495breqtrd 5136 . . . . . . . . . 10 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑋 + 𝑠) < (π‘‰β€˜(𝑖 + 1)))
497481, 482, 484, 491, 496eliood 43810 . . . . . . . . 9 ((πœ’ ∧ 𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) β†’ (𝑋 + 𝑠) ∈ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))
498269, 271, 330, 237, 497fourierdlem23 44445 . . . . . . . 8 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))β€˜(𝑋 + 𝑠))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
499480, 498eqeltrd 2838 . . . . . . 7 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
500 ssid 3971 . . . . . . . . 9 β„‚ βŠ† β„‚
501500a1i 11 . . . . . . . 8 (πœ’ β†’ β„‚ βŠ† β„‚)
502330, 124, 501constcncfg 44187 . . . . . . 7 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝐢) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
503499, 502subcncf 24825 . . . . . 6 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
504166ralrimiva 3144 . . . . . . . 8 (πœ’ β†’ βˆ€π‘  ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))𝑠 ∈ (β„‚ βˆ– {0}))
505 dfss3 3937 . . . . . . . 8 (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† (β„‚ βˆ– {0}) ↔ βˆ€π‘  ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))𝑠 ∈ (β„‚ βˆ– {0}))
506504, 505sylibr 233 . . . . . . 7 (πœ’ β†’ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† (β„‚ βˆ– {0}))
507 difssd 4097 . . . . . . 7 (πœ’ β†’ (β„‚ βˆ– {0}) βŠ† β„‚)
508506, 507idcncfg 44188 . . . . . 6 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝑠) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’(β„‚ βˆ– {0})))
509503, 508divcncf 24827 . . . . 5 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠)) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
510330, 501idcncfg 44188 . . . . . 6 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 𝑠) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
511355, 343fmptd 7067 . . . . . . 7 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))):((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))⟢(β„‚ βˆ– {0}))
512330, 358, 501constcncfg 44187 . . . . . . . . 9 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 2) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
513 sincn 25819 . . . . . . . . . . 11 sin ∈ (ℂ–cnβ†’β„‚)
514513a1i 11 . . . . . . . . . 10 (πœ’ β†’ sin ∈ (ℂ–cnβ†’β„‚))
515367a1i 11 . . . . . . . . . . . 12 (πœ’ β†’ 2 ∈ (β„‚ βˆ– {0}))
516330, 515, 507constcncfg 44187 . . . . . . . . . . 11 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ 2) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’(β„‚ βˆ– {0})))
517510, 516divcncf 24827 . . . . . . . . . 10 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
518514, 517cncfmpt1f 24293 . . . . . . . . 9 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (sinβ€˜(𝑠 / 2))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
519512, 518mulcncf 24826 . . . . . . . 8 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
520 cncfcdm 24277 . . . . . . . 8 (((β„‚ βˆ– {0}) βŠ† β„‚ ∧ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚)) β†’ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’(β„‚ βˆ– {0})) ↔ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))):((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))⟢(β„‚ βˆ– {0})))
521507, 519, 520syl2anc 585 . . . . . . 7 (πœ’ β†’ ((𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’(β„‚ βˆ– {0})) ↔ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))):((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))⟢(β„‚ βˆ– {0})))
522511, 521mpbird 257 . . . . . 6 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’(β„‚ βˆ– {0})))
523510, 522divcncf 24827 . . . . 5 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
524509, 523mulcncf 24826 . . . 4 (πœ’ β†’ (𝑠 ∈ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) ↦ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) Β· (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
525404, 524eqeltrd 2838 . . 3 (πœ’ β†’ (𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
5261, 525sylbir 234 . 2 ((((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1))) βŠ† ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑂 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
527407, 477, 526jca31 516 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 205   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  {crab 3410   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  ifcif 4491  {csn 4591  {cpr 4593   class class class wbr 5110   ↦ cmpt 5193  dom cdm 5638  ran crn 5639   β†Ύ cres 5640  β„©cio 6451  Fun wfun 6495  βŸΆwf 6497  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501   Isom wiso 6502  (class class class)co 7362   ↑m cmap 8772  Fincfn 8890  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  -cneg 11393   / cdiv 11819  β„•cn 12160  2c2 12215  β„€cz 12506  (,)cioo 13271  [,)cico 13273  [,]cicc 13274  ...cfz 13431  ..^cfzo 13574  β™―chash 14237  sincsin 15953  Ο€cpi 15956   β†Ύt crest 17309  TopOpenctopn 17310  β„‚fldccnfld 20812  β€“cnβ†’ccncf 24255   limβ„‚ climc 25242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-pi 15962  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247
This theorem is referenced by:  fourierdlem86  44507
  Copyright terms: Public domain W3C validator