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 44903
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 4133 . . . . . . . . 9 (πœ‘ β†’ 𝐴 βŠ† (-Ο€[,]Ο€))
43adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† (-Ο€[,]Ο€))
54sselda 3981 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
6 fourierdlem95.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
76adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐹:β„βŸΆβ„)
8 fourierdlem95.xre . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ℝ)
98adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑋 ∈ ℝ)
10 ioossre 13381 . . . . . . . . . . . . 13 (𝑋(,)+∞) βŠ† ℝ
1110a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋(,)+∞) βŠ† ℝ)
126, 11fssresd 6755 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (𝑋(,)+∞)):(𝑋(,)+∞)βŸΆβ„)
13 ioosscn 13382 . . . . . . . . . . . 12 (𝑋(,)+∞) βŠ† β„‚
1413a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑋(,)+∞) βŠ† β„‚)
15 eqid 2732 . . . . . . . . . . . 12 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
16 pnfxr 11264 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
1716a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ +∞ ∈ ℝ*)
188ltpnfd 13097 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 < +∞)
1915, 17, 8, 18lptioo1cn 44348 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝑋(,)+∞)))
20 fourierdlem95.y . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ ((𝐹 β†Ύ (𝑋(,)+∞)) limβ„‚ 𝑋))
2112, 14, 19, 20limcrecl 44331 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ ℝ)
2221adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ π‘Œ ∈ ℝ)
23 ioossre 13381 . . . . . . . . . . . . 13 (-∞(,)𝑋) βŠ† ℝ
2423a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (-∞(,)𝑋) βŠ† ℝ)
256, 24fssresd 6755 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (-∞(,)𝑋)):(-∞(,)𝑋)βŸΆβ„)
26 ioosscn 13382 . . . . . . . . . . . 12 (-∞(,)𝑋) βŠ† β„‚
2726a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (-∞(,)𝑋) βŠ† β„‚)
28 mnfxr 11267 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
2928a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ ∈ ℝ*)
308mnfltd 13100 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ < 𝑋)
3115, 29, 8, 30lptioo2cn 44347 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(-∞(,)𝑋)))
32 fourierdlem95.w . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
3325, 27, 31, 32limcrecl 44331 . . . . . . . . . 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 12223 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ ℝ)
39 fourierdlem95.s . . . . . . . . 9 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑛 + (1 / 2)) Β· 𝑠)))
40 fourierdlem95.g . . . . . . . . 9 𝐺 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
417, 9, 22, 34, 35, 36, 37, 38, 39, 40fourierdlem67 44875 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺:(-Ο€[,]Ο€)βŸΆβ„)
4241ffvelcdmda 7083 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (πΊβ€˜π‘ ) ∈ ℝ)
435, 42syldan 591 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) ∈ ℝ)
44 fourierdlem95.admvol . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ dom vol)
4544adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 ∈ dom vol)
4641feqmptd 6957 . . . . . . . 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 6888 . . . . . . . . . . 11 (𝑗 = 𝑖 β†’ (π‘‰β€˜π‘—) = (π‘‰β€˜π‘–))
6362oveq1d 7420 . . . . . . . . . 10 (𝑗 = 𝑖 β†’ ((π‘‰β€˜π‘—) βˆ’ 𝑋) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
6463cbvmptv 5260 . . . . . . . . 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 44896 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐺 ∈ 𝐿1)
7446, 73eqeltrrd 2834 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ (πΊβ€˜π‘ )) ∈ 𝐿1)
754, 45, 42, 74iblss 25313 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (πΊβ€˜π‘ )) ∈ 𝐿1)
7643, 75itgrecl 25306 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(πΊβ€˜π‘ ) d𝑠 ∈ ℝ)
77 pire 25959 . . . . . 6 Ο€ ∈ ℝ
7877a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ ℝ)
79 pipos 25961 . . . . . . 7 0 < Ο€
8077, 79gt0ne0ii 11746 . . . . . 6 Ο€ β‰  0
8180a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ β‰  0)
8276, 78, 81redivcld 12038 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) ∈ ℝ)
83 fourierlemenplusacver2eqitgdirker.e . . . . 5 𝐸 = (𝑛 ∈ β„• ↦ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
8483fvmpt2 7006 . . . 4 ((𝑛 ∈ β„• ∧ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) ∈ ℝ) β†’ (πΈβ€˜π‘›) = (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
851, 82, 84syl2anc 584 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΈβ€˜π‘›) = (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€))
86 fourierdlem95.o . . . . . . 7 (πœ‘ β†’ 𝑂 ∈ ℝ)
8786recnd 11238 . . . . . 6 (πœ‘ β†’ 𝑂 ∈ β„‚)
88 2cnd 12286 . . . . . 6 (πœ‘ β†’ 2 ∈ β„‚)
89 2ne0 12312 . . . . . . 7 2 β‰  0
9089a1i 11 . . . . . 6 (πœ‘ β†’ 2 β‰  0)
9187, 88, 90divrecd 11989 . . . . 5 (πœ‘ β†’ (𝑂 / 2) = (𝑂 Β· (1 / 2)))
9291adantr 481 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 / 2) = (𝑂 Β· (1 / 2)))
93 fourierdlem95.itgdirker . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠 = (1 / 2))
9493eqcomd 2738 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1 / 2) = ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)
9594oveq2d 7421 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 Β· (1 / 2)) = (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠))
9692, 95eqtrd 2772 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 / 2) = (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠))
9785, 96oveq12d 7423 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΈβ€˜π‘›) + (𝑂 / 2)) = ((∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) + (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)))
982sselda 3981 . . . . . . . 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 44874 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ ((-Ο€[,]Ο€) βˆ– {0})) β†’ (πΊβ€˜π‘ ) = (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
10399, 102syldan 591 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) = (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
104103itgeq2dv 25290 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(πΊβ€˜π‘ ) d𝑠 = ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠)
105104oveq1d 7420 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) = (∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 / Ο€))
10678recnd 11238 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ β„‚)
1076adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝐹:β„βŸΆβ„)
1088adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑋 ∈ ℝ)
109 difss 4130 . . . . . . . . . . . . . 14 ((-Ο€[,]Ο€) βˆ– {0}) βŠ† (-Ο€[,]Ο€)
11077renegcli 11517 . . . . . . . . . . . . . . 15 -Ο€ ∈ ℝ
111 iccssre 13402 . . . . . . . . . . . . . . 15 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ) β†’ (-Ο€[,]Ο€) βŠ† ℝ)
112110, 77, 111mp2an 690 . . . . . . . . . . . . . 14 (-Ο€[,]Ο€) βŠ† ℝ
113109, 112sstri 3990 . . . . . . . . . . . . 13 ((-Ο€[,]Ο€) βˆ– {0}) βŠ† ℝ
114113, 98sselid 3979 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ℝ)
115108, 114readdcld 11239 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (𝑋 + 𝑠) ∈ ℝ)
116107, 115ffvelcdmd 7084 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
11721, 33ifcld 4573 . . . . . . . . . . 11 (πœ‘ β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
118117adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
119116, 118resubcld 11638 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
120119adantlr 713 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
1211adantr 481 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑛 ∈ β„•)
122114adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ ℝ)
123100dirkerre 44797 . . . . . . . . 9 ((𝑛 ∈ β„• ∧ 𝑠 ∈ ℝ) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
124121, 122, 123syl2anc 584 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
125120, 124remulcld 11240 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ ℝ)
126103eqcomd 2738 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (πΊβ€˜π‘ ))
127126oveq1d 7420 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) / Ο€) = ((πΊβ€˜π‘ ) / Ο€))
128 picn 25960 . . . . . . . . . . . . 13 Ο€ ∈ β„‚
129128a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ Ο€ ∈ β„‚)
130125recnd 11238 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
13180a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ Ο€ β‰  0)
132129, 130, 129, 131div23d 12023 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) / Ο€) = ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
13343recnd 11238 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΊβ€˜π‘ ) ∈ β„‚)
134133, 129, 131divrec2d 11990 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΊβ€˜π‘ ) / Ο€) = ((1 / Ο€) Β· (πΊβ€˜π‘ )))
135127, 132, 1343eqtr3rd 2781 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((1 / Ο€) Β· (πΊβ€˜π‘ )) = ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
136128, 80dividi 11943 . . . . . . . . . . . 12 (Ο€ / Ο€) = 1
137136a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (Ο€ / Ο€) = 1)
138137oveq1d 7420 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((Ο€ / Ο€) Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (1 Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))))
139130mullidd 11228 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (1 Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )))
140135, 138, 1393eqtrrd 2777 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) = ((1 / Ο€) Β· (πΊβ€˜π‘ )))
141140mpteq2dva 5247 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) = (𝑠 ∈ 𝐴 ↦ ((1 / Ο€) Β· (πΊβ€˜π‘ ))))
142106, 81reccld 11979 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1 / Ο€) ∈ β„‚)
143142, 43, 75iblmulc2 25339 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ ((1 / Ο€) Β· (πΊβ€˜π‘ ))) ∈ 𝐿1)
144141, 143eqeltrd 2833 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) ∈ 𝐿1)
145106, 125, 144itgmulc2 25342 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) = ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠)
146145eqcomd 2738 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 = (Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
147146oveq1d 7420 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(Ο€ Β· (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ ))) d𝑠 / Ο€) = ((Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) / Ο€))
148125, 144itgcl 25292 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 ∈ β„‚)
149148, 106, 81divcan3d 11991 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((Ο€ Β· ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠) / Ο€) = ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
150105, 147, 1493eqtrd 2776 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) = ∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
15187adantr 481 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑂 ∈ β„‚)
152112sseli 3977 . . . . . . 7 (𝑠 ∈ (-Ο€[,]Ο€) β†’ 𝑠 ∈ ℝ)
153152, 123sylan2 593 . . . . . 6 ((𝑛 ∈ β„• ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
154153adantll 712 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ ℝ)
155110a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ -Ο€ ∈ ℝ)
156 ax-resscn 11163 . . . . . . . . . 10 ℝ βŠ† β„‚
157156a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ ℝ βŠ† β„‚)
158 ssid 4003 . . . . . . . . 9 β„‚ βŠ† β„‚
159 cncfss 24406 . . . . . . . . 9 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
160157, 158, 159sylancl 586 . . . . . . . 8 (𝑛 ∈ β„• β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
161 eqid 2732 . . . . . . . . 9 (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )) = (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ ))
162100dirkerf 44799 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ (π·β€˜π‘›):β„βŸΆβ„)
163162feqmptd 6957 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (π·β€˜π‘›) = (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )))
164100dirkercncf 44809 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (π·β€˜π‘›) ∈ (ℝ–cn→ℝ))
165163, 164eqeltrrd 2834 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (𝑠 ∈ ℝ ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ (ℝ–cn→ℝ))
166112a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (-Ο€[,]Ο€) βŠ† ℝ)
167 ssid 4003 . . . . . . . . . 10 ℝ βŠ† ℝ
168167a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ ℝ βŠ† ℝ)
169161, 165, 166, 168, 153cncfmptssg 44573 . . . . . . . 8 (𝑛 ∈ β„• β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
170160, 169sseldd 3982 . . . . . . 7 (𝑛 ∈ β„• β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
171170adantl 482 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
172 cniccibl 25349 . . . . . 6 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ ∧ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚)) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
173155, 78, 171, 172syl3anc 1371 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
1744, 45, 154, 173iblss 25313 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ ((π·β€˜π‘›)β€˜π‘ )) ∈ 𝐿1)
175151, 124, 174itgmulc2 25342 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠) = ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠)
176150, 175oveq12d 7423 . 2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((∫𝐴(πΊβ€˜π‘ ) d𝑠 / Ο€) + (𝑂 Β· ∫𝐴((π·β€˜π‘›)β€˜π‘ ) d𝑠)) = (∫𝐴(((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠 + ∫𝐴(𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) d𝑠))
17786ad2antrr 724 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 ∈ ℝ)
178177, 124remulcld 11240 . . . 4 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ ℝ)
179151, 124, 174iblmulc2 25339 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑠 ∈ 𝐴 ↦ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) ∈ 𝐿1)
180125, 144, 178, 179itgadd 25333 . . 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 7420 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ )) = (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ )))
185184oveq2d 7421 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
186116recnd 11238 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
187186adantlr 713 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
188118recnd 11238 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
189188adantlr 713 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
190124recnd 11238 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((π·β€˜π‘›)β€˜π‘ ) ∈ β„‚)
191187, 189, 190subdird 11667 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) = (((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
192191oveq1d 7420 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))))
193187, 190mulcld 11230 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
194189, 190mulcld 11230 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ )) ∈ β„‚)
195193, 194npcand 11571 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )) βˆ’ (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) + (if(0 < 𝑠, π‘Œ, π‘Š) Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )))
196185, 192, 1953eqtrd 2776 . . . 4 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑠 ∈ 𝐴) β†’ ((((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· ((π·β€˜π‘›)β€˜π‘ )) + (𝑂 Β· ((π·β€˜π‘›)β€˜π‘ ))) = ((πΉβ€˜(𝑋 + 𝑠)) Β· ((π·β€˜π‘›)β€˜π‘ )))
197196itgeq2dv 25290 . . 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 3944   βŠ† wss 3947  ifcif 4527  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675  ran crn 5676   β†Ύ cres 5677  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ↑m cmap 8816  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111  +∞cpnf 11241  -∞cmnf 11242  β„*cxr 11243   < clt 11244   βˆ’ cmin 11440  -cneg 11441   / cdiv 11867  β„•cn 12208  2c2 12263  (,)cioo 13320  [,]cicc 13323  ...cfz 13480  ..^cfzo 13623   mod cmo 13830  sincsin 16003  Ο€cpi 16006  TopOpenctopn 17363  β„‚fldccnfld 20936  β€“cnβ†’ccncf 24383  volcvol 24971  πΏ1cibl 25125  βˆ«citg 25126   limβ„‚ climc 25370   D cdv 25371
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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cc 10426  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
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 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-symdif 4241  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-disj 5113  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 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19644  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931  df-mopn 20932  df-fbas 20933  df-fg 20934  df-cnfld 20937  df-top 22387  df-topon 22404  df-topsp 22426  df-bases 22440  df-cld 22514  df-ntr 22515  df-cls 22516  df-nei 22593  df-lp 22631  df-perf 22632  df-cn 22722  df-cnp 22723  df-t1 22809  df-haus 22810  df-cmp 22882  df-tx 23057  df-hmeo 23250  df-fil 23341  df-fm 23433  df-flim 23434  df-flf 23435  df-xms 23817  df-ms 23818  df-tms 23819  df-cncf 24385  df-ovol 24972  df-vol 24973  df-mbf 25127  df-itg1 25128  df-itg2 25129  df-ibl 25130  df-itg 25131  df-0p 25178  df-limc 25374  df-dv 25375
This theorem is referenced by:  fourierdlem103  44911  fourierdlem104  44912
  Copyright terms: Public domain W3C validator