Metamath Proof Explorer


Theorem fourierdlem67

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

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

Proof

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