This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A ∈ ℝ +
rxp11d.2 ⊢ φ → B ∈ ℝ +
rxp11d.3 ⊢ φ → C ∈ ℝ
rxp11d.4 ⊢ φ → C ≠ 0
rxp11d.5 ⊢ φ → A C = B C
Assertion rxp11d ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 rxp11d.1 ⊢ φ → A ∈ ℝ +
2 rxp11d.2 ⊢ φ → B ∈ ℝ +
3 rxp11d.3 ⊢ φ → C ∈ ℝ
4 rxp11d.4 ⊢ φ → C ≠ 0
5 rxp11d.5 ⊢ φ → A C = B C
6 1 relogcld ⊢ φ → log ⁡ A ∈ ℝ
7 6 recnd ⊢ φ → log ⁡ A ∈ ℂ
8 2 relogcld ⊢ φ → log ⁡ B ∈ ℝ
9 8 recnd ⊢ φ → log ⁡ B ∈ ℂ
10 3 recnd ⊢ φ → C ∈ ℂ
11 5 fveq2d ⊢ φ → log ⁡ A C = log ⁡ B C
12 1 3 logcxpd ⊢ φ → log ⁡ A C = C ⁢ log ⁡ A
13 2 3 logcxpd ⊢ φ → log ⁡ B C = C ⁢ log ⁡ B
14 11 12 13 3eqtr3d ⊢ φ → C ⁢ log ⁡ A = C ⁢ log ⁡ B
15 7 9 10 4 14 mulcanad ⊢ φ → log ⁡ A = log ⁡ B
16 1 2 rplog11d ⊢ φ → log ⁡ A = log ⁡ B ↔ A = B
17 15 16 mpbid ⊢ φ → A = B