Theorem rxp112d

Description: Real exponentiation is one-to-one with respect to the second argument. (TODO: Note that the base C must be positive since -u C ^ A is C ^ A x.e ^ i _pi A , so in the negative case A = B + 2 k ). (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	rxp112d.c	$$⊢\phi \to C\in {ℝ}^{+}$$
	rxp112d.a	$$⊢\phi \to A\in ℝ$$
	rxp112d.b	$$⊢\phi \to B\in ℝ$$
	rxp112d.1	$$⊢\phi \to C\ne 1$$
	rxp112d.2	$$⊢\phi \to C^A=C^B$$
Assertion	rxp112d	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		rxp112d.c	$$⊢\phi \to C\in {ℝ}^{+}$$
2		rxp112d.a	$$⊢\phi \to A\in ℝ$$
3		rxp112d.b	$$⊢\phi \to B\in ℝ$$
4		rxp112d.1	$$⊢\phi \to C\ne 1$$
5		rxp112d.2	$$⊢\phi \to C^A=C^B$$
6	2	recnd	$$⊢\phi \to A\in ℂ$$
7	3	recnd	$$⊢\phi \to B\in ℂ$$
8	1	relogcld	$$⊢\phi \to \log C\in ℝ$$
9	8	recnd	$$⊢\phi \to \log C\in ℂ$$
10	1 4	logne0d	$$⊢\phi \to \log C\ne 0$$
11	5	fveq2d	$$⊢\phi \to \log C^A=\log C^B$$
12	1 2	logcxpd	$$⊢\phi \to \log C^A=A\log C$$
13	1 3	logcxpd	$$⊢\phi \to \log C^B=B\log C$$
14	11 12 13	3eqtr3d	$$⊢\phi \to A\log C=B\log C$$
15	6 7 9 10 14	mulcan2ad	$$⊢\phi \to A=B$$