relogbcl

Description: Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Assertion	relogbcl	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \log_{B} X \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to B \in ℝ^{+}$
2	1	rpcnne0d	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to (B \in ℂ \land B \neq 0)$
3		simp3	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to B \neq 1$
4		df-3an	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \leftrightarrow ((B \in ℂ \land B \neq 0) \land B \neq 1)$
5	2 3 4	sylanbrc	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
6		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
7	5 6	sylibr	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to B \in (ℂ ∖ \{0, 1\})$
8		simp2	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to X \in ℝ^{+}$
9	8	rpcnne0d	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to (X \in ℂ \land X \neq 0)$
10		eldifsn	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land X \neq 0)$
11	9 10	sylibr	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to X \in (ℂ ∖ \{0\})$
12		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
13	7 11 12	syl2anc	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \log_{B} X = \frac{\log X}{\log B}$
14		relogcl	$⊢ X \in ℝ^{+} \to \log X \in ℝ$
15	14	3ad2ant2	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \log X \in ℝ$
16		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
17	16	3ad2ant1	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \log B \in ℝ$
18		logne0	$⊢ (B \in ℝ^{+} \land B \neq 1) \to \log B \neq 0$
19	18	3adant2	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \log B \neq 0$
20	15 17 19	redivcld	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \frac{\log X}{\log B} \in ℝ$
21	13 20	eqeltrd	$⊢ (B \in ℝ^{+} \land X \in ℝ^{+} \land B \neq 1) \to \log_{B} X \in ℝ$

Metamath Proof Explorer

Theorem relogbcl

Proof