# Metamath Proof Explorer

## 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 \mathrm{log}\stackrel{‾}{{A}}=\stackrel{‾}{\mathrm{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 syl6eq ${⊢}{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 \mathrm{log}{A}\in ℂ$
6 4 5 sylan2 ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \mathrm{log}{A}\in ℂ$
7 efcj ${⊢}\mathrm{log}{A}\in ℂ\to {\mathrm{e}}^{\stackrel{‾}{\mathrm{log}{A}}}=\stackrel{‾}{{\mathrm{e}}^{\mathrm{log}{A}}}$
8 6 7 syl ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to {\mathrm{e}}^{\stackrel{‾}{\mathrm{log}{A}}}=\stackrel{‾}{{\mathrm{e}}^{\mathrm{log}{A}}}$
9 eflog ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {\mathrm{e}}^{\mathrm{log}{A}}={A}$
10 4 9 sylan2 ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to {\mathrm{e}}^{\mathrm{log}{A}}={A}$
11 10 fveq2d ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \stackrel{‾}{{\mathrm{e}}^{\mathrm{log}{A}}}=\stackrel{‾}{{A}}$
12 8 11 eqtrd ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to {\mathrm{e}}^{\stackrel{‾}{\mathrm{log}{A}}}=\stackrel{‾}{{A}}$
13 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
14 13 adantr ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \stackrel{‾}{{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↔\stackrel{‾}{{A}}\ne 0\right)$
18 17 adantr ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \left({A}\ne 0↔\stackrel{‾}{{A}}\ne 0\right)$
19 16 18 mpbid ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \stackrel{‾}{{A}}\ne 0$
20 6 cjcld ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \stackrel{‾}{\mathrm{log}{A}}\in ℂ$
21 6 imcld ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \Im \left(\mathrm{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(\mathrm{log}{A}\right)\wedge \Im \left(\mathrm{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(\mathrm{log}{A}\right)\wedge \Im \left(\mathrm{log}{A}\right)\le \mathrm{\pi }\right)$
26 25 simprd ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \Im \left(\mathrm{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 ℝ↔{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 {ℝ}^{+}↔\Im \left(\mathrm{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 {ℝ}^{+}↔\Im \left(\mathrm{log}{A}\right)=\mathrm{\pi }\right)$
35 reim0b ${⊢}{A}\in ℂ\to \left({A}\in ℝ↔\Im \left({A}\right)=0\right)$
36 35 adantr ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \left({A}\in ℝ↔\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(\mathrm{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(\mathrm{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(\mathrm{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(\mathrm{log}{A}\right)$
41 21 23 26 40 leneltd ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \Im \left(\mathrm{log}{A}\right)<\mathrm{\pi }$
42 ltneg ${⊢}\left(\Im \left(\mathrm{log}{A}\right)\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left(\Im \left(\mathrm{log}{A}\right)<\mathrm{\pi }↔-\mathrm{\pi }<-\Im \left(\mathrm{log}{A}\right)\right)$
43 21 22 42 sylancl ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \left(\Im \left(\mathrm{log}{A}\right)<\mathrm{\pi }↔-\mathrm{\pi }<-\Im \left(\mathrm{log}{A}\right)\right)$
44 41 43 mpbid ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to -\mathrm{\pi }<-\Im \left(\mathrm{log}{A}\right)$
45 6 imcjd ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \Im \left(\stackrel{‾}{\mathrm{log}{A}}\right)=-\Im \left(\mathrm{log}{A}\right)$
46 44 45 breqtrrd ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to -\mathrm{\pi }<\Im \left(\stackrel{‾}{\mathrm{log}{A}}\right)$
47 25 simpld ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to -\mathrm{\pi }<\Im \left(\mathrm{log}{A}\right)$
48 22 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
49 ltle ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \Im \left(\mathrm{log}{A}\right)\in ℝ\right)\to \left(-\mathrm{\pi }<\Im \left(\mathrm{log}{A}\right)\to -\mathrm{\pi }\le \Im \left(\mathrm{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(\mathrm{log}{A}\right)\to -\mathrm{\pi }\le \Im \left(\mathrm{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(\mathrm{log}{A}\right)$
52 lenegcon1 ${⊢}\left(\mathrm{\pi }\in ℝ\wedge \Im \left(\mathrm{log}{A}\right)\in ℝ\right)\to \left(-\mathrm{\pi }\le \Im \left(\mathrm{log}{A}\right)↔-\Im \left(\mathrm{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(\mathrm{log}{A}\right)↔-\Im \left(\mathrm{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(\mathrm{log}{A}\right)\le \mathrm{\pi }$
55 45 54 eqbrtrd ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \Im \left(\stackrel{‾}{\mathrm{log}{A}}\right)\le \mathrm{\pi }$
56 ellogrn ${⊢}\stackrel{‾}{\mathrm{log}{A}}\in \mathrm{ran}log↔\left(\stackrel{‾}{\mathrm{log}{A}}\in ℂ\wedge -\mathrm{\pi }<\Im \left(\stackrel{‾}{\mathrm{log}{A}}\right)\wedge \Im \left(\stackrel{‾}{\mathrm{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 \stackrel{‾}{\mathrm{log}{A}}\in \mathrm{ran}log$
58 logeftb ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge \stackrel{‾}{{A}}\ne 0\wedge \stackrel{‾}{\mathrm{log}{A}}\in \mathrm{ran}log\right)\to \left(\mathrm{log}\stackrel{‾}{{A}}=\stackrel{‾}{\mathrm{log}{A}}↔{\mathrm{e}}^{\stackrel{‾}{\mathrm{log}{A}}}=\stackrel{‾}{{A}}\right)$
59 14 19 57 58 syl3anc ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \left(\mathrm{log}\stackrel{‾}{{A}}=\stackrel{‾}{\mathrm{log}{A}}↔{\mathrm{e}}^{\stackrel{‾}{\mathrm{log}{A}}}=\stackrel{‾}{{A}}\right)$
60 12 59 mpbird ${⊢}\left({A}\in ℂ\wedge \Im \left({A}\right)\ne 0\right)\to \mathrm{log}\stackrel{‾}{{A}}=\stackrel{‾}{\mathrm{log}{A}}$