Step |
Hyp |
Ref |
Expression |
1 |
|
ef11d.a |
|- ( ph -> A e. CC ) |
2 |
|
ef11d.b |
|- ( ph -> B e. CC ) |
3 |
1 2
|
efsubd |
|- ( ph -> ( exp ` ( A - B ) ) = ( ( exp ` A ) / ( exp ` B ) ) ) |
4 |
3
|
eqeq1d |
|- ( ph -> ( ( exp ` ( A - B ) ) = 1 <-> ( ( exp ` A ) / ( exp ` B ) ) = 1 ) ) |
5 |
|
ax-icn |
|- _i e. CC |
6 |
5
|
a1i |
|- ( ph -> _i e. CC ) |
7 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
8 |
|
picn |
|- _pi e. CC |
9 |
8
|
a1i |
|- ( ph -> _pi e. CC ) |
10 |
7 9
|
mulcld |
|- ( ph -> ( 2 x. _pi ) e. CC ) |
11 |
6 10
|
mulcld |
|- ( ph -> ( _i x. ( 2 x. _pi ) ) e. CC ) |
12 |
1 2
|
subcld |
|- ( ph -> ( A - B ) e. CC ) |
13 |
|
ine0 |
|- _i =/= 0 |
14 |
13
|
a1i |
|- ( ph -> _i =/= 0 ) |
15 |
|
2ne0 |
|- 2 =/= 0 |
16 |
15
|
a1i |
|- ( ph -> 2 =/= 0 ) |
17 |
|
pine0 |
|- _pi =/= 0 |
18 |
17
|
a1i |
|- ( ph -> _pi =/= 0 ) |
19 |
7 9 16 18
|
mulne0d |
|- ( ph -> ( 2 x. _pi ) =/= 0 ) |
20 |
6 10 14 19
|
mulne0d |
|- ( ph -> ( _i x. ( 2 x. _pi ) ) =/= 0 ) |
21 |
11 12 20
|
zdivgd |
|- ( ph -> ( E. n e. ZZ ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) <-> ( ( A - B ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) ) |
22 |
|
eqcom |
|- ( A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) = A ) |
23 |
2
|
adantr |
|- ( ( ph /\ n e. ZZ ) -> B e. CC ) |
24 |
11
|
adantr |
|- ( ( ph /\ n e. ZZ ) -> ( _i x. ( 2 x. _pi ) ) e. CC ) |
25 |
|
zcn |
|- ( n e. ZZ -> n e. CC ) |
26 |
25
|
adantl |
|- ( ( ph /\ n e. ZZ ) -> n e. CC ) |
27 |
24 26
|
mulcld |
|- ( ( ph /\ n e. ZZ ) -> ( ( _i x. ( 2 x. _pi ) ) x. n ) e. CC ) |
28 |
1
|
adantr |
|- ( ( ph /\ n e. ZZ ) -> A e. CC ) |
29 |
23 27 28
|
addrsub |
|- ( ( ph /\ n e. ZZ ) -> ( ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) = A <-> ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) ) ) |
30 |
22 29
|
bitrid |
|- ( ( ph /\ n e. ZZ ) -> ( A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) ) ) |
31 |
30
|
rexbidva |
|- ( ph -> ( E. n e. ZZ A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> E. n e. ZZ ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) ) ) |
32 |
|
efeq1 |
|- ( ( A - B ) e. CC -> ( ( exp ` ( A - B ) ) = 1 <-> ( ( A - B ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) ) |
33 |
12 32
|
syl |
|- ( ph -> ( ( exp ` ( A - B ) ) = 1 <-> ( ( A - B ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) ) |
34 |
21 31 33
|
3bitr4rd |
|- ( ph -> ( ( exp ` ( A - B ) ) = 1 <-> E. n e. ZZ A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) ) |
35 |
1
|
efcld |
|- ( ph -> ( exp ` A ) e. CC ) |
36 |
2
|
efcld |
|- ( ph -> ( exp ` B ) e. CC ) |
37 |
2
|
efne0d |
|- ( ph -> ( exp ` B ) =/= 0 ) |
38 |
35 36 37
|
diveq1ad |
|- ( ph -> ( ( ( exp ` A ) / ( exp ` B ) ) = 1 <-> ( exp ` A ) = ( exp ` B ) ) ) |
39 |
4 34 38
|
3bitr3rd |
|- ( ph -> ( ( exp ` A ) = ( exp ` B ) <-> E. n e. ZZ A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) ) |