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