Metamath Proof Explorer

Theorem fourierdlem95

Description: Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 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 fourierdlem95 ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) + ( 𝑂 / 2 ) ) = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )

Proof

Step Hyp Ref Expression
1 fourierdlem95.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem95.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem95.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4 fourierdlem95.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 fourierdlem95.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
6 fourierdlem95.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
7 fourierdlem95.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8 fourierdlem95.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
9 fourierdlem95.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
10 fourierdlem95.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
11 fourierdlem95.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
12 fourierdlem95.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
13 fourierdlem95.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
14 fourierdlem95.g ⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
15 fourierdlem95.i ⊢ 𝐼 = ( ℝ D 𝐹 )
16 fourierdlem95.ifn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
17 fourierdlem95.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝐼 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
18 fourierdlem95.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
19 fourierdlem95.y ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
20 fourierdlem95.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
21 fourierdlem95.admvol ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
22 fourierdlem95.ass ⊢ ( 𝜑 → 𝐴 ⊆ ( ( - π [,] π ) ∖ { 0 } ) )
23 fourierlemenplusacver2eqitgdirker.e ⊢ 𝐸 = ( 𝑛 ∈ ℕ ↦ ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) )
24 fourierdlem95.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
25 fourierdlem95.o ⊢ ( 𝜑 → 𝑂 ∈ ℝ )
26 fourierdlem95.ifeqo ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑂 )
27 fourierdlem95.itgdirker ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 = ( 1 / 2 ) )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
29 22 difss2d ⊢ ( 𝜑 → 𝐴 ⊆ ( - π [,] π ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ( - π [,] π ) )
31 30 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( - π [,] π ) )
32 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℝ ⟶ ℝ )
33 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ℝ )
34 ioossre ⊢ ( 𝑋 (,) +∞ ) ⊆ ℝ
35 34 a1i ⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℝ )
36 1 35 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) : ( 𝑋 (,) +∞ ) ⟶ ℝ )
37 ioosscn ⊢ ( 𝑋 (,) +∞ ) ⊆ ℂ
38 37 a1i ⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℂ )
39 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
40 pnfxr ⊢ +∞ ∈ ℝ*
41 40 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
42 2 ltpnfd ⊢ ( 𝜑 → 𝑋 < +∞ )
43 39 41 2 42 lptioo1cn ⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) +∞ ) ) )
44 36 38 43 19 limcrecl ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑌 ∈ ℝ )
46 ioossre ⊢ ( -∞ (,) 𝑋 ) ⊆ ℝ
47 46 a1i ⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℝ )
48 1 47 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) : ( -∞ (,) 𝑋 ) ⟶ ℝ )
49 ioosscn ⊢ ( -∞ (,) 𝑋 ) ⊆ ℂ
50 49 a1i ⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℂ )
51 mnfxr ⊢ -∞ ∈ ℝ*
52 51 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
53 2 mnfltd ⊢ ( 𝜑 → -∞ < 𝑋 )
54 39 52 2 53 lptioo2cn ⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( -∞ (,) 𝑋 ) ) )
55 48 50 54 20 limcrecl ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ℝ )
57 28 nnred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
58 32 33 45 56 10 11 12 57 13 14 fourierdlem67 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 : ( - π [,] π ) ⟶ ℝ )
59 58 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
60 31 59 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
61 21 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ dom vol )
62 58 feqmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
63 6 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ran 𝑉 )
64 19 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
65 20 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
66 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ℕ )
67 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
68 7 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
69 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
70 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
71 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ 𝑖 ) )
72 71 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
73 72 cbvmptv ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
74 eqid ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
75 16 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
76 17 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ( ( 𝐼 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
77 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
78 3 32 63 64 65 10 11 12 57 13 14 66 67 68 69 70 73 74 15 75 76 77 fourierdlem88 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 ∈ 𝐿1 )
79 62 78 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝐺 ‘ 𝑠 ) ) ∈ 𝐿1 )
80 30 61 59 79 iblss ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑠 ) ) ∈ 𝐿1 )
81 60 80 itgrecl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 ∈ ℝ )
82 pire ⊢ π ∈ ℝ
83 82 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℝ )
84 pipos ⊢ 0 < π
85 82 84 gt0ne0ii ⊢ π ≠ 0
86 85 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ≠ 0 )
87 81 83 86 redivcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) ∈ ℝ )
88 23 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) ∈ ℝ ) → ( 𝐸 ‘ 𝑛 ) = ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) )
89 28 87 88 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) = ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) )
90 25 recnd ⊢ ( 𝜑 → 𝑂 ∈ ℂ )
91 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
92 2ne0 ⊢ 2 ≠ 0
93 92 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
94 90 91 93 divrecd ⊢ ( 𝜑 → ( 𝑂 / 2 ) = ( 𝑂 · ( 1 / 2 ) ) )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 / 2 ) = ( 𝑂 · ( 1 / 2 ) ) )
96 27 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 2 ) = ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 )
97 96 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 · ( 1 / 2 ) ) = ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) )
98 95 97 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 / 2 ) = ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) )
99 89 98 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) + ( 𝑂 / 2 ) ) = ( ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) + ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) ) )
100 22 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) )
101 100 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) )
102 eqid ⊢ ( ( - π [,] π ) ∖ { 0 } ) = ( ( - π [,] π ) ∖ { 0 } )
103 1 2 44 55 24 10 11 12 13 14 102 fourierdlem66 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ) → ( 𝐺 ‘ 𝑠 ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
104 101 103 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
105 104 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 )
106 105 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) = ( ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 / π ) )
107 83 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℂ )
108 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐹 : ℝ ⟶ ℝ )
109 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑋 ∈ ℝ )
110 difss ⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π )
111 82 renegcli ⊢ - π ∈ ℝ
112 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
113 111 82 112 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
114 110 113 sstri ⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℝ
115 114 100 sselid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
116 109 115 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
117 108 116 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
118 44 55 ifcld ⊢ ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
120 117 119 resubcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
121 120 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
122 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑛 ∈ ℕ )
123 115 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
124 24 dirkerre ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
125 122 123 124 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
126 121 125 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℝ )
127 104 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( 𝐺 ‘ 𝑠 ) )
128 127 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) / π ) = ( ( 𝐺 ‘ 𝑠 ) / π ) )
129 picn ⊢ π ∈ ℂ
130 129 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → π ∈ ℂ )
131 126 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℂ )
132 85 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → π ≠ 0 )
133 130 131 130 132 div23d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) / π ) = ( ( π / π ) · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
134 60 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℂ )
135 134 130 132 divrec2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑠 ) / π ) = ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) )
136 128 133 135 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) = ( ( π / π ) · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
137 129 85 dividi ⊢ ( π / π ) = 1
138 137 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( π / π ) = 1 )
139 138 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( π / π ) · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( 1 · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
140 131 mullidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 1 · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
141 136 139 140 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) )
142 141 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ 𝐴 ↦ ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) ) )
143 107 86 reccld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / π ) ∈ ℂ )
144 143 60 80 iblmulc2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) ) ∈ 𝐿1 )
145 142 144 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) ∈ 𝐿1 )
146 107 126 145 itgmulc2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) = ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 )
147 146 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 = ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) )
148 147 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 / π ) = ( ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) / π ) )
149 126 145 itgcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ∈ ℂ )
150 149 107 86 divcan3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) / π ) = ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
151 106 148 150 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) = ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
152 90 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑂 ∈ ℂ )
153 113 sseli ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ∈ ℝ )
154 153 124 sylan2 ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
155 154 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
156 111 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → - π ∈ ℝ )
157 ax-resscn ⊢ ℝ ⊆ ℂ
158 157 a1i ⊢ ( 𝑛 ∈ ℕ → ℝ ⊆ ℂ )
159 ssid ⊢ ℂ ⊆ ℂ
160 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( - π [,] π ) –cn→ ℝ ) ⊆ ( ( - π [,] π ) –cn→ ℂ ) )
161 158 159 160 sylancl ⊢ ( 𝑛 ∈ ℕ → ( ( - π [,] π ) –cn→ ℝ ) ⊆ ( ( - π [,] π ) –cn→ ℂ ) )
162 eqid ⊢ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) )
163 24 dirkerf ⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) : ℝ ⟶ ℝ )
164 163 feqmptd ⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
165 24 dirkercncf ⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) ∈ ( ℝ –cn→ ℝ ) )
166 164 165 eqeltrrd ⊢ ( 𝑛 ∈ ℕ → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℝ ) )
167 113 a1i ⊢ ( 𝑛 ∈ ℕ → ( - π [,] π ) ⊆ ℝ )
168 ssid ⊢ ℝ ⊆ ℝ
169 168 a1i ⊢ ( 𝑛 ∈ ℕ → ℝ ⊆ ℝ )
170 162 166 167 169 154 cncfmptssg ⊢ ( 𝑛 ∈ ℕ → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℝ ) )
171 161 170 sseldd ⊢ ( 𝑛 ∈ ℕ → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
172 171 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
173 cniccibl ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ 𝐿1 )
174 156 83 172 173 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ 𝐿1 )
175 30 61 155 174 iblss ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ 𝐿1 )
176 152 125 175 itgmulc2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) = ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
177 151 176 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) + ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) ) = ( ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 + ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) )
178 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑂 ∈ ℝ )
179 178 125 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℝ )
180 152 125 175 iblmulc2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) ∈ 𝐿1 )
181 126 145 179 180 itgadd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 = ( ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 + ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) )
182 26 eqcomd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑂 = if ( 0 < 𝑠 , 𝑌 , 𝑊 ) )
183 182 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑂 = if ( 0 < 𝑠 , 𝑌 , 𝑊 ) )
184 183 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
185 184 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
186 117 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
187 186 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
188 119 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
189 188 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
190 125 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℂ )
191 187 189 190 subdird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) − ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
192 191 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) − ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
193 187 190 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℂ )
194 189 190 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℂ )
195 193 194 npcand ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) − ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
196 185 192 195 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
197 196 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
198 181 197 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 + ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
199 99 177 198 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) + ( 𝑂 / 2 ) ) = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )