Step |
Hyp |
Ref |
Expression |
1 |
|
fourierclim.f |
⊢ 𝐹 : ℝ ⟶ ℝ |
2 |
|
fourierclim.t |
⊢ 𝑇 = ( 2 · π ) |
3 |
|
fourierclim.per |
⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
4 |
|
fourierclim.g |
⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) |
5 |
|
fourierclim.dmdv |
⊢ ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin |
6 |
|
fourierclim.dvcn |
⊢ 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) |
7 |
|
fourierclim.rlim |
⊢ ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ ) |
8 |
|
fourierclim.llim |
⊢ ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ ) |
9 |
|
fourierclim.x |
⊢ 𝑋 ∈ ℝ |
10 |
|
fourierclim.l |
⊢ 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) |
11 |
|
fourierclim.r |
⊢ 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) |
12 |
|
fourierclim.a |
⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ) |
13 |
|
fourierclim.b |
⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ) |
14 |
|
fourierclim.s |
⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) |
15 |
1
|
a1i |
⊢ ( ⊤ → 𝐹 : ℝ ⟶ ℝ ) |
16 |
3
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
17 |
5
|
a1i |
⊢ ( ⊤ → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin ) |
18 |
6
|
a1i |
⊢ ( ⊤ → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) ) |
19 |
7
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ ) |
20 |
8
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ ) |
21 |
9
|
a1i |
⊢ ( ⊤ → 𝑋 ∈ ℝ ) |
22 |
10
|
a1i |
⊢ ( ⊤ → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) |
23 |
11
|
a1i |
⊢ ( ⊤ → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) |
24 |
15 2 16 4 17 18 19 20 21 22 23 12 13 14
|
fourierclimd |
⊢ ( ⊤ → seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) ) |
25 |
24
|
mptru |
⊢ seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) |