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 : π π