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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ )
13	9	fourierdlem5	⊢ ( 𝑁 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ )
14	8 13	syl	⊢ ( 𝜑 → 𝑆 : ( - π [,] π ) ⟶ ℝ )
15	14	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℝ )
16	12 15	remulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℝ )
17	16 10	fmptd	⊢ ( 𝜑 → 𝐺 : ( - π [,] π ) ⟶ ℝ )