Theorem logneg

Description: The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014) (Revised by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	logneg	$$⊢A\in {ℝ}^{+}\to \log \left(-A\right)=\log A+\mathrm{i}\mathrm{\pi }$$

Proof

Step	Hyp	Ref	Expression
1		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
2	1	recnd	$$⊢A\in {ℝ}^{+}\to \log A\in ℂ$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4		picn	$$⊢\mathrm{\pi }\in ℂ$$
5	3 4	mulcli	$$⊢\mathrm{i}\mathrm{\pi }\in ℂ$$
6		efadd	$$⊢\left(\log A\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to {\mathrm{e}}^{\log A+\mathrm{i}\mathrm{\pi }}={\mathrm{e}}^{\log A}{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}$$
7	2 5 6	sylancl	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log A+\mathrm{i}\mathrm{\pi }}={\mathrm{e}}^{\log A}{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}$$
8		efipi	$$⊢{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=-1$$
9	8	oveq2i	$$⊢{\mathrm{e}}^{\log A}{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}={\mathrm{e}}^{\log A}-1$$
10		reeflog	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log A}=A$$
11	10	oveq1d	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log A}-1=A-1$$
12	9 11	syl5eq	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log A}{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=A-1$$
13		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
14		neg1cn	$$⊢-1\in ℂ$$
15		mulcom	$$⊢\left(A\in ℂ\wedge -1\in ℂ\right)\to A-1=-1A$$
16	13 14 15	sylancl	$$⊢A\in {ℝ}^{+}\to A-1=-1A$$
17	13	mulm1d	$$⊢A\in {ℝ}^{+}\to -1A=-A$$
18	16 17	eqtrd	$$⊢A\in {ℝ}^{+}\to A-1=-A$$
19	7 12 18	3eqtrd	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log A+\mathrm{i}\mathrm{\pi }}=-A$$
20	19	fveq2d	$$⊢A\in {ℝ}^{+}\to \log {\mathrm{e}}^{\log A+\mathrm{i}\mathrm{\pi }}=\log \left(-A\right)$$
21		addcl	$$⊢\left(\log A\in ℂ\wedge \mathrm{i}\mathrm{\pi }\in ℂ\right)\to \log A+\mathrm{i}\mathrm{\pi }\in ℂ$$
22	2 5 21	sylancl	$$⊢A\in {ℝ}^{+}\to \log A+\mathrm{i}\mathrm{\pi }\in ℂ$$
23		pipos	$$⊢0<\mathrm{\pi }$$
24		pire	$$⊢\mathrm{\pi }\in ℝ$$
25		lt0neg2	$$⊢\mathrm{\pi }\in ℝ\to \left(0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0\right)$$
26	24 25	ax-mp	$$⊢0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0$$
27	23 26	mpbi	$$⊢-\mathrm{\pi }<0$$
28	24	renegcli	$$⊢-\mathrm{\pi }\in ℝ$$
29		0re	$$⊢0\in ℝ$$
30	28 29 24	lttri	$$⊢\left(-\mathrm{\pi }<0\wedge 0<\mathrm{\pi }\right)\to -\mathrm{\pi }<\mathrm{\pi }$$
31	27 23 30	mp2an	$$⊢-\mathrm{\pi }<\mathrm{\pi }$$
32		crim	$$⊢\left(\log A\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \Im \left(\log A+\mathrm{i}\mathrm{\pi }\right)=\mathrm{\pi }$$
33	1 24 32	sylancl	$$⊢A\in {ℝ}^{+}\to \Im \left(\log A+\mathrm{i}\mathrm{\pi }\right)=\mathrm{\pi }$$
34	31 33	breqtrrid	$$⊢A\in {ℝ}^{+}\to -\mathrm{\pi }<\Im \left(\log A+\mathrm{i}\mathrm{\pi }\right)$$
35	24	leidi	$$⊢\mathrm{\pi }\le \mathrm{\pi }$$
36	33 35	eqbrtrdi	$$⊢A\in {ℝ}^{+}\to \Im \left(\log A+\mathrm{i}\mathrm{\pi }\right)\le \mathrm{\pi }$$
37		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)$$
38	22 34 36 37	syl3anbrc	$$⊢A\in {ℝ}^{+}\to \log A+\mathrm{i}\mathrm{\pi }\in \mathrm{ran}log$$
39		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 }$$
40	38 39	syl	$$⊢A\in {ℝ}^{+}\to \log {\mathrm{e}}^{\log A+\mathrm{i}\mathrm{\pi }}=\log A+\mathrm{i}\mathrm{\pi }$$
41	20 40	eqtr3d	$$⊢A\in {ℝ}^{+}\to \log \left(-A\right)=\log A+\mathrm{i}\mathrm{\pi }$$