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	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	rxp11d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	rxp11d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	rxp11d.4	⊢ ( 𝜑 → 𝐶 ≠ 0 )
	rxp11d.5	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝐶 ) = ( 𝐵 ↑𝑐 𝐶 ) )
Assertion	rxp11d	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rxp11d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		rxp11d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3		rxp11d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		rxp11d.4	⊢ ( 𝜑 → 𝐶 ≠ 0 )
5		rxp11d.5	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝐶 ) = ( 𝐵 ↑𝑐 𝐶 ) )
6	1	relogcld	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
7	6	recnd	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
8	2	relogcld	⊢ ( 𝜑 → ( log ‘ 𝐵 ) ∈ ℝ )
9	8	recnd	⊢ ( 𝜑 → ( log ‘ 𝐵 ) ∈ ℂ )
10	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
11	5	fveq2d	⊢ ( 𝜑 → ( log ‘ ( 𝐴 ↑𝑐 𝐶 ) ) = ( log ‘ ( 𝐵 ↑𝑐 𝐶 ) ) )
12	1 3	logcxpd	⊢ ( 𝜑 → ( log ‘ ( 𝐴 ↑𝑐 𝐶 ) ) = ( 𝐶 · ( log ‘ 𝐴 ) ) )
13	2 3	logcxpd	⊢ ( 𝜑 → ( log ‘ ( 𝐵 ↑𝑐 𝐶 ) ) = ( 𝐶 · ( log ‘ 𝐵 ) ) )
14	11 12 13	3eqtr3d	⊢ ( 𝜑 → ( 𝐶 · ( log ‘ 𝐴 ) ) = ( 𝐶 · ( log ‘ 𝐵 ) ) )
15	7 9 10 4 14	mulcanad	⊢ ( 𝜑 → ( log ‘ 𝐴 ) = ( log ‘ 𝐵 ) )
16	1 2	rplog11d	⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) = ( log ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )
17	15 16	mpbid	⊢ ( 𝜑 → 𝐴 = 𝐵 )