Metamath Proof Explorer

Theorem cos0

Description: Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion cos0 
|- ( cos ` 0 ) = 1

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 recosval 
 |-  ( 0 e. RR -> ( cos ` 0 ) = ( Re ` ( exp ` ( _i x. 0 ) ) ) )
3 1 2 ax-mp 
 |-  ( cos ` 0 ) = ( Re ` ( exp ` ( _i x. 0 ) ) )
4 it0e0 
 |-  ( _i x. 0 ) = 0
5 4 fveq2i 
 |-  ( exp ` ( _i x. 0 ) ) = ( exp ` 0 )
6 ef0 
 |-  ( exp ` 0 ) = 1
7 5 6 eqtri 
 |-  ( exp ` ( _i x. 0 ) ) = 1
8 7 fveq2i 
 |-  ( Re ` ( exp ` ( _i x. 0 ) ) ) = ( Re ` 1 )
9 re1 
 |-  ( Re ` 1 ) = 1
10 8 9 eqtri 
 |-  ( Re ` ( exp ` ( _i x. 0 ) ) ) = 1
11 3 10 eqtri 
 |-  ( cos ` 0 ) = 1