Step |
Hyp |
Ref |
Expression |
1 |
|
eldifsn |
|- ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) ) |
2 |
|
dflog2 |
|- log = `' ( exp |` ran log ) |
3 |
2
|
fveq1i |
|- ( log ` A ) = ( `' ( exp |` ran log ) ` A ) |
4 |
3
|
eqeq1i |
|- ( ( log ` A ) = B <-> ( `' ( exp |` ran log ) ` A ) = B ) |
5 |
|
fvres |
|- ( B e. ran log -> ( ( exp |` ran log ) ` B ) = ( exp ` B ) ) |
6 |
5
|
eqeq1d |
|- ( B e. ran log -> ( ( ( exp |` ran log ) ` B ) = A <-> ( exp ` B ) = A ) ) |
7 |
6
|
adantr |
|- ( ( B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( ( exp |` ran log ) ` B ) = A <-> ( exp ` B ) = A ) ) |
8 |
|
eff1o2 |
|- ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) |
9 |
|
f1ocnvfvb |
|- ( ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) /\ B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( ( exp |` ran log ) ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) ) |
10 |
8 9
|
mp3an1 |
|- ( ( B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( ( exp |` ran log ) ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) ) |
11 |
7 10
|
bitr3d |
|- ( ( B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( exp ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) ) |
12 |
11
|
ancoms |
|- ( ( A e. ( CC \ { 0 } ) /\ B e. ran log ) -> ( ( exp ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) ) |
13 |
4 12
|
bitr4id |
|- ( ( A e. ( CC \ { 0 } ) /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) ) |
14 |
1 13
|
sylanbr |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) ) |
15 |
14
|
3impa |
|- ( ( A e. CC /\ A =/= 0 /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) ) |