Metamath Proof Explorer


Theorem fourierdlem55

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

Ref Expression
Hypotheses fourierdlem55.f
|- ( ph -> F : RR --> RR )
fourierdlem55.x
|- ( ph -> X e. RR )
fourierdlem55.r
|- ( ph -> Y e. RR )
fourierdlem55.w
|- ( ph -> W e. RR )
fourierdlem55.h
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem55.k
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem55.u
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
Assertion fourierdlem55
|- ( ph -> U : ( -u _pi [,] _pi ) --> RR )

Proof

Step Hyp Ref Expression
1 fourierdlem55.f
 |-  ( ph -> F : RR --> RR )
2 fourierdlem55.x
 |-  ( ph -> X e. RR )
3 fourierdlem55.r
 |-  ( ph -> Y e. RR )
4 fourierdlem55.w
 |-  ( ph -> W e. RR )
5 fourierdlem55.h
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
6 fourierdlem55.k
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
7 fourierdlem55.u
 |-  U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
8 1 2 3 4 5 fourierdlem9
 |-  ( ph -> H : ( -u _pi [,] _pi ) --> RR )
9 8 ffvelrnda
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( H ` s ) e. RR )
10 6 fourierdlem43
 |-  K : ( -u _pi [,] _pi ) --> RR
11 10 ffvelrni
 |-  ( s e. ( -u _pi [,] _pi ) -> ( K ` s ) e. RR )
12 11 adantl
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( K ` s ) e. RR )
13 9 12 remulcld
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( ( H ` s ) x. ( K ` s ) ) e. RR )
14 13 7 fmptd
 |-  ( ph -> U : ( -u _pi [,] _pi ) --> RR )