Theorem rxp11d

Description: Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	rxp11d.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	rxp11d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
	rxp11d.3	$$⊢\phi \to C\in ℝ$$
	rxp11d.4	$$⊢\phi \to C\ne 0$$
	rxp11d.5	$$⊢\phi \to A^C=B^C$$
Assertion	rxp11d	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		rxp11d.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		rxp11d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
3		rxp11d.3	$$⊢\phi \to C\in ℝ$$
4		rxp11d.4	$$⊢\phi \to C\ne 0$$
5		rxp11d.5	$$⊢\phi \to A^C=B^C$$
6	1	relogcld	$$⊢\phi \to \log A\in ℝ$$
7	6	recnd	$$⊢\phi \to \log A\in ℂ$$
8	2	relogcld	$$⊢\phi \to \log B\in ℝ$$
9	8	recnd	$$⊢\phi \to \log B\in ℂ$$
10	3	recnd	$$⊢\phi \to C\in ℂ$$
11	5	fveq2d	$$⊢\phi \to \log A^C=\log B^C$$
12	1 3	logcxpd	$$⊢\phi \to \log A^C=C\log A$$
13	2 3	logcxpd	$$⊢\phi \to \log B^C=C\log B$$
14	11 12 13	3eqtr3d	$$⊢\phi \to C\log A=C\log B$$
15	7 9 10 4 14	mulcanad	$$⊢\phi \to \log A=\log B$$
16	1 2	rplog11d	$$⊢\phi \to \left(\log A=\log B\leftrightarrow A=B\right)$$
17	15 16	mpbid	$$⊢\phi \to A=B$$