Metamath Proof Explorer

Theorem logbid1

Description: General logarithm is 1 when base and arg match. Property 1(a) of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by David A. Wheeler, 22-Jul-2017)

		Ref	Expression
	Assertion	logbid1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log_{A} A = 1$

Proof

Step	Hyp	Ref	Expression
1		eldifpr	$⊢ A \in (ℂ ∖ \{0, 1\}) \leftrightarrow (A \in ℂ \land A \neq 0 \land A \neq 1)$
2	1	biimpri	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in (ℂ ∖ \{0, 1\})$
3		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
4	3	biimpri	$⊢ (A \in ℂ \land A \neq 0) \to A \in (ℂ ∖ \{0\})$
5	4	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in (ℂ ∖ \{0\})$
6		logbval	$⊢ (A \in (ℂ ∖ \{0, 1\}) \land A \in (ℂ ∖ \{0\})) \to \log_{A} A = \frac{\log A}{\log A}$
7	2 5 6	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log_{A} A = \frac{\log A}{\log A}$
8		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
9	8	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \in ℂ$
10		logccne0	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \neq 0$
11	9 10	dividd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\log A}{\log A} = 1$
12	7 11	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log_{A} A = 1$