Theorem lognegb

Description: If a number has imaginary part equal to _pi , then it is on the negative real axis and vice-versa. (Contributed by Mario Carneiro, 23-Sep-2014)

	Ref	Expression
Assertion	lognegb	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-A\in {ℝ}^{+}\leftrightarrow \Im \left(\log A\right)=\mathrm{\pi }\right)$$

Proof

Step	Hyp	Ref	Expression
1		logneg	$$⊢-A\in {ℝ}^{+}\to \log \left(-\left(-A\right)\right)=\log \left(-A\right)+\mathrm{i}\mathrm{\pi }$$
2	1	fveq2d	$$⊢-A\in {ℝ}^{+}\to \Im \left(\log \left(-\left(-A\right)\right)\right)=\Im \left(\log \left(-A\right)+\mathrm{i}\mathrm{\pi }\right)$$
3		relogcl	$$⊢-A\in {ℝ}^{+}\to \log \left(-A\right)\in ℝ$$
4		pire	$$⊢\mathrm{\pi }\in ℝ$$
5		crim	$$⊢\left(\log \left(-A\right)\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \Im \left(\log \left(-A\right)+\mathrm{i}\mathrm{\pi }\right)=\mathrm{\pi }$$
6	3 4 5	sylancl	$$⊢-A\in {ℝ}^{+}\to \Im \left(\log \left(-A\right)+\mathrm{i}\mathrm{\pi }\right)=\mathrm{\pi }$$
7	2 6	eqtrd	$$⊢-A\in {ℝ}^{+}\to \Im \left(\log \left(-\left(-A\right)\right)\right)=\mathrm{\pi }$$
8		negneg	$$⊢A\in ℂ\to -\left(-A\right)=A$$
9	8	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -\left(-A\right)=A$$
10	9	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log \left(-\left(-A\right)\right)=\log A$$
11	10	fveqeq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\Im \left(\log \left(-\left(-A\right)\right)\right)=\mathrm{\pi }\leftrightarrow \Im \left(\log A\right)=\mathrm{\pi }\right)$$
12	7 11	syl5ib	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-A\in {ℝ}^{+}\to \Im \left(\log A\right)=\mathrm{\pi }\right)$$
13		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
14	13	replimd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A=\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)$$
15	14	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}={\mathrm{e}}^{\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)}$$
16		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
17	13	recld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)\in ℝ$$
18	17	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)\in ℂ$$
19		ax-icn	$$⊢\mathrm{i}\in ℂ$$
20	13	imcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\in ℝ$$
21	20	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\in ℂ$$
22		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(\log A\right)\in ℂ\right)\to \mathrm{i}\Im \left(\log A\right)\in ℂ$$
23	19 21 22	sylancr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \mathrm{i}\Im \left(\log A\right)\in ℂ$$
24		efadd	$$⊢\left(\Re \left(\log A\right)\in ℂ\wedge \mathrm{i}\Im \left(\log A\right)\in ℂ\right)\to {\mathrm{e}}^{\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)}={\mathrm{e}}^{\Re \left(\log A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}$$
25	18 23 24	syl2anc	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)}={\mathrm{e}}^{\Re \left(\log A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}$$
26	15 16 25	3eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A={\mathrm{e}}^{\Re \left(\log A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}$$
27		oveq2	$$⊢\Im \left(\log A\right)=\mathrm{\pi }\to \mathrm{i}\Im \left(\log A\right)=\mathrm{i}\mathrm{\pi }$$
28	27	fveq2d	$$⊢\Im \left(\log A\right)=\mathrm{\pi }\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}={\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}$$
29		efipi	$$⊢{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=-1$$
30	28 29	eqtrdi	$$⊢\Im \left(\log A\right)=\mathrm{\pi }\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=-1$$
31	30	oveq2d	$$⊢\Im \left(\log A\right)=\mathrm{\pi }\to {\mathrm{e}}^{\Re \left(\log A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}={\mathrm{e}}^{\Re \left(\log A\right)}-1$$
32	31	eqeq2d	$$⊢\Im \left(\log A\right)=\mathrm{\pi }\to \left(A={\mathrm{e}}^{\Re \left(\log A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}\leftrightarrow A={\mathrm{e}}^{\Re \left(\log A\right)}-1\right)$$
33	26 32	syl5ibcom	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\Im \left(\log A\right)=\mathrm{\pi }\to A={\mathrm{e}}^{\Re \left(\log A\right)}-1\right)$$
34	17	rpefcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}\in {ℝ}^{+}$$
35	34	rpcnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}\in ℂ$$
36		neg1cn	$$⊢-1\in ℂ$$
37		mulcom	$$⊢\left({\mathrm{e}}^{\Re \left(\log A\right)}\in ℂ\wedge -1\in ℂ\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}-1=-1{\mathrm{e}}^{\Re \left(\log A\right)}$$
38	35 36 37	sylancl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}-1=-1{\mathrm{e}}^{\Re \left(\log A\right)}$$
39	35	mulm1d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -1{\mathrm{e}}^{\Re \left(\log A\right)}=-{\mathrm{e}}^{\Re \left(\log A\right)}$$
40	38 39	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}-1=-{\mathrm{e}}^{\Re \left(\log A\right)}$$
41	40	negeqd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -{\mathrm{e}}^{\Re \left(\log A\right)}-1=-\left(-{\mathrm{e}}^{\Re \left(\log A\right)}\right)$$
42	35	negnegd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -\left(-{\mathrm{e}}^{\Re \left(\log A\right)}\right)={\mathrm{e}}^{\Re \left(\log A\right)}$$
43	41 42	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -{\mathrm{e}}^{\Re \left(\log A\right)}-1={\mathrm{e}}^{\Re \left(\log A\right)}$$
44	43 34	eqeltrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -{\mathrm{e}}^{\Re \left(\log A\right)}-1\in {ℝ}^{+}$$
45		negeq	$$⊢A={\mathrm{e}}^{\Re \left(\log A\right)}-1\to -A=-{\mathrm{e}}^{\Re \left(\log A\right)}-1$$
46	45	eleq1d	$$⊢A={\mathrm{e}}^{\Re \left(\log A\right)}-1\to \left(-A\in {ℝ}^{+}\leftrightarrow -{\mathrm{e}}^{\Re \left(\log A\right)}-1\in {ℝ}^{+}\right)$$
47	44 46	syl5ibrcom	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(A={\mathrm{e}}^{\Re \left(\log A\right)}-1\to -A\in {ℝ}^{+}\right)$$
48	33 47	syld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\Im \left(\log A\right)=\mathrm{\pi }\to -A\in {ℝ}^{+}\right)$$
49	12 48	impbid	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-A\in {ℝ}^{+}\leftrightarrow \Im \left(\log A\right)=\mathrm{\pi }\right)$$