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	$⊢ φ \to C \in ℝ^{+}$
	rxp112d.a	$⊢ φ \to A \in ℝ$
	rxp112d.b	$⊢ φ \to B \in ℝ$
	rxp112d.1	$⊢ φ \to C \neq 1$
	rxp112d.2	$⊢ φ \to C^{A} = C^{B}$
Assertion	rxp112d	$⊢ φ \to A = B$

Proof

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

Metamath Proof Explorer

Theorem rxp112d

Proof