Metamath Proof Explorer


Theorem exp11nnd

Description: sq11d for positive real bases and positive integer exponents. The base cannot be generalized much further, since if N is even then we have A ^ N = -u A ^ N . (Contributed by SN, 14-Sep-2023)

Ref Expression
Hypotheses exp11nnd.1 φ A +
exp11nnd.2 φ B +
exp11nnd.3 φ N
exp11nnd.4 φ A N = B N
Assertion exp11nnd φ A = B

Proof

Step Hyp Ref Expression
1 exp11nnd.1 φ A +
2 exp11nnd.2 φ B +
3 exp11nnd.3 φ N
4 exp11nnd.4 φ A N = B N
5 1 rpred φ A
6 3 nnnn0d φ N 0
7 5 6 reexpcld φ A N
8 2 rpred φ B
9 8 6 reexpcld φ B N
10 7 9 lttri3d φ A N = B N ¬ A N < B N ¬ B N < A N
11 4 10 mpbid φ ¬ A N < B N ¬ B N < A N
12 1 2 3 ltexp1d φ A < B A N < B N
13 12 notbid φ ¬ A < B ¬ A N < B N
14 2 1 3 ltexp1d φ B < A B N < A N
15 14 notbid φ ¬ B < A ¬ B N < A N
16 13 15 anbi12d φ ¬ A < B ¬ B < A ¬ A N < B N ¬ B N < A N
17 11 16 mpbird φ ¬ A < B ¬ B < A
18 5 8 lttri3d φ A = B ¬ A < B ¬ B < A
19 17 18 mpbird φ A = B