logbcl

Description: General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017)

		Ref	Expression
	Assertion	logbcl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X \in ℂ$

Step	Hyp	Ref	Expression
1		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
2		eldifsn	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land X \neq 0)$
3		logcl	$⊢ (X \in ℂ \land X \neq 0) \to \log X \in ℂ$
4	2 3	sylbi	$⊢ X \in (ℂ ∖ \{0\}) \to \log X \in ℂ$
5	4	adantl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log X \in ℂ$
6		eldifi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to B \in ℂ$
7		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
8	7	simp2bi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to B \neq 0$
9	6 8	logcld	$⊢ B \in (ℂ ∖ \{0, 1\}) \to \log B \in ℂ$
10	9	adantr	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log B \in ℂ$
11		logccne0	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log B \neq 0$
12	7 11	sylbi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to \log B \neq 0$
13	12	adantr	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log B \neq 0$
14	5 10 13	divcld	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \frac{\log X}{\log B} \in ℂ$
15	1 14	eqeltrd	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X \in ℂ$

Metamath Proof Explorer