Theorem logcj

Description: The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015)

	Ref	Expression
Assertion	logcj	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \log \bar{A}=\overline{\log A}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=0\to \Im \left(A\right)=\Im \left(0\right)$$
2		im0	$$⊢\Im \left(0\right)=0$$
3	1 2	eqtrdi	$$⊢A=0\to \Im \left(A\right)=0$$
4	3	necon3i	$$⊢\Im \left(A\right)\ne 0\to A\ne 0$$
5		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
6	4 5	sylan2	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \log A\in ℂ$$
7		efcj	$$⊢\log A\in ℂ\to {\mathrm{e}}^{\overline{\log A}}=\overline{{\mathrm{e}}^{\log A}}$$
8	6 7	syl	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to {\mathrm{e}}^{\overline{\log A}}=\overline{{\mathrm{e}}^{\log A}}$$
9		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
10	4 9	sylan2	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
11	10	fveq2d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \overline{{\mathrm{e}}^{\log A}}=\bar{A}$$
12	8 11	eqtrd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to {\mathrm{e}}^{\overline{\log A}}=\bar{A}$$
13		cjcl	$$⊢A\in ℂ\to \bar{A}\in ℂ$$
14	13	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \bar{A}\in ℂ$$
15		simpr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \Im \left(A\right)\ne 0$$
16	15 4	syl	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to A\ne 0$$
17		cjne0	$$⊢A\in ℂ\to \left(A\ne 0\leftrightarrow \bar{A}\ne 0\right)$$
18	17	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(A\ne 0\leftrightarrow \bar{A}\ne 0\right)$$
19	16 18	mpbid	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \bar{A}\ne 0$$
20	6	cjcld	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \overline{\log A}\in ℂ$$
21	6	imcld	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \Im \left(\log A\right)\in ℝ$$
22		pire	$$⊢\mathrm{\pi }\in ℝ$$
23	22	a1i	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \mathrm{\pi }\in ℝ$$
24		logimcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$
25	4 24	sylan2	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$
26	25	simprd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \Im \left(\log A\right)\le \mathrm{\pi }$$
27		rpre	$$⊢-A\in {ℝ}^{+}\to -A\in ℝ$$
28	27	renegcld	$$⊢-A\in {ℝ}^{+}\to -\left(-A\right)\in ℝ$$
29		negneg	$$⊢A\in ℂ\to -\left(-A\right)=A$$
30	29	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to -\left(-A\right)=A$$
31	30	eleq1d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(-\left(-A\right)\in ℝ\leftrightarrow A\in ℝ\right)$$
32	28 31	syl5ib	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(-A\in {ℝ}^{+}\to A\in ℝ\right)$$
33		lognegb	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-A\in {ℝ}^{+}\leftrightarrow \Im \left(\log A\right)=\mathrm{\pi }\right)$$
34	4 33	sylan2	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(-A\in {ℝ}^{+}\leftrightarrow \Im \left(\log A\right)=\mathrm{\pi }\right)$$
35		reim0b	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
36	35	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
37	32 34 36	3imtr3d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(\Im \left(\log A\right)=\mathrm{\pi }\to \Im \left(A\right)=0\right)$$
38	37	necon3d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(\Im \left(A\right)\ne 0\to \Im \left(\log A\right)\ne \mathrm{\pi }\right)$$
39	15 38	mpd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \Im \left(\log A\right)\ne \mathrm{\pi }$$
40	39	necomd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \mathrm{\pi }\ne \Im \left(\log A\right)$$
41	21 23 26 40	leneltd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \Im \left(\log A\right)<\mathrm{\pi }$$
42		ltneg	$$⊢\left(\Im \left(\log A\right)\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left(\Im \left(\log A\right)<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<-\Im \left(\log A\right)\right)$$
43	21 22 42	sylancl	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(\Im \left(\log A\right)<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<-\Im \left(\log A\right)\right)$$
44	41 43	mpbid	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to -\mathrm{\pi }<-\Im \left(\log A\right)$$
45	6	imcjd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \Im \left(\overline{\log A}\right)=-\Im \left(\log A\right)$$
46	44 45	breqtrrd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to -\mathrm{\pi }<\Im \left(\overline{\log A}\right)$$
47	25	simpld	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to -\mathrm{\pi }<\Im \left(\log A\right)$$
48	22	renegcli	$$⊢-\mathrm{\pi }\in ℝ$$
49		ltle	$$⊢\left(-\mathrm{\pi }\in ℝ\wedge \Im \left(\log A\right)\in ℝ\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\to -\mathrm{\pi }\le \Im \left(\log A\right)\right)$$
50	48 21 49	sylancr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\to -\mathrm{\pi }\le \Im \left(\log A\right)\right)$$
51	47 50	mpd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to -\mathrm{\pi }\le \Im \left(\log A\right)$$
52		lenegcon1	$$⊢\left(\mathrm{\pi }\in ℝ\wedge \Im \left(\log A\right)\in ℝ\right)\to \left(-\mathrm{\pi }\le \Im \left(\log A\right)\leftrightarrow -\Im \left(\log A\right)\le \mathrm{\pi }\right)$$
53	22 21 52	sylancr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(-\mathrm{\pi }\le \Im \left(\log A\right)\leftrightarrow -\Im \left(\log A\right)\le \mathrm{\pi }\right)$$
54	51 53	mpbid	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to -\Im \left(\log A\right)\le \mathrm{\pi }$$
55	45 54	eqbrtrd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \Im \left(\overline{\log A}\right)\le \mathrm{\pi }$$
56		ellogrn	$$⊢\overline{\log A}\in \mathrm{ran}log\leftrightarrow \left(\overline{\log A}\in ℂ\wedge -\mathrm{\pi }<\Im \left(\overline{\log A}\right)\wedge \Im \left(\overline{\log A}\right)\le \mathrm{\pi }\right)$$
57	20 46 55 56	syl3anbrc	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \overline{\log A}\in \mathrm{ran}log$$
58		logeftb	$$⊢\left(\bar{A}\in ℂ\wedge \bar{A}\ne 0\wedge \overline{\log A}\in \mathrm{ran}log\right)\to \left(\log \bar{A}=\overline{\log A}\leftrightarrow {\mathrm{e}}^{\overline{\log A}}=\bar{A}\right)$$
59	14 19 57 58	syl3anc	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \left(\log \bar{A}=\overline{\log A}\leftrightarrow {\mathrm{e}}^{\overline{\log A}}=\bar{A}\right)$$
60	12 59	mpbird	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \log \bar{A}=\overline{\log A}$$