Metamath Proof Explorer

Theorem fourierdlem5

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

Ref Expression
Hypothesis fourierdlem5.1 
|- S = ( x e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( X + ( 1 / 2 ) ) x. x ) ) )
Assertion fourierdlem5 
|- ( X e. RR -> S : ( -u _pi [,] _pi ) --> RR )

Proof

Step Hyp Ref Expression
1 fourierdlem5.1 
 |-  S = ( x e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( X + ( 1 / 2 ) ) x. x ) ) )
2 simpl 
 |-  ( ( X e. RR /\ x e. ( -u _pi [,] _pi ) ) -> X e. RR )
3 1red 
 |-  ( ( X e. RR /\ x e. ( -u _pi [,] _pi ) ) -> 1 e. RR )
4 3 rehalfcld 
 |-  ( ( X e. RR /\ x e. ( -u _pi [,] _pi ) ) -> ( 1 / 2 ) e. RR )
5 2 4 readdcld 
 |-  ( ( X e. RR /\ x e. ( -u _pi [,] _pi ) ) -> ( X + ( 1 / 2 ) ) e. RR )
6 pire 
 |-  _pi e. RR
7 6 renegcli 
 |-  -u _pi e. RR
8 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
9 7 6 8 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
10 9 sseli 
 |-  ( x e. ( -u _pi [,] _pi ) -> x e. RR )
11 10 adantl 
 |-  ( ( X e. RR /\ x e. ( -u _pi [,] _pi ) ) -> x e. RR )
12 5 11 remulcld 
 |-  ( ( X e. RR /\ x e. ( -u _pi [,] _pi ) ) -> ( ( X + ( 1 / 2 ) ) x. x ) e. RR )
13 12 resincld 
 |-  ( ( X e. RR /\ x e. ( -u _pi [,] _pi ) ) -> ( sin ` ( ( X + ( 1 / 2 ) ) x. x ) ) e. RR )
14 13 1 fmptd 
 |-  ( X e. RR -> S : ( -u _pi [,] _pi ) --> RR )