logbf

Description: The general logarithm to a fixed base regarded as function. (Contributed by AV, 11-Jun-2020)

		Ref	Expression
	Assertion	logbf	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to curry logb (B) : ℂ ∖ \{0\} ⟶ ℂ$

Step	Hyp	Ref	Expression
1		logbmpt	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to curry logb (B) = (y \in (ℂ ∖ \{0\}) ⟼ \frac{\log y}{\log B})$
2		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
3		logcl	$⊢ (y \in ℂ \land y \neq 0) \to \log y \in ℂ$
4	2 3	sylbi	$⊢ y \in (ℂ ∖ \{0\}) \to \log y \in ℂ$
5	4	adantl	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land y \in (ℂ ∖ \{0\})) \to \log y \in ℂ$
6		logcl	$⊢ (B \in ℂ \land B \neq 0) \to \log B \in ℂ$
7	6	3adant3	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log B \in ℂ$
8	7	adantr	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land y \in (ℂ ∖ \{0\})) \to \log B \in ℂ$
9		logccne0	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log B \neq 0$
10	9	adantr	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land y \in (ℂ ∖ \{0\})) \to \log B \neq 0$
11	5 8 10	divcld	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land y \in (ℂ ∖ \{0\})) \to \frac{\log y}{\log B} \in ℂ$
12	1 11	fmpt3d	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to curry logb (B) : ℂ ∖ \{0\} ⟶ ℂ$

Metamath Proof Explorer