logrec

Description: Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016)

		Ref	Expression
	Assertion	logrec	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \log A = - \log (\frac{1}{A})$

Proof

Step	Hyp	Ref	Expression
1		reccl	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \in ℂ$
2		recne0	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \neq 0$
3		eflog	$⊢ (\frac{1}{A} \in ℂ \land \frac{1}{A} \neq 0) \to e^{\log (\frac{1}{A})} = \frac{1}{A}$
4	1 2 3	syl2anc	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log (\frac{1}{A})} = \frac{1}{A}$
5	4	eqcomd	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} = e^{\log (\frac{1}{A})}$
6	5	oveq2d	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{\frac{1}{A}} = \frac{1}{e^{\log (\frac{1}{A})}}$
7		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
8		recrec	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{\frac{1}{A}} = A$
9	7 8	eqtr4d	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = \frac{1}{\frac{1}{A}}$
10	1 2	logcld	$⊢ (A \in ℂ \land A \neq 0) \to \log (\frac{1}{A}) \in ℂ$
11		efneg	$⊢ \log (\frac{1}{A}) \in ℂ \to e^{- \log (\frac{1}{A})} = \frac{1}{e^{\log (\frac{1}{A})}}$
12	10 11	syl	$⊢ (A \in ℂ \land A \neq 0) \to e^{- \log (\frac{1}{A})} = \frac{1}{e^{\log (\frac{1}{A})}}$
13	6 9 12	3eqtr4d	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = e^{- \log (\frac{1}{A})}$
14	13	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to e^{\log A} = e^{- \log (\frac{1}{A})}$
15	14	fveq2d	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \log e^{\log A} = \log e^{- \log (\frac{1}{A})}$
16		logrncl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ran log$
17	16	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \log A \in ran log$
18		logef	$⊢ \log A \in ran log \to \log e^{\log A} = \log A$
19	17 18	syl	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \log e^{\log A} = \log A$
20		df-ne	$⊢ ℑ (\log A) \neq π \leftrightarrow \neg ℑ (\log A) = π$
21		lognegb	$⊢ (\frac{1}{A} \in ℂ \land \frac{1}{A} \neq 0) \to (- \frac{1}{A} \in ℝ^{+} \leftrightarrow ℑ (\log (\frac{1}{A})) = π)$
22	1 2 21	syl2anc	$⊢ (A \in ℂ \land A \neq 0) \to (- \frac{1}{A} \in ℝ^{+} \leftrightarrow ℑ (\log (\frac{1}{A})) = π)$
23	22	biimprd	$⊢ (A \in ℂ \land A \neq 0) \to (ℑ (\log (\frac{1}{A})) = π \to - \frac{1}{A} \in ℝ^{+})$
24		ax-1cn	$⊢ 1 \in ℂ$
25		divneg2	$⊢ (1 \in ℂ \land A \in ℂ \land A \neq 0) \to - \frac{1}{A} = \frac{1}{- A}$
26	24 25	mp3an1	$⊢ (A \in ℂ \land A \neq 0) \to - \frac{1}{A} = \frac{1}{- A}$
27	26	eleq1d	$⊢ (A \in ℂ \land A \neq 0) \to (- \frac{1}{A} \in ℝ^{+} \leftrightarrow \frac{1}{- A} \in ℝ^{+})$
28	23 27	sylibd	$⊢ (A \in ℂ \land A \neq 0) \to (ℑ (\log (\frac{1}{A})) = π \to \frac{1}{- A} \in ℝ^{+})$
29		negcl	$⊢ A \in ℂ \to - A \in ℂ$
30		negeq0	$⊢ A \in ℂ \to (A = 0 \leftrightarrow - A = 0)$
31	30	necon3bid	$⊢ A \in ℂ \to (A \neq 0 \leftrightarrow - A \neq 0)$
32	31	biimpa	$⊢ (A \in ℂ \land A \neq 0) \to - A \neq 0$
33		rpreccl	$⊢ \frac{1}{- A} \in ℝ^{+} \to \frac{1}{\frac{1}{- A}} \in ℝ^{+}$
34		recrec	$⊢ (- A \in ℂ \land - A \neq 0) \to \frac{1}{\frac{1}{- A}} = - A$
35	34	eleq1d	$⊢ (- A \in ℂ \land - A \neq 0) \to (\frac{1}{\frac{1}{- A}} \in ℝ^{+} \leftrightarrow - A \in ℝ^{+})$
36	33 35	syl5ib	$⊢ (- A \in ℂ \land - A \neq 0) \to (\frac{1}{- A} \in ℝ^{+} \to - A \in ℝ^{+})$
37	29 32 36	syl2an2r	$⊢ (A \in ℂ \land A \neq 0) \to (\frac{1}{- A} \in ℝ^{+} \to - A \in ℝ^{+})$
38	28 37	syld	$⊢ (A \in ℂ \land A \neq 0) \to (ℑ (\log (\frac{1}{A})) = π \to - A \in ℝ^{+})$
39		lognegb	$⊢ (A \in ℂ \land A \neq 0) \to (- A \in ℝ^{+} \leftrightarrow ℑ (\log A) = π)$
40	38 39	sylibd	$⊢ (A \in ℂ \land A \neq 0) \to (ℑ (\log (\frac{1}{A})) = π \to ℑ (\log A) = π)$
41	40	con3d	$⊢ (A \in ℂ \land A \neq 0) \to (\neg ℑ (\log A) = π \to \neg ℑ (\log (\frac{1}{A})) = π)$
42	41	3impia	$⊢ (A \in ℂ \land A \neq 0 \land \neg ℑ (\log A) = π) \to \neg ℑ (\log (\frac{1}{A})) = π$
43	20 42	syl3an3b	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \neg ℑ (\log (\frac{1}{A})) = π$
44		logrncl	$⊢ (\frac{1}{A} \in ℂ \land \frac{1}{A} \neq 0) \to \log (\frac{1}{A}) \in ran log$
45	1 2 44	syl2anc	$⊢ (A \in ℂ \land A \neq 0) \to \log (\frac{1}{A}) \in ran log$
46		logreclem	$⊢ (\log (\frac{1}{A}) \in ran log \land \neg ℑ (\log (\frac{1}{A})) = π) \to - \log (\frac{1}{A}) \in ran log$
47	45 46	stoic3	$⊢ (A \in ℂ \land A \neq 0 \land \neg ℑ (\log (\frac{1}{A})) = π) \to - \log (\frac{1}{A}) \in ran log$
48	43 47	syld3an3	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to - \log (\frac{1}{A}) \in ran log$
49		logef	$⊢ - \log (\frac{1}{A}) \in ran log \to \log e^{- \log (\frac{1}{A})} = - \log (\frac{1}{A})$
50	48 49	syl	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \log e^{- \log (\frac{1}{A})} = - \log (\frac{1}{A})$
51	15 19 50	3eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \log A = - \log (\frac{1}{A})$

Metamath Proof Explorer

Theorem logrec

Proof