relogbdivb

Description: The logarithm of the quotient of a positive real number and the base is the logarithm of the number minus 1. (Contributed by AV, 29-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ B \in (ℝ^{+} ∖ \{1\}) \leftrightarrow (B \in ℝ^{+} \land B \neq 1)$
2		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
3	2	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in ℂ$
4		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
5	4	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 0$
6		simpr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 1$
7	3 5 6	3jca	$⊢ (B \in ℝ^{+} \land B \neq 1) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
8	1 7	sylbi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
9		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
10	8 9	sylibr	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \in (ℂ ∖ \{0, 1\})$
11	10	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land A \in ℝ^{+}) \to B \in (ℂ ∖ \{0, 1\})$
12		simpr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land A \in ℝ^{+}) \to A \in ℝ^{+}$
13		eldifi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \in ℝ^{+}$
14	13	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land A \in ℝ^{+}) \to B \in ℝ^{+}$
15		relogbdiv	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land B \in ℝ^{+})) \to \log_{B} (\frac{A}{B}) = \log_{B} A - \log_{B} B$
16	11 12 14 15	syl12anc	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land A \in ℝ^{+}) \to \log_{B} (\frac{A}{B}) = \log_{B} A - \log_{B} B$
17		logbid1	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log_{B} B = 1$
18	8 17	syl	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to \log_{B} B = 1$
19	18	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land A \in ℝ^{+}) \to \log_{B} B = 1$
20	19	oveq2d	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land A \in ℝ^{+}) \to \log_{B} A - \log_{B} B = \log_{B} A - 1$
21	16 20	eqtrd	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land A \in ℝ^{+}) \to \log_{B} (\frac{A}{B}) = \log_{B} A - 1$

Metamath Proof Explorer

Theorem relogbdivb

Proof