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	⊢ 𝐴 = ( 𝑛 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( 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	⊢ 𝐴 = ( 𝑛 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( 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	⊢ ( 𝑛 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑘 · 𝑥 ) ) ) d 𝑥 / π ) )
22	12 21	eqtri	⊢ 𝐴 = ( 𝑘 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( 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		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
45		oveq1	⊢ ( 𝑛 = 𝑘 → ( 𝑛 · 𝑋 ) = ( 𝑘 · 𝑋 ) )
46	45	fveq2d	⊢ ( 𝑛 = 𝑘 → ( cos ‘ ( 𝑛 · 𝑋 ) ) = ( cos ‘ ( 𝑘 · 𝑋 ) ) )
47	44 46	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) )
48		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐵 ‘ 𝑛 ) = ( 𝐵 ‘ 𝑘 ) )
49	45	fveq2d	⊢ ( 𝑛 = 𝑘 → ( sin ‘ ( 𝑛 · 𝑋 ) ) = ( sin ‘ ( 𝑘 · 𝑋 ) ) )
50	48 49	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
51	47 50	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
52		nfcv	⊢ Ⅎ 𝑘 ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) )
53		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ₀ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
54	12 53	nfcxfr	⊢ Ⅎ 𝑛 𝐴
55		nfcv	⊢ Ⅎ 𝑛 𝑘
56	54 55	nffv	⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑘 )
57		nfcv	⊢ Ⅎ 𝑛 ·
58		nfcv	⊢ Ⅎ 𝑛 ( cos ‘ ( 𝑘 · 𝑋 ) )
59	56 57 58	nfov	⊢ Ⅎ 𝑛 ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) )
60		nfcv	⊢ Ⅎ 𝑛 +
61		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
62	13 61	nfcxfr	⊢ Ⅎ 𝑛 𝐵
63	62 55	nffv	⊢ Ⅎ 𝑛 ( 𝐵 ‘ 𝑘 )
64		nfcv	⊢ Ⅎ 𝑛 ( sin ‘ ( 𝑘 · 𝑋 ) )
65	63 57 64	nfov	⊢ Ⅎ 𝑛 ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) )
66	59 60 65	nfov	⊢ Ⅎ 𝑛 ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
67	51 52 66	cbvsum	⊢ Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( 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 ) ) )

Metamath Proof Explorer

Theorem fourierdlem115

Proof