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 \log \left(-A\right)=\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	eqtrdi	$$⊢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 \log A\in ℂ$$
10	8 9	syldan	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \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(\log A\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to {\mathrm{e}}^{\log A-\mathrm{i}\mathrm{\pi }}=\frac{{\mathrm{e}}^{\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}}^{\log A-\mathrm{i}\mathrm{\pi }}=\frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}}$$
16		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
17	8 16	syldan	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to {\mathrm{e}}^{\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}}^{\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}}^{\log A-\mathrm{i}\mathrm{\pi }}=-A$$
30	29	fveq2d	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \log {\mathrm{e}}^{\log A-\mathrm{i}\mathrm{\pi }}=\log \left(-A\right)$$
31		subcl	$$⊢\left(\log A\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to \log A-\mathrm{i}\mathrm{\pi }\in ℂ$$
32	10 13 31	sylancl	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \log A-\mathrm{i}\mathrm{\pi }\in ℂ$$
33		argimgt0	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\log A\right)\in \left(0,\mathrm{\pi }\right)$$
34		eliooord	$$⊢\Im \left(\log A\right)\in \left(0,\mathrm{\pi }\right)\to \left(0<\Im \left(\log A\right)\wedge \Im \left(\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(\log A\right)\wedge \Im \left(\log A\right)<\mathrm{\pi }\right)$$
36	35	simpld	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to 0<\Im \left(\log A\right)$$
37		imcl	$$⊢\log A\in ℂ\to \Im \left(\log A\right)\in ℝ$$
38	10 37	syl	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\log A\right)\in ℝ$$
39		pire	$$⊢\mathrm{\pi }\in ℝ$$
40	39	renegcli	$$⊢-\mathrm{\pi }\in ℝ$$
41		ltaddpos2	$$⊢\left(\Im \left(\log A\right)\in ℝ\wedge -\mathrm{\pi }\in ℝ\right)\to \left(0<\Im \left(\log A\right)\leftrightarrow -\mathrm{\pi }<\Im \left(\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(\log A\right)\leftrightarrow -\mathrm{\pi }<\Im \left(\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(\log A\right)+\left(-\mathrm{\pi }\right)$$
44	38	recnd	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\log A\right)\in ℂ$$
45		negsub	$$⊢\left(\Im \left(\log A\right)\in ℂ\wedge \mathrm{\pi }\in ℂ\right)\to \Im \left(\log A\right)+\left(-\mathrm{\pi }\right)=\Im \left(\log A\right)-\mathrm{\pi }$$
46	44 12 45	sylancl	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\log A\right)+\left(-\mathrm{\pi }\right)=\Im \left(\log A\right)-\mathrm{\pi }$$
47	43 46	breqtrd	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to -\mathrm{\pi }<\Im \left(\log A\right)-\mathrm{\pi }$$
48		imsub	$$⊢\left(\log A\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to \Im \left(\log A-\mathrm{i}\mathrm{\pi }\right)=\Im \left(\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(\log A-\mathrm{i}\mathrm{\pi }\right)=\Im \left(\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(\log A\right)-\Im \left(\mathrm{i}\mathrm{\pi }\right)=\Im \left(\log A\right)-\mathrm{\pi }$$
56	49 55	eqtrdi	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\log A-\mathrm{i}\mathrm{\pi }\right)=\Im \left(\log A\right)-\mathrm{\pi }$$
57	47 56	breqtrrd	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to -\mathrm{\pi }<\Im \left(\log A-\mathrm{i}\mathrm{\pi }\right)$$
58		resubcl	$$⊢\left(\Im \left(\log A\right)\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \Im \left(\log A\right)-\mathrm{\pi }\in ℝ$$
59	38 39 58	sylancl	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\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(\log A\right)\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left(0\le \mathrm{\pi }\leftrightarrow \Im \left(\log A\right)-\mathrm{\pi }\le \Im \left(\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 }\leftrightarrow \Im \left(\log A\right)-\mathrm{\pi }\le \Im \left(\log A\right)\right)$$
66	63 65	mpbii	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\log A\right)-\mathrm{\pi }\le \Im \left(\log A\right)$$
67		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)$$
68	8 67	syldan	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$
69	68	simprd	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \Im \left(\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(\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(\log A-\mathrm{i}\mathrm{\pi }\right)\le \mathrm{\pi }$$
72		ellogrn	$$⊢\log A-\mathrm{i}\mathrm{\pi }\in \mathrm{ran}log\leftrightarrow \left(\log A-\mathrm{i}\mathrm{\pi }\in ℂ\wedge -\mathrm{\pi }<\Im \left(\log A-\mathrm{i}\mathrm{\pi }\right)\wedge \Im \left(\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 \log A-\mathrm{i}\mathrm{\pi }\in \mathrm{ran}log$$
74		logef	$$⊢\log A-\mathrm{i}\mathrm{\pi }\in \mathrm{ran}log\to \log {\mathrm{e}}^{\log A-\mathrm{i}\mathrm{\pi }}=\log A-\mathrm{i}\mathrm{\pi }$$
75	73 74	syl	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \log {\mathrm{e}}^{\log A-\mathrm{i}\mathrm{\pi }}=\log A-\mathrm{i}\mathrm{\pi }$$
76	30 75	eqtr3d	$$⊢\left(A\in ℂ\wedge 0<\Im \left(A\right)\right)\to \log \left(-A\right)=\log A-\mathrm{i}\mathrm{\pi }$$