logbfval

Description: The general logarithm of a complex number to a fixed base. (Contributed by AV, 11-Jun-2020)

		Ref	Expression
	Assertion	logbfval	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to curry logb (B) (X) = \log_{B} X$

Step	Hyp	Ref	Expression
1		df-logb	$⊢ logb = (x \in (ℂ ∖ \{0, 1\}), y \in (ℂ ∖ \{0\}) ⟼ \frac{\log y}{\log x})$
2		ovexd	$⊢ (((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \land (x \in (ℂ ∖ \{0, 1\}) \land y \in (ℂ ∖ \{0\}))) \to \frac{\log y}{\log x} \in V$
3	2	ralrimivva	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to \forall x \in (ℂ ∖ \{0, 1\}) \forall y \in (ℂ ∖ \{0\}) \frac{\log y}{\log x} \in V$
4		cnex	$⊢ ℂ \in V$
5		difexg	$⊢ ℂ \in V \to ℂ ∖ \{0\} \in V$
6	4 5	mp1i	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to ℂ ∖ \{0\} \in V$
7		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
8	7	biimpri	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to B \in (ℂ ∖ \{0, 1\})$
9	8	adantr	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to B \in (ℂ ∖ \{0, 1\})$
10		simpr	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to X \in (ℂ ∖ \{0\})$
11	1 3 6 9 10	fvmpocurryd	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land X \in (ℂ ∖ \{0\})) \to curry logb (B) (X) = \log_{B} X$

Metamath Proof Explorer