logbrec

Description: Logarithm of a reciprocal changes sign. See logrec . Particular case of Property 3 of Cohen4 p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Assertion	logbrec	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log_{B} (\frac{1}{A}) = - \log_{B} A$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to A \in ℝ^{+}$
2	1	rpreccld	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \frac{1}{A} \in ℝ^{+}$
3		relogbval	$⊢ (B \in ℤ_{\geq 2} \land \frac{1}{A} \in ℝ^{+}) \to \log_{B} (\frac{1}{A}) = \frac{\log (\frac{1}{A})}{\log B}$
4	2 3	syldan	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log_{B} (\frac{1}{A}) = \frac{\log (\frac{1}{A})}{\log B}$
5		relogbval	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log_{B} A = \frac{\log A}{\log B}$
6	5	negeqd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to - \log_{B} A = - \frac{\log A}{\log B}$
7	1	rpcnd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to A \in ℂ$
8	1	rpne0d	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to A \neq 0$
9	7 8	logcld	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log A \in ℂ$
10		zgt1rpn0n1	$⊢ B \in ℤ_{\geq 2} \to (B \in ℝ^{+} \land B \neq 0 \land B \neq 1)$
11	10	simp1d	$⊢ B \in ℤ_{\geq 2} \to B \in ℝ^{+}$
12	11	adantr	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to B \in ℝ^{+}$
13	12	relogcld	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log B \in ℝ$
14	13	recnd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log B \in ℂ$
15	10	simp3d	$⊢ B \in ℤ_{\geq 2} \to B \neq 1$
16	15	adantr	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to B \neq 1$
17		logne0	$⊢ (B \in ℝ^{+} \land B \neq 1) \to \log B \neq 0$
18	12 16 17	syl2anc	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log B \neq 0$
19	9 14 18	divnegd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to - \frac{\log A}{\log B} = \frac{- \log A}{\log B}$
20	7 8	reccld	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \frac{1}{A} \in ℂ$
21	7 8	recne0d	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \frac{1}{A} \neq 0$
22	20 21	logcld	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log (\frac{1}{A}) \in ℂ$
23	1	relogcld	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log A \in ℝ$
24	23	reim0d	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to ℑ (\log A) = 0$
25		0re	$⊢ 0 \in ℝ$
26		pipos	$⊢ 0 < π$
27	25 26	gtneii	$⊢ π \neq 0$
28	27	a1i	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to π \neq 0$
29	28	necomd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to 0 \neq π$
30	24 29	eqnetrd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to ℑ (\log A) \neq π$
31		logrec	$⊢ (A \in ℂ \land A \neq 0 \land ℑ (\log A) \neq π) \to \log A = - \log (\frac{1}{A})$
32	7 8 30 31	syl3anc	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log A = - \log (\frac{1}{A})$
33	32	eqcomd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to - \log (\frac{1}{A}) = \log A$
34	22 33	negcon1ad	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to - \log A = \log (\frac{1}{A})$
35	34	oveq1d	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \frac{- \log A}{\log B} = \frac{\log (\frac{1}{A})}{\log B}$
36	6 19 35	3eqtrd	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to - \log_{B} A = \frac{\log (\frac{1}{A})}{\log B}$
37	4 36	eqtr4d	$⊢ (B \in ℤ_{\geq 2} \land A \in ℝ^{+}) \to \log_{B} (\frac{1}{A}) = - \log_{B} A$

Metamath Proof Explorer

Theorem logbrec

Proof