Metamath Proof Explorer


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 φ C +
rxp112d.a φ A
rxp112d.b φ B
rxp112d.1 φ C 1
rxp112d.2 φ C A = C B
Assertion rxp112d φ A = B

Proof

Step Hyp Ref Expression
1 rxp112d.c φ C +
2 rxp112d.a φ A
3 rxp112d.b φ B
4 rxp112d.1 φ C 1
5 rxp112d.2 φ C A = C B
6 2 recnd φ A
7 3 recnd φ B
8 1 relogcld φ log C
9 8 recnd φ log C
10 1 4 logne0d φ log C 0
11 5 fveq2d φ log C A = log C B
12 1 2 logcxpd φ log C A = A log C
13 1 3 logcxpd φ log C B = B log C
14 11 12 13 3eqtr3d φ A log C = B log C
15 6 7 9 10 14 mulcan2ad φ A = B