# Metamath Proof Explorer

## Theorem logneg2

Description: The logarithm of the negative of a number with positive imaginary part is _i x. _pi less than the original. (Compare logneg .) (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion logneg2 ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{log}\left(-{A}\right)=\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }$

### Proof

Step Hyp Ref Expression
1 imcl ${⊢}{A}\in ℂ\to \Im \left({A}\right)\in ℝ$
2 gt0ne0 ${⊢}\left(\Im \left({A}\right)\in ℝ\wedge 0<\Im \left({A}\right)\right)\to \Im \left({A}\right)\ne 0$
3 1 2 sylan ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left({A}\right)\ne 0$
4 fveq2 ${⊢}{A}=0\to \Im \left({A}\right)=\Im \left(0\right)$
5 im0 ${⊢}\Im \left(0\right)=0$
6 4 5 syl6eq ${⊢}{A}=0\to \Im \left({A}\right)=0$
7 6 necon3i ${⊢}\Im \left({A}\right)\ne 0\to {A}\ne 0$
8 3 7 syl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to {A}\ne 0$
9 logcl ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \mathrm{log}{A}\in ℂ$
10 8 9 syldan ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{log}{A}\in ℂ$
11 ax-icn ${⊢}\mathrm{i}\in ℂ$
12 picn ${⊢}\mathrm{\pi }\in ℂ$
13 11 12 mulcli ${⊢}\mathrm{i}\mathrm{\pi }\in ℂ$
14 efsub ${⊢}\left(\mathrm{log}{A}\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to {\mathrm{e}}^{\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }}=\frac{{\mathrm{e}}^{\mathrm{log}{A}}}{{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}}$
15 10 13 14 sylancl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to {\mathrm{e}}^{\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }}=\frac{{\mathrm{e}}^{\mathrm{log}{A}}}{{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}}$
16 eflog ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {\mathrm{e}}^{\mathrm{log}{A}}={A}$
17 8 16 syldan ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to {\mathrm{e}}^{\mathrm{log}{A}}={A}$
18 efipi ${⊢}{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=-1$
19 18 a1i ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to {\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=-1$
20 17 19 oveq12d ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \frac{{\mathrm{e}}^{\mathrm{log}{A}}}{{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}}=\frac{{A}}{-1}$
21 ax-1cn ${⊢}1\in ℂ$
22 ax-1ne0 ${⊢}1\ne 0$
23 divneg2 ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\wedge 1\ne 0\right)\to -\frac{{A}}{1}=\frac{{A}}{-1}$
24 21 22 23 mp3an23 ${⊢}{A}\in ℂ\to -\frac{{A}}{1}=\frac{{A}}{-1}$
25 div1 ${⊢}{A}\in ℂ\to \frac{{A}}{1}={A}$
26 25 negeqd ${⊢}{A}\in ℂ\to -\frac{{A}}{1}=-{A}$
27 24 26 eqtr3d ${⊢}{A}\in ℂ\to \frac{{A}}{-1}=-{A}$
28 27 adantr ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \frac{{A}}{-1}=-{A}$
29 15 20 28 3eqtrd ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to {\mathrm{e}}^{\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }}=-{A}$
30 29 fveq2d ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{log}{\mathrm{e}}^{\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }}=\mathrm{log}\left(-{A}\right)$
31 subcl ${⊢}\left(\mathrm{log}{A}\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to \mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\in ℂ$
32 10 13 31 sylancl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\in ℂ$
33 argimgt0 ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)\in \left(0,\mathrm{\pi }\right)$
34 eliooord ${⊢}\Im \left(\mathrm{log}{A}\right)\in \left(0,\mathrm{\pi }\right)\to \left(0<\Im \left(\mathrm{log}{A}\right)\wedge \Im \left(\mathrm{log}{A}\right)<\mathrm{\pi }\right)$
35 33 34 syl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \left(0<\Im \left(\mathrm{log}{A}\right)\wedge \Im \left(\mathrm{log}{A}\right)<\mathrm{\pi }\right)$
36 35 simpld ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to 0<\Im \left(\mathrm{log}{A}\right)$
37 imcl ${⊢}\mathrm{log}{A}\in ℂ\to \Im \left(\mathrm{log}{A}\right)\in ℝ$
38 10 37 syl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)\in ℝ$
39 pire ${⊢}\mathrm{\pi }\in ℝ$
40 39 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
41 ltaddpos2 ${⊢}\left(\Im \left(\mathrm{log}{A}\right)\in ℝ\wedge -\mathrm{\pi }\in ℝ\right)\to \left(0<\Im \left(\mathrm{log}{A}\right)↔-\mathrm{\pi }<\Im \left(\mathrm{log}{A}\right)+\left(-\mathrm{\pi }\right)\right)$
42 38 40 41 sylancl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \left(0<\Im \left(\mathrm{log}{A}\right)↔-\mathrm{\pi }<\Im \left(\mathrm{log}{A}\right)+\left(-\mathrm{\pi }\right)\right)$
43 36 42 mpbid ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to -\mathrm{\pi }<\Im \left(\mathrm{log}{A}\right)+\left(-\mathrm{\pi }\right)$
44 38 recnd ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)\in ℂ$
45 negsub ${⊢}\left(\Im \left(\mathrm{log}{A}\right)\in ℂ\wedge \mathrm{\pi }\in ℂ\right)\to \Im \left(\mathrm{log}{A}\right)+\left(-\mathrm{\pi }\right)=\Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }$
46 44 12 45 sylancl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)+\left(-\mathrm{\pi }\right)=\Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }$
47 43 46 breqtrd ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to -\mathrm{\pi }<\Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }$
48 imsub ${⊢}\left(\mathrm{log}{A}\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to \Im \left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\right)=\Im \left(\mathrm{log}{A}\right)-\Im \left(\mathrm{i}\mathrm{\pi }\right)$
49 10 13 48 sylancl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\right)=\Im \left(\mathrm{log}{A}\right)-\Im \left(\mathrm{i}\mathrm{\pi }\right)$
50 reim ${⊢}\mathrm{\pi }\in ℂ\to \Re \left(\mathrm{\pi }\right)=\Im \left(\mathrm{i}\mathrm{\pi }\right)$
51 12 50 ax-mp ${⊢}\Re \left(\mathrm{\pi }\right)=\Im \left(\mathrm{i}\mathrm{\pi }\right)$
52 rere ${⊢}\mathrm{\pi }\in ℝ\to \Re \left(\mathrm{\pi }\right)=\mathrm{\pi }$
53 39 52 ax-mp ${⊢}\Re \left(\mathrm{\pi }\right)=\mathrm{\pi }$
54 51 53 eqtr3i ${⊢}\Im \left(\mathrm{i}\mathrm{\pi }\right)=\mathrm{\pi }$
55 54 oveq2i ${⊢}\Im \left(\mathrm{log}{A}\right)-\Im \left(\mathrm{i}\mathrm{\pi }\right)=\Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }$
56 49 55 syl6eq ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\right)=\Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }$
57 47 56 breqtrrd ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to -\mathrm{\pi }<\Im \left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\right)$
58 resubcl ${⊢}\left(\Im \left(\mathrm{log}{A}\right)\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }\in ℝ$
59 38 39 58 sylancl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }\in ℝ$
60 39 a1i ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{\pi }\in ℝ$
61 0re ${⊢}0\in ℝ$
62 pipos ${⊢}0<\mathrm{\pi }$
63 61 39 62 ltleii ${⊢}0\le \mathrm{\pi }$
64 subge02 ${⊢}\left(\Im \left(\mathrm{log}{A}\right)\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left(0\le \mathrm{\pi }↔\Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }\le \Im \left(\mathrm{log}{A}\right)\right)$
65 38 39 64 sylancl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \left(0\le \mathrm{\pi }↔\Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }\le \Im \left(\mathrm{log}{A}\right)\right)$
66 63 65 mpbii ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }\le \Im \left(\mathrm{log}{A}\right)$
67 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)$
68 8 67 syldan ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \left(-\mathrm{\pi }<\Im \left(\mathrm{log}{A}\right)\wedge \Im \left(\mathrm{log}{A}\right)\le \mathrm{\pi }\right)$
69 68 simprd ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)\le \mathrm{\pi }$
70 59 38 60 66 69 letrd ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}\right)-\mathrm{\pi }\le \mathrm{\pi }$
71 56 70 eqbrtrd ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \Im \left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\right)\le \mathrm{\pi }$
72 ellogrn ${⊢}\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\in \mathrm{ran}log↔\left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\in ℂ\wedge -\mathrm{\pi }<\Im \left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\right)\wedge \Im \left(\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\right)\le \mathrm{\pi }\right)$
73 32 57 71 72 syl3anbrc ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\in \mathrm{ran}log$
74 logef ${⊢}\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }\in \mathrm{ran}log\to \mathrm{log}{\mathrm{e}}^{\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }}=\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }$
75 73 74 syl ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{log}{\mathrm{e}}^{\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }}=\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }$
76 30 75 eqtr3d ${⊢}\left({A}\in ℂ\wedge 0<\Im \left({A}\right)\right)\to \mathrm{log}\left(-{A}\right)=\mathrm{log}{A}-\mathrm{i}\mathrm{\pi }$