relogbdiv

Description: The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of Cohen4 p. 361. (Contributed by AV, 29-May-2020)

		Ref	Expression
	Assertion	relogbdiv	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} (\frac{A}{C}) = \log_{B} A - \log_{B} C$

Proof

Step	Hyp	Ref	Expression
1		neg1rr	$⊢ - 1 \in ℝ$
2		relogbmulexp	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+} \land - 1 \in ℝ)) \to \log_{B} A C^{- 1} = \log_{B} A + -1 \log_{B} C$
3	1 2	mp3anr3	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} A C^{- 1} = \log_{B} A + -1 \log_{B} C$
4		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
5	4	adantr	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to A \in ℂ$
6		rpcn	$⊢ C \in ℝ^{+} \to C \in ℂ$
7	6	adantl	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to C \in ℂ$
8		rpne0	$⊢ C \in ℝ^{+} \to C \neq 0$
9	8	adantl	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to C \neq 0$
10	5 7 9	divrecd	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to \frac{A}{C} = A (\frac{1}{C})$
11		1cnd	$⊢ C \in ℝ^{+} \to 1 \in ℂ$
12	6 8 11	cxpnegd	$⊢ C \in ℝ^{+} \to C^{- 1} = \frac{1}{C^{1}}$
13	6	cxp1d	$⊢ C \in ℝ^{+} \to C^{1} = C$
14	13	oveq2d	$⊢ C \in ℝ^{+} \to \frac{1}{C^{1}} = \frac{1}{C}$
15	12 14	eqtrd	$⊢ C \in ℝ^{+} \to C^{- 1} = \frac{1}{C}$
16	15	adantl	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to C^{- 1} = \frac{1}{C}$
17	16	oveq2d	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to A C^{- 1} = A (\frac{1}{C})$
18	10 17	eqtr4d	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to \frac{A}{C} = A C^{- 1}$
19	18	adantl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \frac{A}{C} = A C^{- 1}$
20	19	oveq2d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} (\frac{A}{C}) = \log_{B} A C^{- 1}$
21		rpcndif0	$⊢ C \in ℝ^{+} \to C \in (ℂ ∖ \{0\})$
22	21	adantl	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to C \in (ℂ ∖ \{0\})$
23		logbcl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in (ℂ ∖ \{0\})) \to \log_{B} C \in ℂ$
24	22 23	sylan2	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} C \in ℂ$
25		mulm1	$⊢ \log_{B} C \in ℂ \to -1 \log_{B} C = - \log_{B} C$
26	25	oveq2d	$⊢ \log_{B} C \in ℂ \to \log_{B} A + -1 \log_{B} C = \log_{B} A + (- \log_{B} C)$
27	24 26	syl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} A + -1 \log_{B} C = \log_{B} A + (- \log_{B} C)$
28		rpcndif0	$⊢ A \in ℝ^{+} \to A \in (ℂ ∖ \{0\})$
29	28	adantr	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to A \in (ℂ ∖ \{0\})$
30		logbcl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land A \in (ℂ ∖ \{0\})) \to \log_{B} A \in ℂ$
31	29 30	sylan2	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} A \in ℂ$
32	31 24	negsubd	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} A + (- \log_{B} C) = \log_{B} A - \log_{B} C$
33	27 32	eqtr2d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} A - \log_{B} C = \log_{B} A + -1 \log_{B} C$
34	3 20 33	3eqtr4d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} (\frac{A}{C}) = \log_{B} A - \log_{B} C$

Metamath Proof Explorer

Theorem relogbdiv

Proof