Metamath Proof Explorer


Theorem fourierdlem67

Description: G is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem67.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
fourierdlem67.x ( 𝜑𝑋 ∈ ℝ )
fourierdlem67.y ( 𝜑𝑌 ∈ ℝ )
fourierdlem67.w ( 𝜑𝑊 ∈ ℝ )
fourierdlem67.h 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem67.k 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem67.u 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻𝑠 ) · ( 𝐾𝑠 ) ) )
fourierdlem67.n ( 𝜑𝑁 ∈ ℝ )
fourierdlem67.s 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
fourierdlem67.g 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈𝑠 ) · ( 𝑆𝑠 ) ) )
Assertion fourierdlem67 ( 𝜑𝐺 : ( - π [,] π ) ⟶ ℝ )

Proof

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 ( 𝜑𝐺 : ( - π [,] π ) ⟶ ℝ )