Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem85 Structured version   Visualization version   GIF version

Theorem fourierdlem85 45205
Description: Limit of the function 𝐺 at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem85.p 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (-Ο€ + 𝑋) ∧ (π‘β€˜π‘š) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem85.f (πœ‘ β†’ 𝐹:β„βŸΆβ„)
fourierdlem85.x (πœ‘ β†’ 𝑋 ∈ ran 𝑉)
fourierdlem85.y (πœ‘ β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
fourierdlem85.w (πœ‘ β†’ π‘Š ∈ ℝ)
fourierdlem85.h 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
fourierdlem85.k 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
fourierdlem85.u π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
fourierdlem85.n (πœ‘ β†’ 𝑁 ∈ ℝ)
fourierdlem85.s 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
fourierdlem85.g 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
fourierdlem85.m (πœ‘ β†’ 𝑀 ∈ β„•)
fourierdlem85.v (πœ‘ β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
fourierdlem85.r ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
fourierdlem85.q 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
fourierdlem85.o 𝑂 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = -Ο€ ∧ (π‘β€˜π‘š) = Ο€) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem85.i 𝐼 = (ℝ D 𝐹)
fourierdlem85.ifn ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐼 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„‚)
fourierdlem85.e (πœ‘ β†’ 𝐸 ∈ ((𝐼 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
fourierdlem85.a 𝐴 = ((if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) Β· (πΎβ€˜(π‘„β€˜π‘–))) Β· (π‘†β€˜(π‘„β€˜π‘–)))
Assertion
Ref Expression
fourierdlem85 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐴 ∈ ((𝐺 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
Distinct variable groups:   𝐸,𝑠   𝐹,𝑠   𝐻,𝑠   𝐾,𝑠   𝑖,𝑀,π‘š,𝑝   𝑀,𝑠,𝑖   𝑁,𝑠   𝑄,𝑖,𝑝   𝑄,𝑠   𝑅,𝑠   𝑆,𝑠   𝑖,𝑉,𝑝   𝑉,𝑠   π‘Š,𝑠   𝑖,𝑋,π‘š,𝑝   𝑋,𝑠   π‘Œ,𝑠   πœ‘,𝑖,𝑠
Allowed substitution hints:   πœ‘(π‘š,𝑝)   𝐴(𝑖,π‘š,𝑠,𝑝)   𝑃(𝑖,π‘š,𝑠,𝑝)   𝑄(π‘š)   𝑅(𝑖,π‘š,𝑝)   𝑆(𝑖,π‘š,𝑝)   π‘ˆ(𝑖,π‘š,𝑠,𝑝)   𝐸(𝑖,π‘š,𝑝)   𝐹(𝑖,π‘š,𝑝)   𝐺(𝑖,π‘š,𝑠,𝑝)   𝐻(𝑖,π‘š,𝑝)   𝐼(𝑖,π‘š,𝑠,𝑝)   𝐾(𝑖,π‘š,𝑝)   𝑁(𝑖,π‘š,𝑝)   𝑂(𝑖,π‘š,𝑠,𝑝)   𝑉(π‘š)   π‘Š(𝑖,π‘š,𝑝)   π‘Œ(𝑖,π‘š,𝑝)

Proof of Theorem fourierdlem85
StepHypRef Expression
1 fourierdlem85.a . . 3 𝐴 = ((if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) Β· (πΎβ€˜(π‘„β€˜π‘–))) Β· (π‘†β€˜(π‘„β€˜π‘–)))
2 eqid 2730 . . . 4 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘ˆβ€˜π‘ )) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘ˆβ€˜π‘ ))
3 eqid 2730 . . . 4 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘†β€˜π‘ )) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘†β€˜π‘ ))
4 eqid 2730 . . . 4 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
5 pire 26204 . . . . . . . . . . 11 Ο€ ∈ ℝ
65renegcli 11525 . . . . . . . . . 10 -Ο€ ∈ ℝ
76rexri 11276 . . . . . . . . 9 -Ο€ ∈ ℝ*
87a1i 11 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ -Ο€ ∈ ℝ*)
95rexri 11276 . . . . . . . . 9 Ο€ ∈ ℝ*
109a1i 11 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Ο€ ∈ ℝ*)
11 fourierdlem85.o . . . . . . . . . . 11 𝑂 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = -Ο€ ∧ (π‘β€˜π‘š) = Ο€) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
12 fourierdlem85.m . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ β„•)
135a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ Ο€ ∈ ℝ)
1413renegcld 11645 . . . . . . . . . . . 12 (πœ‘ β†’ -Ο€ ∈ ℝ)
15 fourierdlem85.v . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
16 fourierdlem85.p . . . . . . . . . . . . . . . . . 18 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (-Ο€ + 𝑋) ∧ (π‘β€˜π‘š) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
1716fourierdlem2 45123 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ β„• β†’ (𝑉 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘‰β€˜0) = (-Ο€ + 𝑋) ∧ (π‘‰β€˜π‘€) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1))))))
1812, 17syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑉 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘‰β€˜0) = (-Ο€ + 𝑋) ∧ (π‘‰β€˜π‘€) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1))))))
1915, 18mpbid 231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘‰β€˜0) = (-Ο€ + 𝑋) ∧ (π‘‰β€˜π‘€) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1)))))
2019simpld 493 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑉 ∈ (ℝ ↑m (0...𝑀)))
21 elmapi 8845 . . . . . . . . . . . . . 14 (𝑉 ∈ (ℝ ↑m (0...𝑀)) β†’ 𝑉:(0...𝑀)βŸΆβ„)
22 frn 6723 . . . . . . . . . . . . . 14 (𝑉:(0...𝑀)βŸΆβ„ β†’ ran 𝑉 βŠ† ℝ)
2320, 21, 223syl 18 . . . . . . . . . . . . 13 (πœ‘ β†’ ran 𝑉 βŠ† ℝ)
24 fourierdlem85.x . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 ∈ ran 𝑉)
2523, 24sseldd 3982 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ ℝ)
26 fourierdlem85.q . . . . . . . . . . . 12 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
2714, 13, 25, 16, 11, 12, 15, 26fourierdlem14 45135 . . . . . . . . . . 11 (πœ‘ β†’ 𝑄 ∈ (π‘‚β€˜π‘€))
2811, 12, 27fourierdlem15 45136 . . . . . . . . . 10 (πœ‘ β†’ 𝑄:(0...𝑀)⟢(-Ο€[,]Ο€))
2928adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑄:(0...𝑀)⟢(-Ο€[,]Ο€))
3029adantr 479 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑄:(0...𝑀)⟢(-Ο€[,]Ο€))
31 simplr 765 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑖 ∈ (0..^𝑀))
328, 10, 30, 31fourierdlem8 45129 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1))) βŠ† (-Ο€[,]Ο€))
33 ioossicc 13414 . . . . . . . . 9 ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1)))
3433sseli 3977 . . . . . . . 8 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) β†’ 𝑠 ∈ ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1))))
3534adantl 480 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1))))
3632, 35sseldd 3982 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
37 fourierdlem85.f . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
38 ioossre 13389 . . . . . . . . . . . . . 14 (𝑋(,)+∞) βŠ† ℝ
3938a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑋(,)+∞) βŠ† ℝ)
4037, 39fssresd 6757 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 β†Ύ (𝑋(,)+∞)):(𝑋(,)+∞)βŸΆβ„)
41 ax-resscn 11169 . . . . . . . . . . . . 13 ℝ βŠ† β„‚
4239, 41sstrdi 3993 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋(,)+∞) βŠ† β„‚)
43 eqid 2730 . . . . . . . . . . . . 13 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
44 pnfxr 11272 . . . . . . . . . . . . . 14 +∞ ∈ ℝ*
4544a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ +∞ ∈ ℝ*)
4625ltpnfd 13105 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 < +∞)
4743, 45, 25, 46lptioo1cn 44660 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝑋(,)+∞)))
48 fourierdlem85.y . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
4940, 42, 47, 48limcrecl 44643 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ ℝ)
50 fourierdlem85.w . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ ℝ)
51 fourierdlem85.h . . . . . . . . . . 11 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
5237, 25, 49, 50, 51fourierdlem9 45130 . . . . . . . . . 10 (πœ‘ β†’ 𝐻:(-Ο€[,]Ο€)βŸΆβ„)
5341a1i 11 . . . . . . . . . 10 (πœ‘ β†’ ℝ βŠ† β„‚)
5452, 53fssd 6734 . . . . . . . . 9 (πœ‘ β†’ 𝐻:(-Ο€[,]Ο€)βŸΆβ„‚)
5554ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝐻:(-Ο€[,]Ο€)βŸΆβ„‚)
5655, 36ffvelcdmd 7086 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π»β€˜π‘ ) ∈ β„‚)
57 fourierdlem85.k . . . . . . . . . . 11 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
5857fourierdlem43 45164 . . . . . . . . . 10 𝐾:(-Ο€[,]Ο€)βŸΆβ„
5958a1i 11 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝐾:(-Ο€[,]Ο€)βŸΆβ„)
6059, 36ffvelcdmd 7086 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΎβ€˜π‘ ) ∈ ℝ)
6160recnd 11246 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΎβ€˜π‘ ) ∈ β„‚)
6256, 61mulcld 11238 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ β„‚)
63 fourierdlem85.u . . . . . . 7 π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
6463fvmpt2 7008 . . . . . 6 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ β„‚) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
6536, 62, 64syl2anc 582 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
6665, 62eqeltrd 2831 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘ˆβ€˜π‘ ) ∈ β„‚)
67 fourierdlem85.n . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ ℝ)
68 fourierdlem85.s . . . . . . . . . 10 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
6967, 68fourierdlem18 45139 . . . . . . . . 9 (πœ‘ β†’ 𝑆 ∈ ((-Ο€[,]Ο€)–cn→ℝ))
70 cncff 24633 . . . . . . . . 9 (𝑆 ∈ ((-Ο€[,]Ο€)–cn→ℝ) β†’ 𝑆:(-Ο€[,]Ο€)βŸΆβ„)
7169, 70syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑆:(-Ο€[,]Ο€)βŸΆβ„)
7271adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑆:(-Ο€[,]Ο€)βŸΆβ„)
7372adantr 479 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑆:(-Ο€[,]Ο€)βŸΆβ„)
7473, 36ffvelcdmd 7086 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘†β€˜π‘ ) ∈ ℝ)
7574recnd 11246 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘†β€˜π‘ ) ∈ β„‚)
76 eqid 2730 . . . . . 6 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π»β€˜π‘ )) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π»β€˜π‘ ))
77 eqid 2730 . . . . . 6 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΎβ€˜π‘ )) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΎβ€˜π‘ ))
78 eqid 2730 . . . . . 6 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
79 fourierdlem85.r . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
80 fourierdlem85.i . . . . . . . 8 𝐼 = (ℝ D 𝐹)
81 fourierdlem85.ifn . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐼 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„‚)
82 fourierdlem85.e . . . . . . . 8 (πœ‘ β†’ 𝐸 ∈ ((𝐼 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
83 eqid 2730 . . . . . . . 8 if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) = if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–)))
8425, 16, 37, 24, 48, 50, 51, 12, 15, 79, 26, 11, 80, 81, 82, 83fourierdlem75 45195 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) ∈ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
8552adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐻:(-Ο€[,]Ο€)βŸΆβ„)
867a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ -Ο€ ∈ ℝ*)
879a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ Ο€ ∈ ℝ*)
88 simpr 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑖 ∈ (0..^𝑀))
8986, 87, 29, 88fourierdlem8 45129 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1))) βŠ† (-Ο€[,]Ο€))
9033, 89sstrid 3992 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† (-Ο€[,]Ο€))
9185, 90feqresmpt 6960 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π»β€˜π‘ )))
9291oveq1d 7426 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)) = ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π»β€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)))
9384, 92eleqtrd 2833 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π»β€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)))
94 limcresi 25634 . . . . . . . 8 (𝐾 limβ„‚ (π‘„β€˜π‘–)) βŠ† ((𝐾 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–))
95 ssid 4003 . . . . . . . . . . . 12 β„‚ βŠ† β„‚
96 cncfss 24639 . . . . . . . . . . . 12 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
9741, 95, 96mp2an 688 . . . . . . . . . . 11 ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚)
9857fourierdlem62 45182 . . . . . . . . . . 11 𝐾 ∈ ((-Ο€[,]Ο€)–cn→ℝ)
9997, 98sselii 3978 . . . . . . . . . 10 𝐾 ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚)
10099a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐾 ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
101 elfzofz 13652 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) β†’ 𝑖 ∈ (0...𝑀))
102101adantl 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑖 ∈ (0...𝑀))
10329, 102ffvelcdmd 7086 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) ∈ (-Ο€[,]Ο€))
104100, 103cnlimci 25638 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (πΎβ€˜(π‘„β€˜π‘–)) ∈ (𝐾 limβ„‚ (π‘„β€˜π‘–)))
10594, 104sselid 3979 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (πΎβ€˜(π‘„β€˜π‘–)) ∈ ((𝐾 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
106 cncff 24633 . . . . . . . . . 10 (𝐾 ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚) β†’ 𝐾:(-Ο€[,]Ο€)βŸΆβ„‚)
10799, 106mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐾:(-Ο€[,]Ο€)βŸΆβ„‚)
108107, 90feqresmpt 6960 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐾 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΎβ€˜π‘ )))
109108oveq1d 7426 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐾 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)) = ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΎβ€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)))
110105, 109eleqtrd 2833 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (πΎβ€˜(π‘„β€˜π‘–)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΎβ€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)))
11176, 77, 78, 56, 61, 93, 110mullimc 44630 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) Β· (πΎβ€˜(π‘„β€˜π‘–))) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) limβ„‚ (π‘„β€˜π‘–)))
11265mpteq2dva 5247 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘ˆβ€˜π‘ )) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))))
113112oveq1d 7426 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘ˆβ€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)) = ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) limβ„‚ (π‘„β€˜π‘–)))
114111, 113eleqtrrd 2834 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) Β· (πΎβ€˜(π‘„β€˜π‘–))) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘ˆβ€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)))
115 limcresi 25634 . . . . . 6 (𝑆 limβ„‚ (π‘„β€˜π‘–)) βŠ† ((𝑆 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–))
11669adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑆 ∈ ((-Ο€[,]Ο€)–cn→ℝ))
117116, 103cnlimci 25638 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘†β€˜(π‘„β€˜π‘–)) ∈ (𝑆 limβ„‚ (π‘„β€˜π‘–)))
118115, 117sselid 3979 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘†β€˜(π‘„β€˜π‘–)) ∈ ((𝑆 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
11972, 90feqresmpt 6960 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑆 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘†β€˜π‘ )))
120119oveq1d 7426 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝑆 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)) = ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘†β€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)))
121118, 120eleqtrd 2833 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘†β€˜(π‘„β€˜π‘–)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π‘†β€˜π‘ )) limβ„‚ (π‘„β€˜π‘–)))
1222, 3, 4, 66, 75, 114, 121mullimc 44630 . . 3 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((if((π‘‰β€˜π‘–) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜π‘–) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜π‘–))) Β· (πΎβ€˜(π‘„β€˜π‘–))) Β· (π‘†β€˜(π‘„β€˜π‘–))) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) limβ„‚ (π‘„β€˜π‘–)))
1231, 122eqeltrid 2835 . 2 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐴 ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) limβ„‚ (π‘„β€˜π‘–)))
124 fourierdlem85.g . . . . 5 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
125124reseq1i 5976 . . . 4 (𝐺 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
12690resmptd 6039 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))))
127125, 126eqtr2id 2783 . . 3 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) = (𝐺 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))))
128127oveq1d 7426 . 2 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) limβ„‚ (π‘„β€˜π‘–)) = ((𝐺 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
129123, 128eleqtrd 2833 1 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐴 ∈ ((𝐺 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  {crab 3430   βŠ† wss 3947  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230  ran crn 5676   β†Ύ cres 5677  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ↑m cmap 8822  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  +∞cpnf 11249  β„*cxr 11251   < clt 11252   βˆ’ cmin 11448  -cneg 11449   / cdiv 11875  β„•cn 12216  2c2 12271  (,)cioo 13328  [,]cicc 13331  ...cfz 13488  ..^cfzo 13631  sincsin 16011  Ο€cpi 16014  TopOpenctopn 17371  β„‚fldccnfld 21144  β€“cnβ†’ccncf 24616   limβ„‚ climc 25611   D cdv 25612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ioc 13333  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-fac 14238  df-bc 14267  df-hash 14295  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637  df-ef 16015  df-sin 16017  df-cos 16018  df-pi 16020  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-hom 17225  df-cco 17226  df-rest 17372  df-topn 17373  df-0g 17391  df-gsum 17392  df-topgen 17393  df-pt 17394  df-prds 17397  df-xrs 17452  df-qtop 17457  df-imas 17458  df-xps 17460  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-mulg 18987  df-cntz 19222  df-cmn 19691  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-cnfld 21145  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-lp 22860  df-perf 22861  df-cn 22951  df-cnp 22952  df-t1 23038  df-haus 23039  df-cmp 23111  df-tx 23286  df-hmeo 23479  df-fil 23570  df-fm 23662  df-flim 23663  df-flf 23664  df-xms 24046  df-ms 24047  df-tms 24048  df-cncf 24618  df-limc 25615  df-dv 25616
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator