Metamath Proof Explorer

Theorem cosf

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

Ref Expression
Assertion cosf 
|- cos : CC --> CC

Proof

Step Hyp Ref Expression
1 df-cos 
 |-  cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
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 addcld 
 |-  ( x e. CC -> ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) e. CC )
13 12 halfcld 
 |-  ( x e. CC -> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) e. CC )
14 1 13 fmpti 
 |-  cos : CC --> CC