logbchbase

Description: Change of base for logarithms. Property in Cohen4 p. 367. (Contributed by AV, 11-Jun-2020)

		Ref	Expression
	Assertion	logbchbase	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log_{A} X = \frac{\log_{B} X}{\log_{B} A}$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land X \neq 0)$
2		logcl	$⊢ (X \in ℂ \land X \neq 0) \to \log X \in ℂ$
3	1 2	sylbi	$⊢ X \in (ℂ ∖ \{0\}) \to \log X \in ℂ$
4	3	3ad2ant3	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log X \in ℂ$
5		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
6	5	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \in ℂ$
7		logccne0	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \neq 0$
8	6 7	jca	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\log A \in ℂ \land \log A \neq 0)$
9	8	3ad2ant1	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to (\log A \in ℂ \land \log A \neq 0)$
10		logcl	$⊢ (B \in ℂ \land B \neq 0) \to \log B \in ℂ$
11	10	3adant3	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log B \in ℂ$
12		logccne0	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log B \neq 0$
13	11 12	jca	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to (\log B \in ℂ \land \log B \neq 0)$
14	13	3ad2ant2	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to (\log B \in ℂ \land \log B \neq 0)$
15		divcan7	$⊢ (\log X \in ℂ \land (\log A \in ℂ \land \log A \neq 0) \land (\log B \in ℂ \land \log B \neq 0)) \to \frac{\frac{\log X}{\log B}}{\frac{\log A}{\log B}} = \frac{\log X}{\log A}$
16	4 9 14 15	syl3anc	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \frac{\frac{\log X}{\log B}}{\frac{\log A}{\log B}} = \frac{\log X}{\log A}$
17		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
18		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
19	17 18	sylanbr	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
20	19	3adant1	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
21	17	biimpri	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to B \in (ℂ ∖ \{0, 1\})$
22		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
23	22	biimpri	$⊢ (A \in ℂ \land A \neq 0) \to A \in (ℂ ∖ \{0\})$
24	23	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in (ℂ ∖ \{0\})$
25		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land A \in (ℂ ∖ \{0\})) \to \log_{B} A = \frac{\log A}{\log B}$
26	21 24 25	syl2anr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1)) \to \log_{B} A = \frac{\log A}{\log B}$
27	26	3adant3	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log_{B} A = \frac{\log A}{\log B}$
28	20 27	oveq12d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \frac{\log_{B} X}{\log_{B} A} = \frac{\frac{\log X}{\log B}}{\frac{\log A}{\log B}}$
29		eldifpr	$⊢ A \in (ℂ ∖ \{0, 1\}) \leftrightarrow (A \in ℂ \land A \neq 0 \land A \neq 1)$
30		logbval	$⊢ (A \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{A} X = \frac{\log X}{\log A}$
31	29 30	sylanbr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log_{A} X = \frac{\log X}{\log A}$
32	31	3adant2	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log_{A} X = \frac{\log X}{\log A}$
33	16 28 32	3eqtr4rd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \log_{A} X = \frac{\log_{B} X}{\log_{B} A}$

Metamath Proof Explorer

Theorem logbchbase

Proof