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 ) )