Metamath Proof Explorer

Theorem efper

Description: The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008) (Proof shortened by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion efper 
|- ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( exp ` A ) )

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 mulcl 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) e. CC /\ K e. CC ) -> ( ( _i x. ( 2 x. _pi ) ) x. K ) e. CC )
8 5 6 7 sylancr 
 |-  ( K e. ZZ -> ( ( _i x. ( 2 x. _pi ) ) x. K ) e. CC )
9 efadd 
 |-  ( ( A e. CC /\ ( ( _i x. ( 2 x. _pi ) ) x. K ) e. CC ) -> ( exp ` ( A + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( ( exp ` A ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) )
10 8 9 sylan2 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( ( exp ` A ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) )
11 ef2kpi 
 |-  ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) = 1 )
12 11 oveq2d 
 |-  ( K e. ZZ -> ( ( exp ` A ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( ( exp ` A ) x. 1 ) )
13 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
14 13 mulid1d 
 |-  ( A e. CC -> ( ( exp ` A ) x. 1 ) = ( exp ` A ) )
15 12 14 sylan9eqr 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( ( exp ` A ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( exp ` A ) )
16 10 15 eqtrd 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( exp ` A ) )