| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fourierdlem67.f |
|- ( ph -> F : RR --> RR ) |
| 2 |
|
fourierdlem67.x |
|- ( ph -> X e. RR ) |
| 3 |
|
fourierdlem67.y |
|- ( ph -> Y e. RR ) |
| 4 |
|
fourierdlem67.w |
|- ( ph -> W e. RR ) |
| 5 |
|
fourierdlem67.h |
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |
| 6 |
|
fourierdlem67.k |
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
| 7 |
|
fourierdlem67.u |
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) ) |
| 8 |
|
fourierdlem67.n |
|- ( ph -> N e. RR ) |
| 9 |
|
fourierdlem67.s |
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
| 10 |
|
fourierdlem67.g |
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) ) |
| 11 |
1 2 3 4 5 6 7
|
fourierdlem55 |
|- ( ph -> U : ( -u _pi [,] _pi ) --> RR ) |
| 12 |
11
|
ffvelcdmda |
|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) e. RR ) |
| 13 |
9
|
fourierdlem5 |
|- ( N e. RR -> S : ( -u _pi [,] _pi ) --> RR ) |
| 14 |
8 13
|
syl |
|- ( ph -> S : ( -u _pi [,] _pi ) --> RR ) |
| 15 |
14
|
ffvelcdmda |
|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( S ` s ) e. RR ) |
| 16 |
12 15
|
remulcld |
|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( ( U ` s ) x. ( S ` s ) ) e. RR ) |
| 17 |
16 10
|
fmptd |
|- ( ph -> G : ( -u _pi [,] _pi ) --> RR ) |