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∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
fourierdlem55.k ⊢K=s∈−ππ⟼ifs=01s2⁢sin⁡s2
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∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
6 fourierdlem55.k ⊢K=s∈−ππ⟼ifs=01s2⁢sin⁡s2
7 fourierdlem55.u ⊢U=s∈−ππ⟼H⁡s⁢K⁡s
8 1 2 3 4 5 fourierdlem9 ⊢φ→H:−ππ⟶ℝ
9 8 ffvelcdmda ⊢φ∧s∈−ππ→H⁡s∈ℝ
10 6 fourierdlem43 ⊢K:−ππ⟶ℝ
11 10 ffvelcdmi ⊢s∈−ππ→K⁡s∈ℝ
12 11 adantl ⊢φ∧s∈−ππ→K⁡s∈ℝ
13 9 12 remulcld ⊢φ∧s∈−ππ→H⁡s⁢K⁡s∈ℝ
14 13 7 fmptd ⊢φ→U:−ππ⟶ℝ