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