This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ef2kpi

Description: If K is an integer, then the exponential of 2 Kpi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion ef2kpi 
|- ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) = 1 )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 2cn 
 |-  2 e. CC
3 picn 
 |-  _pi e. CC
4 2 3 mulcli 
 |-  ( 2 x. _pi ) e. CC
5 1 4 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
6 zcn 
 |-  ( K e. ZZ -> K e. CC )
7 mulcom 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) e. CC /\ K e. CC ) -> ( ( _i x. ( 2 x. _pi ) ) x. K ) = ( K x. ( _i x. ( 2 x. _pi ) ) ) )
8 5 6 7 sylancr 
 |-  ( K e. ZZ -> ( ( _i x. ( 2 x. _pi ) ) x. K ) = ( K x. ( _i x. ( 2 x. _pi ) ) ) )
9 8 fveq2d 
 |-  ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) = ( exp ` ( K x. ( _i x. ( 2 x. _pi ) ) ) ) )
10 efexp 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) e. CC /\ K e. ZZ ) -> ( exp ` ( K x. ( _i x. ( 2 x. _pi ) ) ) ) = ( ( exp ` ( _i x. ( 2 x. _pi ) ) ) ^ K ) )
11 5 10 mpan 
 |-  ( K e. ZZ -> ( exp ` ( K x. ( _i x. ( 2 x. _pi ) ) ) ) = ( ( exp ` ( _i x. ( 2 x. _pi ) ) ) ^ K ) )
12 ef2pi 
 |-  ( exp ` ( _i x. ( 2 x. _pi ) ) ) = 1
13 12 oveq1i 
 |-  ( ( exp ` ( _i x. ( 2 x. _pi ) ) ) ^ K ) = ( 1 ^ K )
14 1exp 
 |-  ( K e. ZZ -> ( 1 ^ K ) = 1 )
15 13 14 eqtrid 
 |-  ( K e. ZZ -> ( ( exp ` ( _i x. ( 2 x. _pi ) ) ) ^ K ) = 1 )
16 9 11 15 3eqtrd 
 |-  ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) = 1 )