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∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
fourierdlem67.k ⊢K=s∈−ππ⟼ifs=01s2⁢sin⁡s2
fourierdlem67.u ⊢U=s∈−ππ⟼H⁡s⁢K⁡s
fourierdlem67.n ⊢φ→N∈ℝ
fourierdlem67.s ⊢S=s∈−ππ⟼sin⁡N+12⁢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∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
6 fourierdlem67.k ⊢K=s∈−ππ⟼ifs=01s2⁢sin⁡s2
7 fourierdlem67.u ⊢U=s∈−ππ⟼H⁡s⁢K⁡s
8 fourierdlem67.n ⊢φ→N∈ℝ
9 fourierdlem67.s ⊢S=s∈−ππ⟼sin⁡N+12⁢s
10 fourierdlem67.g ⊢G=s∈−ππ⟼U⁡s⁢S⁡s
11 1 2 3 4 5 6 7 fourierdlem55 ⊢φ→U:−ππ⟶ℝ
12 11 ffvelcdmda ⊢φ∧s∈−ππ→U⁡s∈ℝ
13 9 fourierdlem5 ⊢N∈ℝ→S:−ππ⟶ℝ
14 8 13 syl ⊢φ→S:−ππ⟶ℝ
15 14 ffvelcdmda ⊢φ∧s∈−ππ→S⁡s∈ℝ
16 12 15 remulcld ⊢φ∧s∈−ππ→U⁡s⁢S⁡s∈ℝ
17 16 10 fmptd ⊢φ→G:−ππ⟶ℝ