Metamath Proof Explorer

Theorem fourierdlem55

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

Ref Expression
Hypotheses fourierdlem55.f ⊢ φ → F : ℝ ⟶ ℝ
fourierdlem55.x ⊢ φ → X ∈ ℝ
fourierdlem55.r ⊢ φ → Y ∈ ℝ
fourierdlem55.w ⊢ φ → W ∈ ℝ
fourierdlem55.h ⊢ H = s ∈ − π π ⟼ if s = 0 0 F ⁡ X + s − if 0 < s Y W s
fourierdlem55.k ⊢ K = s ∈ − π π ⟼ if s = 0 1 s 2 ⁢ sin ⁡ s 2
fourierdlem55.u ⊢ U = s ∈ − π π ⟼ H ⁡ s ⁢ K ⁡ s
Assertion fourierdlem55 ⊢ φ → U : − π π ⟶ ℝ

Proof

Step Hyp Ref Expression
1 fourierdlem55.f ⊢ φ → F : ℝ ⟶ ℝ
2 fourierdlem55.x ⊢ φ → X ∈ ℝ
3 fourierdlem55.r ⊢ φ → Y ∈ ℝ
4 fourierdlem55.w ⊢ φ → W ∈ ℝ
5 fourierdlem55.h ⊢ H = s ∈ − π π ⟼ if s = 0 0 F ⁡ X + s − if 0 < s Y W s
6 fourierdlem55.k ⊢ K = s ∈ − π π ⟼ if s = 0 1 s 2 ⁢ sin ⁡ s 2
7 fourierdlem55.u ⊢ U = s ∈ − π π ⟼ H ⁡ s ⁢ K ⁡ s
8 1 2 3 4 5 fourierdlem9 ⊢ φ → H : − π π ⟶ ℝ
9 8 ffvelrnda ⊢ φ ∧ s ∈ − π π → H ⁡ s ∈ ℝ
10 6 fourierdlem43 ⊢ K : − π π ⟶ ℝ
11 10 ffvelrni ⊢ s ∈ − π π → K ⁡ s ∈ ℝ
12 11 adantl ⊢ φ ∧ s ∈ − π π → K ⁡ s ∈ ℝ
13 9 12 remulcld ⊢ φ ∧ s ∈ − π π → H ⁡ s ⁢ K ⁡ s ∈ ℝ
14 13 7 fmptd ⊢ φ → U : − π π ⟶ ℝ