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 45002
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 485 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
2 fourierdlem95.ass . . . . . . . . . 10 (πœ‘ β†’ 𝐴 βŠ† ((-Ο€[,]Ο€) βˆ– {0}))
32difss2d 4134 . . . . . . . . 9 (πœ‘ β†’ 𝐴 βŠ† (-Ο€[,]Ο€))
43adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† (-Ο€[,]Ο€))
54sselda 3982 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
6 fourierdlem95.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
76adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐹:β„βŸΆβ„)
8 fourierdlem95.xre . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ℝ)
98adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑋 ∈ ℝ)
10 ioossre 13387 . . . . . . . . . . . . 13 (𝑋(,)+∞) βŠ† ℝ
1110a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋(,)+∞) βŠ† ℝ)
126, 11fssresd 6758 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (𝑋(,)+∞)):(𝑋(,)+∞)βŸΆβ„)
13 ioosscn 13388 . . . . . . . . . . . 12 (𝑋(,)+∞) βŠ† β„‚
1413a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑋(,)+∞) βŠ† β„‚)
15 eqid 2732 . . . . . . . . . . . 12 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
16 pnfxr 11270 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
1716a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ +∞ ∈ ℝ*)
188ltpnfd 13103 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 < +∞)
1915, 17, 8, 18lptioo1cn 44447 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝑋(,)+∞)))
20 fourierdlem95.y . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
2112, 14, 19, 20limcrecl 44430 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ ℝ)
2221adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Œ ∈ ℝ)
23 ioossre 13387 . . . . . . . . . . . . 13 (-∞(,)𝑋) βŠ† ℝ
2423a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (-∞(,)𝑋) βŠ† ℝ)
256, 24fssresd 6758 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (-∞(,)𝑋)):(-∞(,)𝑋)βŸΆβ„)
26 ioosscn 13388 . . . . . . . . . . . 12 (-∞(,)𝑋) βŠ† β„‚
2726a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (-∞(,)𝑋) βŠ† β„‚)
28 mnfxr 11273 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
2928a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ ∈ ℝ*)
308mnfltd 13106 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ < 𝑋)
3115, 29, 8, 30lptioo2cn 44446 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(-∞(,)𝑋)))
32 fourierdlem95.w . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
3325, 27, 31, 32limcrecl 44430 . . . . . . . . . 10 (πœ‘ β†’ π‘Š ∈ ℝ)
3433adantr 481 . . . . . . . . 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 12229 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ ℝ)
39 fourierdlem95.s . . . . . . . . 9 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑛 + (1 / 2)) Β· 𝑠)))
40 fourierdlem95.g . . . . . . . . 9 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
417, 9, 22, 34, 35, 36, 37, 38, 39, 40fourierdlem67 44974 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺:(-Ο€[,]Ο€)βŸΆβ„)
4241ffvelcdmda 7086 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (πΊβ€˜π‘ ) ∈ ℝ)
435, 42syldan 591 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) ∈ ℝ)
44 fourierdlem95.admvol . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ dom vol)
4544adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 ∈ dom vol)
4641feqmptd 6960 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (πΊβ€˜π‘ )))
47 fourierdlem95.p . . . . . . . . 9 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (-Ο€ + 𝑋) ∧ (π‘β€˜π‘š) = (Ο€ + 𝑋)) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
48 fourierdlem95.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ran 𝑉)
4948adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑋 ∈ ran 𝑉)
5020adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
5132adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Š ∈ ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
52 fourierdlem95.m . . . . . . . . . 10 (πœ‘ β†’ 𝑀 ∈ β„•)
5352adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑀 ∈ β„•)
54 fourierdlem95.v . . . . . . . . . 10 (πœ‘ β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
5554adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑉 ∈ (π‘ƒβ€˜π‘€))
56 fourierdlem95.fcn . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
5756adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) ∈ (((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))–cnβ†’β„‚))
58 fourierdlem95.r . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
5958adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜π‘–)))
60 fourierdlem95.l . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
6160adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
62 fveq2 6891 . . . . . . . . . . 11 (𝑗 = 𝑖 β†’ (π‘‰β€˜π‘—) = (π‘‰β€˜π‘–))
6362oveq1d 7426 . . . . . . . . . 10 (𝑗 = 𝑖 β†’ ((π‘‰β€˜π‘—) βˆ’ 𝑋) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
6463cbvmptv 5261 . . . . . . . . 9 (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋)) = (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
65 eqid 2732 . . . . . . . . 9 (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = -Ο€ ∧ (π‘β€˜π‘š) = Ο€) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))}) = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = -Ο€ ∧ (π‘β€˜π‘š) = Ο€) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
66 fourierdlem95.i . . . . . . . . 9 𝐼 = (ℝ D 𝐹)
67 fourierdlem95.ifn . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐼 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„)
6867adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐼 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„)
69 fourierdlem95.b . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ ((𝐼 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
7069adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐡 ∈ ((𝐼 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
71 fourierdlem95.c . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ ((𝐼 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
7271adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐢 ∈ ((𝐼 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
7347, 7, 49, 50, 51, 35, 36, 37, 38, 39, 40, 53, 55, 57, 59, 61, 64, 65, 66, 68, 70, 72fourierdlem88 44995 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺 ∈ 𝐿1)
7446, 73eqeltrrd 2834 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ (πΊβ€˜π‘ )) ∈ 𝐿1)
754, 45, 42, 74iblss 25329 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (πΊβ€˜π‘ )) ∈ 𝐿1)
7643, 75itgrecl 25322 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(πΊβ€˜π‘ ) d𝑠 ∈ ℝ)
77 pire 25975 . . . . . 6 Ο€ ∈ ℝ
7877a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ ℝ)
79 pipos 25977 . . . . . . 7 0 < Ο€
8077, 79gt0ne0ii 11752 . . . . . 6 Ο€ β‰  0
8180a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ β‰  0)
8276, 78, 81redivcld 12044 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) ∈ ℝ)
83 fourierlemenplusacver2eqitgdirker.e . . . . 5 𝐸 = (𝑛 ∈ β„• ↦ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
8483fvmpt2 7009 . . . 4 ((𝑛 ∈ β„• ∧ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) ∈ ℝ) β†’ (πΈβ€˜π‘›) = (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
851, 82, 84syl2anc 584 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΈβ€˜π‘›) = (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
86 fourierdlem95.o . . . . . . 7 (πœ‘ β†’ 𝑂 ∈ ℝ)
8786recnd 11244 . . . . . 6 (πœ‘ β†’ 𝑂 ∈ β„‚)
88 2cnd 12292 . . . . . 6 (πœ‘ β†’ 2 ∈ β„‚)
89 2ne0 12318 . . . . . . 7 2 β‰  0
9089a1i 11 . . . . . 6 (πœ‘ β†’ 2 β‰  0)
9187, 88, 90divrecd 11995 . . . . 5 (πœ‘ β†’ (𝑂 / 2) = (𝑂 Β· (1 / 2)))
9291adantr 481 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 / 2) = (𝑂 Β· (1 / 2)))
93 fourierdlem95.itgdirker . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠 = (1 / 2))
9493eqcomd 2738 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1 / 2) = ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)
9594oveq2d 7427 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 Β· (1 / 2)) = (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠))
9692, 95eqtrd 2772 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 / 2) = (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠))
9785, 96oveq12d 7429 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΈβ€˜π‘›) + (𝑂 / 2)) = ((∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) + (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)))
982sselda 3982 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ((-Ο€[,]Ο€) βˆ– {0}))
9998adantlr 713 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ((-Ο€[,]Ο€) βˆ– {0}))
100 fourierdlem95.d . . . . . . . 8 𝐷 = (𝑛 ∈ β„• ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 Β· Ο€)) = 0, (((2 Β· 𝑛) + 1) / (2 Β· Ο€)), ((sinβ€˜((𝑛 + (1 / 2)) Β· 𝑠)) / ((2 Β· Ο€) Β· (sinβ€˜(𝑠 / 2)))))))
101 eqid 2732 . . . . . . . 8 ((-Ο€[,]Ο€) βˆ– {0}) = ((-Ο€[,]Ο€) βˆ– {0})
1026, 8, 21, 33, 100, 35, 36, 37, 39, 40, 101fourierdlem66 44973 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ ((-Ο€[,]Ο€) βˆ– {0})) β†’ (πΊβ€˜π‘ ) = (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
10399, 102syldan 591 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) = (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
104103itgeq2dv 25306 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(πΊβ€˜π‘ ) d𝑠 = ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠)
105104oveq1d 7426 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) = (∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 / Ο€))
10678recnd 11244 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ β„‚)
1076adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝐹:β„βŸΆβ„)
1088adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑋 ∈ ℝ)
109 difss 4131 . . . . . . . . . . . . . 14 ((-Ο€[,]Ο€) βˆ– {0}) βŠ† (-Ο€[,]Ο€)
11077renegcli 11523 . . . . . . . . . . . . . . 15 -Ο€ ∈ ℝ
111 iccssre 13408 . . . . . . . . . . . . . . 15 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ) β†’ (-Ο€[,]Ο€) βŠ† ℝ)
112110, 77, 111mp2an 690 . . . . . . . . . . . . . 14 (-Ο€[,]Ο€) βŠ† ℝ
113109, 112sstri 3991 . . . . . . . . . . . . 13 ((-Ο€[,]Ο€) βˆ– {0}) βŠ† ℝ
114113, 98sselid 3980 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ℝ)
115108, 114readdcld 11245 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (𝑋 + 𝑠) ∈ ℝ)
116107, 115ffvelcdmd 7087 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
11721, 33ifcld 4574 . . . . . . . . . . 11 (πœ‘ β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
118117adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
119116, 118resubcld 11644 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
120119adantlr 713 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
1211adantr 481 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑛 ∈ β„•)
122114adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ℝ)
123100dirkerre 44896 . . . . . . . . 9 ((𝑛 ∈ β„• ∧ 𝑠 ∈ ℝ) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
124121, 122, 123syl2anc 584 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
125120, 124remulcld 11246 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ ℝ)
126103eqcomd 2738 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (πΊβ€˜π‘ ))
127126oveq1d 7426 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) / Ο€) = ((πΊβ€˜π‘ ) / Ο€))
128 picn 25976 . . . . . . . . . . . . 13 Ο€ ∈ β„‚
129128a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ Ο€ ∈ β„‚)
130125recnd 11244 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
13180a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ Ο€ β‰  0)
132129, 130, 129, 131div23d 12029 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) / Ο€) = ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
13343recnd 11244 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) ∈ β„‚)
134133, 129, 131divrec2d 11996 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΊβ€˜π‘ ) / Ο€) = ((1 / Ο€) Β· (πΊβ€˜π‘ )))
135127, 132, 1343eqtr3rd 2781 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((1 / Ο€) Β· (πΊβ€˜π‘ )) = ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
136128, 80dividi 11949 . . . . . . . . . . . 12 (Ο€ / Ο€) = 1
137136a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (Ο€ / Ο€) = 1)
138137oveq1d 7426 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (1 Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
139130mullidd 11234 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (1 Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )))
140135, 138, 1393eqtrrd 2777 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) = ((1 / Ο€) Β· (πΊβ€˜π‘ )))
141140mpteq2dva 5248 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (𝑠 ∈ 𝐴 ↦ ((1 / Ο€) Β· (πΊβ€˜π‘ ))))
142106, 81reccld 11985 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1 / Ο€) ∈ β„‚)
143142, 43, 75iblmulc2 25355 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ ((1 / Ο€) Β· (πΊβ€˜π‘ ))) ∈ 𝐿1)
144141, 143eqeltrd 2833 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) ∈ 𝐿1)
145106, 125, 144itgmulc2 25358 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) = ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠)
146145eqcomd 2738 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 = (Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
147146oveq1d 7426 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 / Ο€) = ((Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) / Ο€))
148125, 144itgcl 25308 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 ∈ β„‚)
149148, 106, 81divcan3d 11997 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) / Ο€) = ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
150105, 147, 1493eqtrd 2776 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) = ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
15187adantr 481 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑂 ∈ β„‚)
152112sseli 3978 . . . . . . 7 (𝑠 ∈ (-Ο€[,]Ο€) β†’ 𝑠 ∈ ℝ)
153152, 123sylan2 593 . . . . . 6 ((𝑛 ∈ β„• ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
154153adantll 712 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
155110a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ -Ο€ ∈ ℝ)
156 ax-resscn 11169 . . . . . . . . . 10 ℝ βŠ† β„‚
157156a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ ℝ βŠ† β„‚)
158 ssid 4004 . . . . . . . . 9 β„‚ βŠ† β„‚
159 cncfss 24422 . . . . . . . . 9 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
160157, 158, 159sylancl 586 . . . . . . . 8 (𝑛 ∈ β„• β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
161 eqid 2732 . . . . . . . . 9 (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )) = (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ ))
162100dirkerf 44898 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ (π·β€˜π‘›):β„βŸΆβ„)
163162feqmptd 6960 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (π·β€˜π‘›) = (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )))
164100dirkercncf 44908 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (π·β€˜π‘›) ∈ (ℝ–cn→ℝ))
165163, 164eqeltrrd 2834 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ (ℝ–cn→ℝ))
166112a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (-Ο€[,]Ο€) βŠ† ℝ)
167 ssid 4004 . . . . . . . . . 10 ℝ βŠ† ℝ
168167a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ ℝ βŠ† ℝ)
169161, 165, 166, 168, 153cncfmptssg 44672 . . . . . . . 8 (𝑛 ∈ β„• β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
170160, 169sseldd 3983 . . . . . . 7 (𝑛 ∈ β„• β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
171170adantl 482 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
172 cniccibl 25365 . . . . . 6 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ ∧ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚)) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
173155, 78, 171, 172syl3anc 1371 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
1744, 45, 154, 173iblss 25329 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
175151, 124, 174itgmulc2 25358 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠) = ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
176150, 175oveq12d 7429 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) + (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)) = (∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 + ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
17786ad2antrr 724 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 ∈ ℝ)
178177, 124remulcld 11246 . . . 4 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ ℝ)
179151, 124, 174iblmulc2 25355 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) ∈ 𝐿1)
180125, 144, 178, 179itgadd 25349 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 = (∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 + ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
181 fourierdlem95.ifeqo . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = 𝑂)
182181eqcomd 2738 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 = if(0 < 𝑠, π‘Œ, π‘Š))
183182adantlr 713 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 = if(0 < 𝑠, π‘Œ, π‘Š))
184183oveq1d 7426 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) = (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ )))
185184oveq2d 7427 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
186116recnd 11244 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
187186adantlr 713 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
188118recnd 11244 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
189188adantlr 713 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
190124recnd 11244 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ β„‚)
191187, 189, 190subdird 11673 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) = (((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
192191oveq1d 7426 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
193187, 190mulcld 11236 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
194189, 190mulcld 11236 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
195193, 194npcand 11577 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )))
196185, 192, 1953eqtrd 2776 . . . 4 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )))
197196itgeq2dv 25306 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 = ∫𝐴((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
198180, 197eqtr3d 2774 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 + ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) = ∫𝐴((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
19997, 176, 1983eqtrd 2776 1 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΈβ€˜π‘›) + (𝑂 / 2)) = ∫𝐴((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  {crab 3432   βˆ– cdif 3945   βŠ† wss 3948  ifcif 4528  {csn 4628   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  ran crn 5677   β†Ύ cres 5678  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ↑m cmap 8822  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  +∞cpnf 11247  -∞cmnf 11248  β„*cxr 11249   < clt 11250   βˆ’ cmin 11446  -cneg 11447   / cdiv 11873  β„•cn 12214  2c2 12269  (,)cioo 13326  [,]cicc 13329  ...cfz 13486  ..^cfzo 13629   mod cmo 13836  sincsin 16009  Ο€cpi 16012  TopOpenctopn 17369  β„‚fldccnfld 20950  β€“cnβ†’ccncf 24399  volcvol 24987  πΏ1cibl 25141  βˆ«citg 25142   limβ„‚ climc 25386   D cdv 25387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cc 10432  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 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-symdif 4242  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-ofr 7673  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-oadd 8472  df-omul 8473  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-dju 9898  df-card 9936  df-acn 9939  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-q 12935  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-ioo 13330  df-ioc 13331  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-mod 13837  df-seq 13969  df-exp 14030  df-fac 14236  df-bc 14265  df-hash 14293  df-shft 15016  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-limsup 15417  df-clim 15434  df-rlim 15435  df-sum 15635  df-ef 16013  df-sin 16015  df-cos 16016  df-pi 16018  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-starv 17214  df-sca 17215  df-vsca 17216  df-ip 17217  df-tset 17218  df-ple 17219  df-ds 17221  df-unif 17222  df-hom 17223  df-cco 17224  df-rest 17370  df-topn 17371  df-0g 17389  df-gsum 17390  df-topgen 17391  df-pt 17392  df-prds 17395  df-xrs 17450  df-qtop 17455  df-imas 17456  df-xps 17458  df-mre 17532  df-mrc 17533  df-acs 17535  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-submnd 18674  df-mulg 18953  df-cntz 19183  df-cmn 19652  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-mopn 20946  df-fbas 20947  df-fg 20948  df-cnfld 20951  df-top 22403  df-topon 22420  df-topsp 22442  df-bases 22456  df-cld 22530  df-ntr 22531  df-cls 22532  df-nei 22609  df-lp 22647  df-perf 22648  df-cn 22738  df-cnp 22739  df-t1 22825  df-haus 22826  df-cmp 22898  df-tx 23073  df-hmeo 23266  df-fil 23357  df-fm 23449  df-flim 23450  df-flf 23451  df-xms 23833  df-ms 23834  df-tms 23835  df-cncf 24401  df-ovol 24988  df-vol 24989  df-mbf 25143  df-itg1 25144  df-itg2 25145  df-ibl 25146  df-itg 25147  df-0p 25194  df-limc 25390  df-dv 25391
This theorem is referenced by:  fourierdlem103  45010  fourierdlem104  45011
  Copyright terms: Public domain W3C validator