Metamath Proof Explorer

Theorem sinf

Description: Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion sinf 
|- sin : CC --> CC

Proof

Step Hyp Ref Expression
1 df-sin 
 |-  sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
2 ax-icn 
 |-  _i e. CC
3 mulcl 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
4 2 3 mpan 
 |-  ( x e. CC -> ( _i x. x ) e. CC )
5 efcl 
 |-  ( ( _i x. x ) e. CC -> ( exp ` ( _i x. x ) ) e. CC )
6 4 5 syl 
 |-  ( x e. CC -> ( exp ` ( _i x. x ) ) e. CC )
7 negicn 
 |-  -u _i e. CC
8 mulcl 
 |-  ( ( -u _i e. CC /\ x e. CC ) -> ( -u _i x. x ) e. CC )
9 7 8 mpan 
 |-  ( x e. CC -> ( -u _i x. x ) e. CC )
10 efcl 
 |-  ( ( -u _i x. x ) e. CC -> ( exp ` ( -u _i x. x ) ) e. CC )
11 9 10 syl 
 |-  ( x e. CC -> ( exp ` ( -u _i x. x ) ) e. CC )
12 6 11 subcld 
 |-  ( x e. CC -> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) e. CC )
13 2mulicn 
 |-  ( 2 x. _i ) e. CC
14 2muline0 
 |-  ( 2 x. _i ) =/= 0
15 divcl 
 |-  ( ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) e. CC )
16 13 14 15 mp3an23 
 |-  ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) e. CC -> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) e. CC )
17 12 16 syl 
 |-  ( x e. CC -> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) e. CC )
18 1 17 fmpti 
 |-  sin : CC --> CC