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 ) |