Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem67.f |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
2 |
|
fourierdlem67.x |
⊢ ( 𝜑 → 𝑋 ∈ ℝ ) |
3 |
|
fourierdlem67.y |
⊢ ( 𝜑 → 𝑌 ∈ ℝ ) |
4 |
|
fourierdlem67.w |
⊢ ( 𝜑 → 𝑊 ∈ ℝ ) |
5 |
|
fourierdlem67.h |
⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) |
6 |
|
fourierdlem67.k |
⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) |
7 |
|
fourierdlem67.u |
⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) |
8 |
|
fourierdlem67.n |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
9 |
|
fourierdlem67.s |
⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) |
10 |
|
fourierdlem67.g |
⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) |
11 |
1 2 3 4 5 6 7
|
fourierdlem55 |
⊢ ( 𝜑 → 𝑈 : ( - π [,] π ) ⟶ ℝ ) |
12 |
11
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ ) |
13 |
9
|
fourierdlem5 |
⊢ ( 𝑁 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ ) |
14 |
8 13
|
syl |
⊢ ( 𝜑 → 𝑆 : ( - π [,] π ) ⟶ ℝ ) |
15 |
14
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℝ ) |
16 |
12 15
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℝ ) |
17 |
16 10
|
fmptd |
⊢ ( 𝜑 → 𝐺 : ( - π [,] π ) ⟶ ℝ ) |