logblog

Description: The general logarithm to the base being Euler's constant regarded as function is the natural logarithm. (Contributed by AV, 12-Jun-2020)

		Ref	Expression
	Assertion	logblog	$⊢ curry logb (e) = log$

Proof

Step	Hyp	Ref	Expression
1		loge	$⊢ \log e = 1$
2	1	a1i	$⊢ y \in (ℂ ∖ \{0\}) \to \log e = 1$
3	2	oveq2d	$⊢ y \in (ℂ ∖ \{0\}) \to \frac{\log y}{\log e} = \frac{\log y}{1}$
4		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
5		logcl	$⊢ (y \in ℂ \land y \neq 0) \to \log y \in ℂ$
6	4 5	sylbi	$⊢ y \in (ℂ ∖ \{0\}) \to \log y \in ℂ$
7	6	div1d	$⊢ y \in (ℂ ∖ \{0\}) \to \frac{\log y}{1} = \log y$
8	3 7	eqtrd	$⊢ y \in (ℂ ∖ \{0\}) \to \frac{\log y}{\log e} = \log y$
9	8	mpteq2ia	$⊢ (y \in (ℂ ∖ \{0\}) ⟼ \frac{\log y}{\log e}) = (y \in (ℂ ∖ \{0\}) ⟼ \log y)$
10		ere	$⊢ e \in ℝ$
11	10	recni	$⊢ e \in ℂ$
12		ene0	$⊢ e \neq 0$
13		ene1	$⊢ e \neq 1$
14		logbmpt	$⊢ (e \in ℂ \land e \neq 0 \land e \neq 1) \to curry logb (e) = (y \in (ℂ ∖ \{0\}) ⟼ \frac{\log y}{\log e})$
15	11 12 13 14	mp3an	$⊢ curry logb (e) = (y \in (ℂ ∖ \{0\}) ⟼ \frac{\log y}{\log e})$
16		logf1o	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log$
17		f1ofn	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log \to log Fn (ℂ ∖ \{0\})$
18	16 17	ax-mp	$⊢ log Fn (ℂ ∖ \{0\})$
19		dffn5	$⊢ log Fn (ℂ ∖ \{0\}) \leftrightarrow log = (y \in (ℂ ∖ \{0\}) ⟼ \log y)$
20	18 19	mpbi	$⊢ log = (y \in (ℂ ∖ \{0\}) ⟼ \log y)$
21	9 15 20	3eqtr4i	$⊢ curry logb (e) = log$

Metamath Proof Explorer

Theorem logblog

Proof