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