Metamath Proof Explorer

Theorem fourierdlem67

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

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

Proof

Step Hyp Ref Expression
1 fourierdlem67.f ⊢ φ → F : ℝ ⟶ ℝ
2 fourierdlem67.x ⊢ φ → X ∈ ℝ
3 fourierdlem67.y ⊢ φ → Y ∈ ℝ
4 fourierdlem67.w ⊢ φ → W ∈ ℝ
5 fourierdlem67.h ⊢ H = s ∈ − π π ⟼ if s = 0 0 F ⁡ X + s − if 0 < s Y W s
6 fourierdlem67.k ⊢ K = s ∈ − π π ⟼ if s = 0 1 s 2 ⁢ sin ⁡ s 2
7 fourierdlem67.u ⊢ U = s ∈ − π π ⟼ H ⁡ s ⁢ K ⁡ s
8 fourierdlem67.n ⊢ φ → N ∈ ℝ
9 fourierdlem67.s ⊢ S = s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s
10 fourierdlem67.g ⊢ G = s ∈ − π π ⟼ U ⁡ s ⁢ S ⁡ s
11 1 2 3 4 5 6 7 fourierdlem55 ⊢ φ → U : − π π ⟶ ℝ
12 11 ffvelrnda ⊢ φ ∧ s ∈ − π π → U ⁡ s ∈ ℝ
13 9 fourierdlem5 ⊢ N ∈ ℝ → S : − π π ⟶ ℝ
14 8 13 syl ⊢ φ → S : − π π ⟶ ℝ
15 14 ffvelrnda ⊢ φ ∧ s ∈ − π π → S ⁡ s ∈ ℝ
16 12 15 remulcld ⊢ φ ∧ s ∈ − π π → U ⁡ s ⁢ S ⁡ s ∈ ℝ
17 16 10 fmptd ⊢ φ → G : − π π ⟶ ℝ