Theorem log11d

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

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

Proof

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