This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem55

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

Ref Expression
Hypotheses fourierdlem55.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem55.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem55.r ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
fourierdlem55.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
fourierdlem55.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem55.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem55.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
Assertion fourierdlem55 ( 𝜑 → 𝑈 : ( - π [,] π ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 fourierdlem55.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem55.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem55.r ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
4 fourierdlem55.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
5 fourierdlem55.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
6 fourierdlem55.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
7 fourierdlem55.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
8 1 2 3 4 5 fourierdlem9 ⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )
9 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐻 ‘ 𝑠 ) ∈ ℝ )
10 6 fourierdlem43 ⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ
11 10 ffvelcdmi ⊢ ( 𝑠 ∈ ( - π [,] π ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
13 9 12 remulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ )
14 13 7 fmptd ⊢ ( 𝜑 → 𝑈 : ( - π [,] π ) ⟶ ℝ )