Metamath Proof Explorer

Theorem ef2pi

Description: The exponential of 2pi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion ef2pi 
|- ( exp ` ( _i x. ( 2 x. _pi ) ) ) = 1

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 picn 
 |-  _pi e. CC
3 1 2 mulcli 
 |-  ( 2 x. _pi ) e. CC
4 efival 
 |-  ( ( 2 x. _pi ) e. CC -> ( exp ` ( _i x. ( 2 x. _pi ) ) ) = ( ( cos ` ( 2 x. _pi ) ) + ( _i x. ( sin ` ( 2 x. _pi ) ) ) ) )
5 3 4 ax-mp 
 |-  ( exp ` ( _i x. ( 2 x. _pi ) ) ) = ( ( cos ` ( 2 x. _pi ) ) + ( _i x. ( sin ` ( 2 x. _pi ) ) ) )
6 cos2pi 
 |-  ( cos ` ( 2 x. _pi ) ) = 1
7 sin2pi 
 |-  ( sin ` ( 2 x. _pi ) ) = 0
8 7 oveq2i 
 |-  ( _i x. ( sin ` ( 2 x. _pi ) ) ) = ( _i x. 0 )
9 it0e0 
 |-  ( _i x. 0 ) = 0
10 8 9 eqtri 
 |-  ( _i x. ( sin ` ( 2 x. _pi ) ) ) = 0
11 6 10 oveq12i 
 |-  ( ( cos ` ( 2 x. _pi ) ) + ( _i x. ( sin ` ( 2 x. _pi ) ) ) ) = ( 1 + 0 )
12 1p0e1 
 |-  ( 1 + 0 ) = 1
13 11 12 eqtri 
 |-  ( ( cos ` ( 2 x. _pi ) ) + ( _i x. ( sin ` ( 2 x. _pi ) ) ) ) = 1
14 5 13 eqtri 
 |-  ( exp ` ( _i x. ( 2 x. _pi ) ) ) = 1