This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eflogeq

Description: Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion eflogeq 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( exp ` A ) = B <-> E. n e. ZZ A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )

Proof

Step Hyp Ref Expression
1 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
2 efne0 
 |-  ( A e. CC -> ( exp ` A ) =/= 0 )
3 1 2 logcld 
 |-  ( A e. CC -> ( log ` ( exp ` A ) ) e. CC )
4 efsub 
 |-  ( ( A e. CC /\ ( log ` ( exp ` A ) ) e. CC ) -> ( exp ` ( A - ( log ` ( exp ` A ) ) ) ) = ( ( exp ` A ) / ( exp ` ( log ` ( exp ` A ) ) ) ) )
5 3 4 mpdan 
 |-  ( A e. CC -> ( exp ` ( A - ( log ` ( exp ` A ) ) ) ) = ( ( exp ` A ) / ( exp ` ( log ` ( exp ` A ) ) ) ) )
6 eflog 
 |-  ( ( ( exp ` A ) e. CC /\ ( exp ` A ) =/= 0 ) -> ( exp ` ( log ` ( exp ` A ) ) ) = ( exp ` A ) )
7 1 2 6 syl2anc 
 |-  ( A e. CC -> ( exp ` ( log ` ( exp ` A ) ) ) = ( exp ` A ) )
8 7 oveq2d 
 |-  ( A e. CC -> ( ( exp ` A ) / ( exp ` ( log ` ( exp ` A ) ) ) ) = ( ( exp ` A ) / ( exp ` A ) ) )
9 1 2 dividd 
 |-  ( A e. CC -> ( ( exp ` A ) / ( exp ` A ) ) = 1 )
10 5 8 9 3eqtrd 
 |-  ( A e. CC -> ( exp ` ( A - ( log ` ( exp ` A ) ) ) ) = 1 )
11 subcl 
 |-  ( ( A e. CC /\ ( log ` ( exp ` A ) ) e. CC ) -> ( A - ( log ` ( exp ` A ) ) ) e. CC )
12 3 11 mpdan 
 |-  ( A e. CC -> ( A - ( log ` ( exp ` A ) ) ) e. CC )
13 efeq1 
 |-  ( ( A - ( log ` ( exp ` A ) ) ) e. CC -> ( ( exp ` ( A - ( log ` ( exp ` A ) ) ) ) = 1 <-> ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
14 12 13 syl 
 |-  ( A e. CC -> ( ( exp ` ( A - ( log ` ( exp ` A ) ) ) ) = 1 <-> ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
15 10 14 mpbid 
 |-  ( A e. CC -> ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ )
16 ax-icn 
 |-  _i e. CC
17 2cn 
 |-  2 e. CC
18 picn 
 |-  _pi e. CC
19 17 18 mulcli 
 |-  ( 2 x. _pi ) e. CC
20 16 19 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
21 20 a1i 
 |-  ( A e. CC -> ( _i x. ( 2 x. _pi ) ) e. CC )
22 ine0 
 |-  _i =/= 0
23 2ne0 
 |-  2 =/= 0
24 pire 
 |-  _pi e. RR
25 pipos 
 |-  0 < _pi
26 24 25 gt0ne0ii 
 |-  _pi =/= 0
27 17 18 23 26 mulne0i 
 |-  ( 2 x. _pi ) =/= 0
28 16 19 22 27 mulne0i 
 |-  ( _i x. ( 2 x. _pi ) ) =/= 0
29 28 a1i 
 |-  ( A e. CC -> ( _i x. ( 2 x. _pi ) ) =/= 0 )
30 12 21 29 divcan2d 
 |-  ( A e. CC -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) ) = ( A - ( log ` ( exp ` A ) ) ) )
31 30 oveq2d 
 |-  ( A e. CC -> ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) ) ) = ( ( log ` ( exp ` A ) ) + ( A - ( log ` ( exp ` A ) ) ) ) )
32 pncan3 
 |-  ( ( ( log ` ( exp ` A ) ) e. CC /\ A e. CC ) -> ( ( log ` ( exp ` A ) ) + ( A - ( log ` ( exp ` A ) ) ) ) = A )
33 3 32 mpancom 
 |-  ( A e. CC -> ( ( log ` ( exp ` A ) ) + ( A - ( log ` ( exp ` A ) ) ) ) = A )
34 31 33 eqtr2d 
 |-  ( A e. CC -> A = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) ) ) )
35 oveq2 
 |-  ( n = ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( ( _i x. ( 2 x. _pi ) ) x. ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) ) )
36 35 oveq2d 
 |-  ( n = ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) -> ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) ) ) )
37 36 rspceeqv 
 |-  ( ( ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ /\ A = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( ( A - ( log ` ( exp ` A ) ) ) / ( _i x. ( 2 x. _pi ) ) ) ) ) ) -> E. n e. ZZ A = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) )
38 15 34 37 syl2anc 
 |-  ( A e. CC -> E. n e. ZZ A = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) )
39 38 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E. n e. ZZ A = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) )
40 fveq2 
 |-  ( ( exp ` A ) = B -> ( log ` ( exp ` A ) ) = ( log ` B ) )
41 40 oveq1d 
 |-  ( ( exp ` A ) = B -> ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) )
42 41 eqeq2d 
 |-  ( ( exp ` A ) = B -> ( A = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )
43 42 rexbidv 
 |-  ( ( exp ` A ) = B -> ( E. n e. ZZ A = ( ( log ` ( exp ` A ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> E. n e. ZZ A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )
44 39 43 syl5ibcom 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( exp ` A ) = B -> E. n e. ZZ A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )
45 logcl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( log ` B ) e. CC )
46 45 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( log ` B ) e. CC )
47 zcn 
 |-  ( n e. ZZ -> n e. CC )
48 47 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> n e. CC )
49 mulcl 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) e. CC /\ n e. CC ) -> ( ( _i x. ( 2 x. _pi ) ) x. n ) e. CC )
50 20 48 49 sylancr 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> ( ( _i x. ( 2 x. _pi ) ) x. n ) e. CC )
51 efadd 
 |-  ( ( ( log ` B ) e. CC /\ ( ( _i x. ( 2 x. _pi ) ) x. n ) e. CC ) -> ( exp ` ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) = ( ( exp ` ( log ` B ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )
52 46 50 51 syl2an2r 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> ( exp ` ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) = ( ( exp ` ( log ` B ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )
53 eflog 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( exp ` ( log ` B ) ) = B )
54 53 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( exp ` ( log ` B ) ) = B )
55 ef2kpi 
 |-  ( n e. ZZ -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. n ) ) = 1 )
56 54 55 oveqan12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> ( ( exp ` ( log ` B ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) = ( B x. 1 ) )
57 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> B e. CC )
58 57 mulridd 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> ( B x. 1 ) = B )
59 52 56 58 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> ( exp ` ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) = B )
60 fveqeq2 
 |-  ( A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) -> ( ( exp ` A ) = B <-> ( exp ` ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) = B ) )
61 59 60 syl5ibrcom 
 |-  ( ( ( A e. CC /\ B e. CC /\ B =/= 0 ) /\ n e. ZZ ) -> ( A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) -> ( exp ` A ) = B ) )
62 61 rexlimdva 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( E. n e. ZZ A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) -> ( exp ` A ) = B ) )
63 44 62 impbid 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( exp ` A ) = B <-> E. n e. ZZ A = ( ( log ` B ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )