Theorem rplog11d

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

	Ref	Expression
Hypotheses	rplog11d.a	$$⊢\phi \to A\in {ℝ}^{+}$$
	rplog11d.b	$$⊢\phi \to B\in {ℝ}^{+}$$
Assertion	rplog11d	$$⊢\phi \to \left(\log A=\log B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rplog11d.a	$$⊢\phi \to A\in {ℝ}^{+}$$
2		rplog11d.b	$$⊢\phi \to B\in {ℝ}^{+}$$
3	1	rpcnd	$$⊢\phi \to A\in ℂ$$
4	2	rpcnd	$$⊢\phi \to B\in ℂ$$
5	1	rpne0d	$$⊢\phi \to A\ne 0$$
6	2	rpne0d	$$⊢\phi \to B\ne 0$$
7	3 4 5 6	log11d	$$⊢\phi \to \left(\log A=\log B\leftrightarrow A=B\right)$$