log11d

Description: The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	log11d.a	$⊢ φ \to A \in ℂ$
	log11d.b	$⊢ φ \to B \in ℂ$
	log11d.1	$⊢ φ \to A \neq 0$
	log11d.2	$⊢ φ \to B \neq 0$
Assertion	log11d	$⊢ φ \to (\log A = \log B \leftrightarrow A = B)$

Step	Hyp	Ref	Expression
1		log11d.a	$⊢ φ \to A \in ℂ$
2		log11d.b	$⊢ φ \to B \in ℂ$
3		log11d.1	$⊢ φ \to A \neq 0$
4		log11d.2	$⊢ φ \to B \neq 0$
5		fveq2	$⊢ \log A = \log B \to e^{\log A} = e^{\log B}$
6		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
7	1 3 6	syl2anc	$⊢ φ \to e^{\log A} = A$
8		eflog	$⊢ (B \in ℂ \land B \neq 0) \to e^{\log B} = B$
9	2 4 8	syl2anc	$⊢ φ \to e^{\log B} = B$
10	7 9	eqeq12d	$⊢ φ \to (e^{\log A} = e^{\log B} \leftrightarrow A = B)$
11	5 10	imbitrid	$⊢ φ \to (\log A = \log B \to A = B)$
12		fveq2	$⊢ A = B \to \log A = \log B$
13	11 12	impbid1	$⊢ φ \to (\log A = \log B \leftrightarrow A = B)$

Metamath Proof Explorer