Metamath Proof Explorer

Theorem fourierdlem115

Description: Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem115.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem115.t ⊢ 𝑇 = ( 2 · π )
fourierdlem115.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem115.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
fourierdlem115.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
fourierdlem115.dvcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
fourierdlem115.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
fourierdlem115.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
fourierdlem115.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem115.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
fourierdlem115.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
fourierdlem115.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourierdlem115.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourierdlem115.s ⊢ 𝑆 = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
Assertion fourierdlem115 ( 𝜑 → ( seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem115.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem115.t ⊢ 𝑇 = ( 2 · π )
3 fourierdlem115.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4 fourierdlem115.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
5 fourierdlem115.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
6 fourierdlem115.dvcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
7 fourierdlem115.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
8 fourierdlem115.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
9 fourierdlem115.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10 fourierdlem115.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
11 fourierdlem115.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
12 fourierdlem115.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
13 fourierdlem115.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
14 fourierdlem115.s ⊢ 𝑆 = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
15 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 · 𝑥 ) = ( 𝑘 · 𝑥 ) )
16 15 fveq2d ⊢ ( 𝑛 = 𝑘 → ( cos ‘ ( 𝑛 · 𝑥 ) ) = ( cos ‘ ( 𝑘 · 𝑥 ) ) )
17 16 oveq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑘 · 𝑥 ) ) ) )
18 17 adantr ⊢ ( ( 𝑛 = 𝑘 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑘 · 𝑥 ) ) ) )
19 18 itgeq2dv ⊢ ( 𝑛 = 𝑘 → ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 = ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 )
20 19 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) = ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 / π ) )
21 20 cbvmptv ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 / π ) )
22 12 21 eqtri ⊢ 𝐴 = ( 𝑘 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 / π ) )
23 15 fveq2d ⊢ ( 𝑛 = 𝑘 → ( sin ‘ ( 𝑛 · 𝑥 ) ) = ( sin ‘ ( 𝑘 · 𝑥 ) ) )
24 23 oveq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑘 · 𝑥 ) ) ) )
25 24 adantr ⊢ ( ( 𝑛 = 𝑘 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑘 · 𝑥 ) ) ) )
26 25 itgeq2dv ⊢ ( 𝑛 = 𝑘 → ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 = ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 )
27 26 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) = ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 / π ) )
28 27 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ) = ( 𝑘 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 / π ) )
29 13 28 eqtri ⊢ 𝐵 = ( 𝑘 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 / π ) )
30 eqid ⊢ ( 𝑘 ∈ ℕ ↦ { 𝑤 ∈ ( ℝ ↑m ( 0 ... 𝑘 ) ) ∣ ( ( ( 𝑤 ‘ 0 ) = - π ∧ ( 𝑤 ‘ 𝑘 ) = π ) ∧ ∀ 𝑧 ∈ ( 0 ..^ 𝑘 ) ( 𝑤 ‘ 𝑧 ) < ( 𝑤 ‘ ( 𝑧 + 1 ) ) ) } ) = ( 𝑘 ∈ ℕ ↦ { 𝑤 ∈ ( ℝ ↑m ( 0 ... 𝑘 ) ) ∣ ( ( ( 𝑤 ‘ 0 ) = - π ∧ ( 𝑤 ‘ 𝑘 ) = π ) ∧ ∀ 𝑧 ∈ ( 0 ..^ 𝑘 ) ( 𝑤 ‘ 𝑧 ) < ( 𝑤 ‘ ( 𝑧 + 1 ) ) ) } )
31 id ⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
32 oveq2 ⊢ ( 𝑦 = 𝑥 → ( π − 𝑦 ) = ( π − 𝑥 ) )
33 32 oveq1d ⊢ ( 𝑦 = 𝑥 → ( ( π − 𝑦 ) / 𝑇 ) = ( ( π − 𝑥 ) / 𝑇 ) )
34 33 fveq2d ⊢ ( 𝑦 = 𝑥 → ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) )
35 34 oveq1d ⊢ ( 𝑦 = 𝑥 → ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
36 31 35 oveq12d ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
37 36 cbvmptv ⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
38 eqid ⊢ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) = ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) )
39 eqid ⊢ ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) = ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 )
40 isoeq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) ) )
41 40 cbviotavw ⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) )
42 1 2 3 4 5 6 7 8 9 10 11 22 29 14 30 37 38 39 41 fourierdlem114 ⊢ ( 𝜑 → ( seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) ) )
43 42 simpld ⊢ ( 𝜑 → seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) )
44 nfcv ⊢ Ⅎ 𝑘 ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) )
45 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
46 12 45 nfcxfr ⊢ Ⅎ 𝑛 𝐴
47 nfcv ⊢ Ⅎ 𝑛 𝑘
48 46 47 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑘 )
49 nfcv ⊢ Ⅎ 𝑛 ·
50 nfcv ⊢ Ⅎ 𝑛 ( cos ‘ ( 𝑘 · 𝑋 ) )
51 48 49 50 nfov ⊢ Ⅎ 𝑛 ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) )
52 nfcv ⊢ Ⅎ 𝑛 +
53 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
54 13 53 nfcxfr ⊢ Ⅎ 𝑛 𝐵
55 54 47 nffv ⊢ Ⅎ 𝑛 ( 𝐵 ‘ 𝑘 )
56 nfcv ⊢ Ⅎ 𝑛 ( sin ‘ ( 𝑘 · 𝑋 ) )
57 55 49 56 nfov ⊢ Ⅎ 𝑛 ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) )
58 51 52 57 nfov ⊢ Ⅎ 𝑛 ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
59 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
60 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 · 𝑋 ) = ( 𝑘 · 𝑋 ) )
61 60 fveq2d ⊢ ( 𝑛 = 𝑘 → ( cos ‘ ( 𝑛 · 𝑋 ) ) = ( cos ‘ ( 𝑘 · 𝑋 ) ) )
62 59 61 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) )
63 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐵 ‘ 𝑛 ) = ( 𝐵 ‘ 𝑘 ) )
64 60 fveq2d ⊢ ( 𝑛 = 𝑘 → ( sin ‘ ( 𝑛 · 𝑋 ) ) = ( sin ‘ ( 𝑘 · 𝑋 ) ) )
65 63 64 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
66 62 65 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
67 44 58 66 cbvsumi ⊢ Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
68 67 oveq2i ⊢ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
69 42 simprd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) )
70 68 69 eqtrid ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) )
71 43 70 jca ⊢ ( 𝜑 → ( seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) ) )