Theorem eflogeq

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

	Ref	Expression
Assertion	eflogeq	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left({\mathrm{e}}^A=B\leftrightarrow \exists n\in \mathbb{Z}A=\log B+\mathrm{i}2\mathrm{\pi }n\right)$$

Proof

Step	Hyp	Ref	Expression
1		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
2		efne0	$$⊢A\in ℂ\to {\mathrm{e}}^A\ne 0$$
3	1 2	logcld	$$⊢A\in ℂ\to \log {\mathrm{e}}^A\in ℂ$$
4		efsub	$$⊢\left(A\in ℂ\wedge \log {\mathrm{e}}^A\in ℂ\right)\to {\mathrm{e}}^{A-\log {\mathrm{e}}^A}=\frac{{\mathrm{e}}^A}{{\mathrm{e}}^{\log {\mathrm{e}}^A}}$$
5	3 4	mpdan	$$⊢A\in ℂ\to {\mathrm{e}}^{A-\log {\mathrm{e}}^A}=\frac{{\mathrm{e}}^A}{{\mathrm{e}}^{\log {\mathrm{e}}^A}}$$
6		eflog	$$⊢\left({\mathrm{e}}^A\in ℂ\wedge {\mathrm{e}}^A\ne 0\right)\to {\mathrm{e}}^{\log {\mathrm{e}}^A}={\mathrm{e}}^A$$
7	1 2 6	syl2anc	$$⊢A\in ℂ\to {\mathrm{e}}^{\log {\mathrm{e}}^A}={\mathrm{e}}^A$$
8	7	oveq2d	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^A}{{\mathrm{e}}^{\log {\mathrm{e}}^A}}=\frac{{\mathrm{e}}^A}{{\mathrm{e}}^A}$$
9	1 2	dividd	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^A}{{\mathrm{e}}^A}=1$$
10	5 8 9	3eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^{A-\log {\mathrm{e}}^A}=1$$
11		subcl	$$⊢\left(A\in ℂ\wedge \log {\mathrm{e}}^A\in ℂ\right)\to A-\log {\mathrm{e}}^A\in ℂ$$
12	3 11	mpdan	$$⊢A\in ℂ\to A-\log {\mathrm{e}}^A\in ℂ$$
13		efeq1	$$⊢A-\log {\mathrm{e}}^A\in ℂ\to \left({\mathrm{e}}^{A-\log {\mathrm{e}}^A}=1\leftrightarrow \frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}\right)$$
14	12 13	syl	$$⊢A\in ℂ\to \left({\mathrm{e}}^{A-\log {\mathrm{e}}^A}=1\leftrightarrow \frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}\right)$$
15	10 14	mpbid	$$⊢A\in ℂ\to \frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}$$
16		ax-icn	$$⊢\mathrm{i}\in ℂ$$
17		2cn	$$⊢2\in ℂ$$
18		picn	$$⊢\mathrm{\pi }\in ℂ$$
19	17 18	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
20	16 19	mulcli	$$⊢\mathrm{i}2\mathrm{\pi }\in ℂ$$
21	20	a1i	$$⊢A\in ℂ\to \mathrm{i}2\mathrm{\pi }\in ℂ$$
22		ine0	$$⊢\mathrm{i}\ne 0$$
23		2ne0	$$⊢2\ne 0$$
24		pire	$$⊢\mathrm{\pi }\in ℝ$$
25		pipos	$$⊢0<\mathrm{\pi }$$
26	24 25	gt0ne0ii	$$⊢\mathrm{\pi }\ne 0$$
27	17 18 23 26	mulne0i	$$⊢2\mathrm{\pi }\ne 0$$
28	16 19 22 27	mulne0i	$$⊢\mathrm{i}2\mathrm{\pi }\ne 0$$
29	28	a1i	$$⊢A\in ℂ\to \mathrm{i}2\mathrm{\pi }\ne 0$$
30	12 21 29	divcan2d	$$⊢A\in ℂ\to \mathrm{i}2\mathrm{\pi }\left(\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\right)=A-\log {\mathrm{e}}^A$$
31	30	oveq2d	$$⊢A\in ℂ\to \log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }\left(\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\right)=\log {\mathrm{e}}^A+A-\log {\mathrm{e}}^A$$
32		pncan3	$$⊢\left(\log {\mathrm{e}}^A\in ℂ\wedge A\in ℂ\right)\to \log {\mathrm{e}}^A+A-\log {\mathrm{e}}^A=A$$
33	3 32	mpancom	$$⊢A\in ℂ\to \log {\mathrm{e}}^A+A-\log {\mathrm{e}}^A=A$$
34	31 33	eqtr2d	$$⊢A\in ℂ\to A=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }\left(\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\right)$$
35		oveq2	$$⊢n=\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\to \mathrm{i}2\mathrm{\pi }n=\mathrm{i}2\mathrm{\pi }\left(\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\right)$$
36	35	oveq2d	$$⊢n=\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\to \log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }n=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }\left(\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\right)$$
37	36	rspceeqv	$$⊢\left(\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}\wedge A=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }\left(\frac{A-\log {\mathrm{e}}^A}{\mathrm{i}2\mathrm{\pi }}\right)\right)\to \exists n\in \mathbb{Z}A=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }n$$
38	15 34 37	syl2anc	$$⊢A\in ℂ\to \exists n\in \mathbb{Z}A=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }n$$
39	38	3ad2ant1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \exists n\in \mathbb{Z}A=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }n$$
40		fveq2	$$⊢{\mathrm{e}}^A=B\to \log {\mathrm{e}}^A=\log B$$
41	40	oveq1d	$$⊢{\mathrm{e}}^A=B\to \log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }n=\log B+\mathrm{i}2\mathrm{\pi }n$$
42	41	eqeq2d	$$⊢{\mathrm{e}}^A=B\to \left(A=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }n\leftrightarrow A=\log B+\mathrm{i}2\mathrm{\pi }n\right)$$
43	42	rexbidv	$$⊢{\mathrm{e}}^A=B\to \left(\exists n\in \mathbb{Z}A=\log {\mathrm{e}}^A+\mathrm{i}2\mathrm{\pi }n\leftrightarrow \exists n\in \mathbb{Z}A=\log B+\mathrm{i}2\mathrm{\pi }n\right)$$
44	39 43	syl5ibcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left({\mathrm{e}}^A=B\to \exists n\in \mathbb{Z}A=\log B+\mathrm{i}2\mathrm{\pi }n\right)$$
45		logcl	$$⊢\left(B\in ℂ\wedge B\ne 0\right)\to \log B\in ℂ$$
46	45	3adant1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \log B\in ℂ$$
47		zcn	$$⊢n\in \mathbb{Z}\to n\in ℂ$$
48	47	adantl	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to n\in ℂ$$
49		mulcl	$$⊢\left(\mathrm{i}2\mathrm{\pi }\in ℂ\wedge n\in ℂ\right)\to \mathrm{i}2\mathrm{\pi }n\in ℂ$$
50	20 48 49	sylancr	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to \mathrm{i}2\mathrm{\pi }n\in ℂ$$
51		efadd	$$⊢\left(\log B\in ℂ\wedge \mathrm{i}2\mathrm{\pi }n\in ℂ\right)\to {\mathrm{e}}^{\log B+\mathrm{i}2\mathrm{\pi }n}={\mathrm{e}}^{\log B}{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }n}$$
52	46 50 51	syl2an2r	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to {\mathrm{e}}^{\log B+\mathrm{i}2\mathrm{\pi }n}={\mathrm{e}}^{\log B}{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }n}$$
53		eflog	$$⊢\left(B\in ℂ\wedge B\ne 0\right)\to {\mathrm{e}}^{\log B}=B$$
54	53	3adant1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to {\mathrm{e}}^{\log B}=B$$
55		ef2kpi	$$⊢n\in \mathbb{Z}\to {\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }n}=1$$
56	54 55	oveqan12d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to {\mathrm{e}}^{\log B}{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }n}=B\cdot 1$$
57		simpl2	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to B\in ℂ$$
58	57	mulid1d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to B\cdot 1=B$$
59	52 56 58	3eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to {\mathrm{e}}^{\log B+\mathrm{i}2\mathrm{\pi }n}=B$$
60		fveqeq2	$$⊢A=\log B+\mathrm{i}2\mathrm{\pi }n\to \left({\mathrm{e}}^A=B\leftrightarrow {\mathrm{e}}^{\log B+\mathrm{i}2\mathrm{\pi }n}=B\right)$$
61	59 60	syl5ibrcom	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\wedge n\in \mathbb{Z}\right)\to \left(A=\log B+\mathrm{i}2\mathrm{\pi }n\to {\mathrm{e}}^A=B\right)$$
62	61	rexlimdva	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\exists n\in \mathbb{Z}A=\log B+\mathrm{i}2\mathrm{\pi }n\to {\mathrm{e}}^A=B\right)$$
63	44 62	impbid	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left({\mathrm{e}}^A=B\leftrightarrow \exists n\in \mathbb{Z}A=\log B+\mathrm{i}2\mathrm{\pi }n\right)$$