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

Theorem fourierdlem95 45217
Description: Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem95.f (πœ‘ β†’ 𝐹:β„βŸΆβ„)
fourierdlem95.xre (πœ‘ β†’ 𝑋 ∈ ℝ)
fourierdlem95.p 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (-Ο€ + 𝑋) ∧ (π‘β€˜π‘š) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem95.m (πœ‘ β†’ 𝑀 ∈ β„•)
fourierdlem95.v (πœ‘ β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
fourierdlem95.x (πœ‘ β†’ 𝑋 ∈ ran 𝑉)
fourierdlem95.fcn ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
fourierdlem95.r ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
fourierdlem95.l ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
fourierdlem95.h 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
fourierdlem95.k 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
fourierdlem95.u π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
fourierdlem95.s 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑛 + (1 / 2)) Β· 𝑠)))
fourierdlem95.g 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
fourierdlem95.i 𝐼 = (ℝ D 𝐹)
fourierdlem95.ifn ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐼 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„)
fourierdlem95.b (πœ‘ β†’ 𝐡 ∈ ((𝐼 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
fourierdlem95.c (πœ‘ β†’ 𝐢 ∈ ((𝐼 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
fourierdlem95.y (πœ‘ β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
fourierdlem95.w (πœ‘ β†’ π‘Š ∈ ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
fourierdlem95.admvol (πœ‘ β†’ 𝐴 ∈ dom vol)
fourierdlem95.ass (πœ‘ β†’ 𝐴 βŠ† ((-Ο€[,]Ο€) βˆ– {0}))
fourierlemenplusacver2eqitgdirker.e 𝐸 = (𝑛 ∈ β„• ↦ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
fourierdlem95.d 𝐷 = (𝑛 ∈ β„• ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 Β· Ο€)) = 0, (((2 Β· 𝑛) + 1) / (2 Β· Ο€)), ((sinβ€˜((𝑛 + (1 / 2)) Β· 𝑠)) / ((2 Β· Ο€) Β· (sinβ€˜(𝑠 / 2)))))))
fourierdlem95.o (πœ‘ β†’ 𝑂 ∈ ℝ)
fourierdlem95.ifeqo ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = 𝑂)
fourierdlem95.itgdirker ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠 = (1 / 2))
Assertion
Ref Expression
fourierdlem95 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΈβ€˜π‘›) + (𝑂 / 2)) = ∫𝐴((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
Distinct variable groups:   𝐴,𝑠   𝐡,𝑠   𝐢,𝑠   𝐷,𝑠   𝐹,𝑠   𝑖,𝐺,𝑠   𝐻,𝑠   𝐾,𝑠   𝐿,𝑠   𝑖,𝑀,𝑝,π‘š   𝑀,𝑠   𝑂,𝑠   𝑅,𝑠   𝑆,𝑠   𝑖,𝑉,𝑝   𝑉,𝑠   π‘Š,𝑠   𝑖,𝑋,𝑝,π‘š   𝑋,𝑠   π‘Œ,𝑠   𝑖,𝑛,𝑠   πœ‘,𝑖,𝑠
Allowed substitution hints:   πœ‘(π‘š,𝑛,𝑝)   𝐴(𝑖,π‘š,𝑛,𝑝)   𝐡(𝑖,π‘š,𝑛,𝑝)   𝐢(𝑖,π‘š,𝑛,𝑝)   𝐷(𝑖,π‘š,𝑛,𝑝)   𝑃(𝑖,π‘š,𝑛,𝑠,𝑝)   𝑅(𝑖,π‘š,𝑛,𝑝)   𝑆(𝑖,π‘š,𝑛,𝑝)   π‘ˆ(𝑖,π‘š,𝑛,𝑠,𝑝)   𝐸(𝑖,π‘š,𝑛,𝑠,𝑝)   𝐹(𝑖,π‘š,𝑛,𝑝)   𝐺(π‘š,𝑛,𝑝)   𝐻(𝑖,π‘š,𝑛,𝑝)   𝐼(𝑖,π‘š,𝑛,𝑠,𝑝)   𝐾(𝑖,π‘š,𝑛,𝑝)   𝐿(𝑖,π‘š,𝑛,𝑝)   𝑀(𝑛)   𝑂(𝑖,π‘š,𝑛,𝑝)   𝑉(π‘š,𝑛)   π‘Š(𝑖,π‘š,𝑛,𝑝)   𝑋(𝑛)   π‘Œ(𝑖,π‘š,𝑛,𝑝)

Proof of Theorem fourierdlem95
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 simpr 484 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
2 fourierdlem95.ass . . . . . . . . . 10 (πœ‘ β†’ 𝐴 βŠ† ((-Ο€[,]Ο€) βˆ– {0}))
32difss2d 4135 . . . . . . . . 9 (πœ‘ β†’ 𝐴 βŠ† (-Ο€[,]Ο€))
43adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† (-Ο€[,]Ο€))
54sselda 3983 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
6 fourierdlem95.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
76adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐹:β„βŸΆβ„)
8 fourierdlem95.xre . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ℝ)
98adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑋 ∈ ℝ)
10 ioossre 13390 . . . . . . . . . . . . 13 (𝑋(,)+∞) βŠ† ℝ
1110a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋(,)+∞) βŠ† ℝ)
126, 11fssresd 6759 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (𝑋(,)+∞)):(𝑋(,)+∞)βŸΆβ„)
13 ioosscn 13391 . . . . . . . . . . . 12 (𝑋(,)+∞) βŠ† β„‚
1413a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑋(,)+∞) βŠ† β„‚)
15 eqid 2731 . . . . . . . . . . . 12 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
16 pnfxr 11273 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
1716a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ +∞ ∈ ℝ*)
188ltpnfd 13106 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 < +∞)
1915, 17, 8, 18lptioo1cn 44662 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝑋(,)+∞)))
20 fourierdlem95.y . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
2112, 14, 19, 20limcrecl 44645 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ ℝ)
2221adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Œ ∈ ℝ)
23 ioossre 13390 . . . . . . . . . . . . 13 (-∞(,)𝑋) βŠ† ℝ
2423a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (-∞(,)𝑋) βŠ† ℝ)
256, 24fssresd 6759 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (-∞(,)𝑋)):(-∞(,)𝑋)βŸΆβ„)
26 ioosscn 13391 . . . . . . . . . . . 12 (-∞(,)𝑋) βŠ† β„‚
2726a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (-∞(,)𝑋) βŠ† β„‚)
28 mnfxr 11276 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
2928a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ ∈ ℝ*)
308mnfltd 13109 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ < 𝑋)
3115, 29, 8, 30lptioo2cn 44661 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(-∞(,)𝑋)))
32 fourierdlem95.w . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
3325, 27, 31, 32limcrecl 44645 . . . . . . . . . 10 (πœ‘ β†’ π‘Š ∈ ℝ)
3433adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Š ∈ ℝ)
35 fourierdlem95.h . . . . . . . . 9 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
36 fourierdlem95.k . . . . . . . . 9 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
37 fourierdlem95.u . . . . . . . . 9 π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
381nnred 12232 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ ℝ)
39 fourierdlem95.s . . . . . . . . 9 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑛 + (1 / 2)) Β· 𝑠)))
40 fourierdlem95.g . . . . . . . . 9 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
417, 9, 22, 34, 35, 36, 37, 38, 39, 40fourierdlem67 45189 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺:(-Ο€[,]Ο€)βŸΆβ„)
4241ffvelcdmda 7087 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (πΊβ€˜π‘ ) ∈ ℝ)
435, 42syldan 590 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) ∈ ℝ)
44 fourierdlem95.admvol . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ dom vol)
4544adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 ∈ dom vol)
4641feqmptd 6961 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (πΊβ€˜π‘ )))
47 fourierdlem95.p . . . . . . . . 9 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (-Ο€ + 𝑋) ∧ (π‘β€˜π‘š) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
48 fourierdlem95.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ran 𝑉)
4948adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑋 ∈ ran 𝑉)
5020adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
5132adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Š ∈ ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
52 fourierdlem95.m . . . . . . . . . 10 (πœ‘ β†’ 𝑀 ∈ β„•)
5352adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑀 ∈ β„•)
54 fourierdlem95.v . . . . . . . . . 10 (πœ‘ β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
5554adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
56 fourierdlem95.fcn . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
5756adantlr 712 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
58 fourierdlem95.r . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
5958adantlr 712 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
60 fourierdlem95.l . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
6160adantlr 712 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
62 fveq2 6892 . . . . . . . . . . 11 (𝑗 = 𝑖 β†’ (π‘‰β€˜π‘—) = (π‘‰β€˜π‘–))
6362oveq1d 7427 . . . . . . . . . 10 (𝑗 = 𝑖 β†’ ((π‘‰β€˜π‘—) βˆ’ 𝑋) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
6463cbvmptv 5262 . . . . . . . . 9 (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋)) = (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
65 eqid 2731 . . . . . . . . 9 (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = -Ο€ ∧ (π‘β€˜π‘š) = Ο€) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))}) = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = -Ο€ ∧ (π‘β€˜π‘š) = Ο€) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
66 fourierdlem95.i . . . . . . . . 9 𝐼 = (ℝ D 𝐹)
67 fourierdlem95.ifn . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐼 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„)
6867adantlr 712 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐼 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„)
69 fourierdlem95.b . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ ((𝐼 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
7069adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐡 ∈ ((𝐼 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
71 fourierdlem95.c . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ ((𝐼 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
7271adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐢 ∈ ((𝐼 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
7347, 7, 49, 50, 51, 35, 36, 37, 38, 39, 40, 53, 55, 57, 59, 61, 64, 65, 66, 68, 70, 72fourierdlem88 45210 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺 ∈ 𝐿1)
7446, 73eqeltrrd 2833 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ (πΊβ€˜π‘ )) ∈ 𝐿1)
754, 45, 42, 74iblss 25555 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (πΊβ€˜π‘ )) ∈ 𝐿1)
7643, 75itgrecl 25548 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(πΊβ€˜π‘ ) d𝑠 ∈ ℝ)
77 pire 26201 . . . . . 6 Ο€ ∈ ℝ
7877a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ ℝ)
79 pipos 26203 . . . . . . 7 0 < Ο€
8077, 79gt0ne0ii 11755 . . . . . 6 Ο€ β‰  0
8180a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ β‰  0)
8276, 78, 81redivcld 12047 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) ∈ ℝ)
83 fourierlemenplusacver2eqitgdirker.e . . . . 5 𝐸 = (𝑛 ∈ β„• ↦ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
8483fvmpt2 7010 . . . 4 ((𝑛 ∈ β„• ∧ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) ∈ ℝ) β†’ (πΈβ€˜π‘›) = (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
851, 82, 84syl2anc 583 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΈβ€˜π‘›) = (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
86 fourierdlem95.o . . . . . . 7 (πœ‘ β†’ 𝑂 ∈ ℝ)
8786recnd 11247 . . . . . 6 (πœ‘ β†’ 𝑂 ∈ β„‚)
88 2cnd 12295 . . . . . 6 (πœ‘ β†’ 2 ∈ β„‚)
89 2ne0 12321 . . . . . . 7 2 β‰  0
9089a1i 11 . . . . . 6 (πœ‘ β†’ 2 β‰  0)
9187, 88, 90divrecd 11998 . . . . 5 (πœ‘ β†’ (𝑂 / 2) = (𝑂 Β· (1 / 2)))
9291adantr 480 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 / 2) = (𝑂 Β· (1 / 2)))
93 fourierdlem95.itgdirker . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠 = (1 / 2))
9493eqcomd 2737 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1 / 2) = ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)
9594oveq2d 7428 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 Β· (1 / 2)) = (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠))
9692, 95eqtrd 2771 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 / 2) = (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠))
9785, 96oveq12d 7430 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΈβ€˜π‘›) + (𝑂 / 2)) = ((∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) + (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)))
982sselda 3983 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ((-Ο€[,]Ο€) βˆ– {0}))
9998adantlr 712 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ((-Ο€[,]Ο€) βˆ– {0}))
100 fourierdlem95.d . . . . . . . 8 𝐷 = (𝑛 ∈ β„• ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 Β· Ο€)) = 0, (((2 Β· 𝑛) + 1) / (2 Β· Ο€)), ((sinβ€˜((𝑛 + (1 / 2)) Β· 𝑠)) / ((2 Β· Ο€) Β· (sinβ€˜(𝑠 / 2)))))))
101 eqid 2731 . . . . . . . 8 ((-Ο€[,]Ο€) βˆ– {0}) = ((-Ο€[,]Ο€) βˆ– {0})
1026, 8, 21, 33, 100, 35, 36, 37, 39, 40, 101fourierdlem66 45188 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ ((-Ο€[,]Ο€) βˆ– {0})) β†’ (πΊβ€˜π‘ ) = (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
10399, 102syldan 590 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) = (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
104103itgeq2dv 25532 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(πΊβ€˜π‘ ) d𝑠 = ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠)
105104oveq1d 7427 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) = (∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 / Ο€))
10678recnd 11247 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ β„‚)
1076adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝐹:β„βŸΆβ„)
1088adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑋 ∈ ℝ)
109 difss 4132 . . . . . . . . . . . . . 14 ((-Ο€[,]Ο€) βˆ– {0}) βŠ† (-Ο€[,]Ο€)
11077renegcli 11526 . . . . . . . . . . . . . . 15 -Ο€ ∈ ℝ
111 iccssre 13411 . . . . . . . . . . . . . . 15 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ) β†’ (-Ο€[,]Ο€) βŠ† ℝ)
112110, 77, 111mp2an 689 . . . . . . . . . . . . . 14 (-Ο€[,]Ο€) βŠ† ℝ
113109, 112sstri 3992 . . . . . . . . . . . . 13 ((-Ο€[,]Ο€) βˆ– {0}) βŠ† ℝ
114113, 98sselid 3981 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ℝ)
115108, 114readdcld 11248 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (𝑋 + 𝑠) ∈ ℝ)
116107, 115ffvelcdmd 7088 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
11721, 33ifcld 4575 . . . . . . . . . . 11 (πœ‘ β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
118117adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
119116, 118resubcld 11647 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
120119adantlr 712 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
1211adantr 480 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑛 ∈ β„•)
122114adantlr 712 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ℝ)
123100dirkerre 45111 . . . . . . . . 9 ((𝑛 ∈ β„• ∧ 𝑠 ∈ ℝ) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
124121, 122, 123syl2anc 583 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
125120, 124remulcld 11249 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ ℝ)
126103eqcomd 2737 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (πΊβ€˜π‘ ))
127126oveq1d 7427 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) / Ο€) = ((πΊβ€˜π‘ ) / Ο€))
128 picn 26202 . . . . . . . . . . . . 13 Ο€ ∈ β„‚
129128a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ Ο€ ∈ β„‚)
130125recnd 11247 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
13180a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ Ο€ β‰  0)
132129, 130, 129, 131div23d 12032 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) / Ο€) = ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
13343recnd 11247 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) ∈ β„‚)
134133, 129, 131divrec2d 11999 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΊβ€˜π‘ ) / Ο€) = ((1 / Ο€) Β· (πΊβ€˜π‘ )))
135127, 132, 1343eqtr3rd 2780 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((1 / Ο€) Β· (πΊβ€˜π‘ )) = ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
136128, 80dividi 11952 . . . . . . . . . . . 12 (Ο€ / Ο€) = 1
137136a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (Ο€ / Ο€) = 1)
138137oveq1d 7427 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (1 Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
139130mullidd 11237 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (1 Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )))
140135, 138, 1393eqtrrd 2776 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) = ((1 / Ο€) Β· (πΊβ€˜π‘ )))
141140mpteq2dva 5249 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (𝑠 ∈ 𝐴 ↦ ((1 / Ο€) Β· (πΊβ€˜π‘ ))))
142106, 81reccld 11988 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1 / Ο€) ∈ β„‚)
143142, 43, 75iblmulc2 25581 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ ((1 / Ο€) Β· (πΊβ€˜π‘ ))) ∈ 𝐿1)
144141, 143eqeltrd 2832 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) ∈ 𝐿1)
145106, 125, 144itgmulc2 25584 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) = ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠)
146145eqcomd 2737 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 = (Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
147146oveq1d 7427 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 / Ο€) = ((Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) / Ο€))
148125, 144itgcl 25534 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 ∈ β„‚)
149148, 106, 81divcan3d 12000 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) / Ο€) = ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
150105, 147, 1493eqtrd 2775 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) = ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
15187adantr 480 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑂 ∈ β„‚)
152112sseli 3979 . . . . . . 7 (𝑠 ∈ (-Ο€[,]Ο€) β†’ 𝑠 ∈ ℝ)
153152, 123sylan2 592 . . . . . 6 ((𝑛 ∈ β„• ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
154153adantll 711 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
155110a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ -Ο€ ∈ ℝ)
156 ax-resscn 11170 . . . . . . . . . 10 ℝ βŠ† β„‚
157156a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ ℝ βŠ† β„‚)
158 ssid 4005 . . . . . . . . 9 β„‚ βŠ† β„‚
159 cncfss 24640 . . . . . . . . 9 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
160157, 158, 159sylancl 585 . . . . . . . 8 (𝑛 ∈ β„• β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
161 eqid 2731 . . . . . . . . 9 (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )) = (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ ))
162100dirkerf 45113 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ (π·β€˜π‘›):β„βŸΆβ„)
163162feqmptd 6961 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (π·β€˜π‘›) = (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )))
164100dirkercncf 45123 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (π·β€˜π‘›) ∈ (ℝ–cn→ℝ))
165163, 164eqeltrrd 2833 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ (ℝ–cn→ℝ))
166112a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (-Ο€[,]Ο€) βŠ† ℝ)
167 ssid 4005 . . . . . . . . . 10 ℝ βŠ† ℝ
168167a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ ℝ βŠ† ℝ)
169161, 165, 166, 168, 153cncfmptssg 44887 . . . . . . . 8 (𝑛 ∈ β„• β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
170160, 169sseldd 3984 . . . . . . 7 (𝑛 ∈ β„• β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
171170adantl 481 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
172 cniccibl 25591 . . . . . 6 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ ∧ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚)) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
173155, 78, 171, 172syl3anc 1370 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
1744, 45, 154, 173iblss 25555 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
175151, 124, 174itgmulc2 25584 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠) = ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
176150, 175oveq12d 7430 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) + (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)) = (∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 + ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
17786ad2antrr 723 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 ∈ ℝ)
178177, 124remulcld 11249 . . . 4 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ ℝ)
179151, 124, 174iblmulc2 25581 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) ∈ 𝐿1)
180125, 144, 178, 179itgadd 25575 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 = (∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 + ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
181 fourierdlem95.ifeqo . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = 𝑂)
182181eqcomd 2737 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 = if(0 < 𝑠, π‘Œ, π‘Š))
183182adantlr 712 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 = if(0 < 𝑠, π‘Œ, π‘Š))
184183oveq1d 7427 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) = (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ )))
185184oveq2d 7428 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
186116recnd 11247 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
187186adantlr 712 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
188118recnd 11247 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
189188adantlr 712 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
190124recnd 11247 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ β„‚)
191187, 189, 190subdird 11676 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) = (((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
192191oveq1d 7427 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
193187, 190mulcld 11239 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
194189, 190mulcld 11239 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
195193, 194npcand 11580 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )))
196185, 192, 1953eqtrd 2775 . . . 4 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )))
197196itgeq2dv 25532 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 = ∫𝐴((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
198180, 197eqtr3d 2773 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 + ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) = ∫𝐴((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
19997, 176, 1983eqtrd 2775 1 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΈβ€˜π‘›) + (𝑂 / 2)) = ∫𝐴((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  {crab 3431   βˆ– cdif 3946   βŠ† wss 3949  ifcif 4529  {csn 4629   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   β†Ύ cres 5679  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7412   ↑m cmap 8823  β„‚cc 11111  β„cr 11112  0cc0 11113  1c1 11114   + caddc 11116   Β· cmul 11118  +∞cpnf 11250  -∞cmnf 11251  β„*cxr 11252   < clt 11253   βˆ’ cmin 11449  -cneg 11450   / cdiv 11876  β„•cn 12217  2c2 12272  (,)cioo 13329  [,]cicc 13332  ...cfz 13489  ..^cfzo 13632   mod cmo 13839  sincsin 16012  Ο€cpi 16015  TopOpenctopn 17372  β„‚fldccnfld 21145  β€“cnβ†’ccncf 24617  volcvol 25213  πΏ1cibl 25367  βˆ«citg 25368   limβ„‚ climc 25612   D cdv 25613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-inf2 9639  ax-cc 10433  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191  ax-addf 11192  ax-mulf 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-symdif 4243  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7673  df-ofr 7674  df-om 7859  df-1st 7978  df-2nd 7979  df-supp 8150  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-2o 8470  df-oadd 8473  df-omul 8474  df-er 8706  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9365  df-fi 9409  df-sup 9440  df-inf 9441  df-oi 9508  df-dju 9899  df-card 9937  df-acn 9940  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-z 12564  df-dec 12683  df-uz 12828  df-q 12938  df-rp 12980  df-xneg 13097  df-xadd 13098  df-xmul 13099  df-ioo 13333  df-ioc 13334  df-ico 13335  df-icc 13336  df-fz 13490  df-fzo 13633  df-fl 13762  df-mod 13840  df-seq 13972  df-exp 14033  df-fac 14239  df-bc 14268  df-hash 14296  df-shft 15019  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-limsup 15420  df-clim 15437  df-rlim 15438  df-sum 15638  df-ef 16016  df-sin 16018  df-cos 16019  df-pi 16021  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-rest 17373  df-topn 17374  df-0g 17392  df-gsum 17393  df-topgen 17394  df-pt 17395  df-prds 17398  df-xrs 17453  df-qtop 17458  df-imas 17459  df-xps 17461  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-submnd 18707  df-mulg 18988  df-cntz 19223  df-cmn 19692  df-psmet 21137  df-xmet 21138  df-met 21139  df-bl 21140  df-mopn 21141  df-fbas 21142  df-fg 21143  df-cnfld 21146  df-top 22617  df-topon 22634  df-topsp 22656  df-bases 22670  df-cld 22744  df-ntr 22745  df-cls 22746  df-nei 22823  df-lp 22861  df-perf 22862  df-cn 22952  df-cnp 22953  df-t1 23039  df-haus 23040  df-cmp 23112  df-tx 23287  df-hmeo 23480  df-fil 23571  df-fm 23663  df-flim 23664  df-flf 23665  df-xms 24047  df-ms 24048  df-tms 24049  df-cncf 24619  df-ovol 25214  df-vol 25215  df-mbf 25369  df-itg1 25370  df-itg2 25371  df-ibl 25372  df-itg 25373  df-0p 25420  df-limc 25616  df-dv 25617
This theorem is referenced by:  fourierdlem103  45225  fourierdlem104  45226
  Copyright terms: Public domain W3C validator