HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem expordit 6608
Description: Ordering relationship for exponentiation.
Assertion
Ref Expression
expordit |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^M) < (A^N))
Proof of Theorem expordit
StepHypRef Expression
1 expgt1t 6600 . . . 4 |- ((A e. RR /\ (N - M) e. NN /\ 1 < A) -> 1 < (A^(N - M)))
2 3simp1 790 . . . . 5 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> A e. RR)
32adantr 391 . . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> A e. RR)
4 znnsubt 6186 . . . . . . . 8 |- ((M e. ZZ /\ N e. ZZ) -> (M < N <-> (N - M) e. NN))
5 nn0zt 6163 . . . . . . . 8 |- (M e. NN0 -> M e. ZZ)
6 nn0zt 6163 . . . . . . . 8 |- (N e. NN0 -> N e. ZZ)
74, 5, 6syl2an 456 . . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> (M < N <-> (N - M) e. NN))
873adant1 799 . . . . . 6 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (M < N <-> (N - M) e. NN))
98biimpa 418 . . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (N - M) e. NN)
109adantrl 396 . . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (N - M) e. NN)
11 simprl 416 . . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 1 < A)
121, 3, 10, 11syl3anc 860 . . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 1 < (A^(N - M)))
13 ltmul1t 5839 . . . 4 |- (((1 e. RR /\ (A^(N - M)) e. RR /\ (A^M) e. RR) /\ 0 < (A^M)) -> (1 < (A^(N - M)) <-> (1 x. (A^M)) < ((A^(N - M)) x. (A^M))))
14 1re 5454 . . . . . 6 |- 1 e. RR
1514a1i 8 . . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 1 e. RR)
16 reexpclt 6588 . . . . . . 7 |- ((A e. RR /\ (N - M) e. NN0) -> (A^(N - M)) e. RR)
172adantr 391 . . . . . . 7 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> A e. RR)
18 nnnn0t 6115 . . . . . . . 8 |- ((N - M) e. NN -> (N - M) e. NN0)
199, 18syl 10 . . . . . . 7 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (N - M) e. NN0)
2016, 17, 19sylanc 473 . . . . . 6 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (A^(N - M)) e. RR)
2120adantrl 396 . . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^(N - M)) e. RR)
22 reexpclt 6588 . . . . . . 7 |- ((A e. RR /\ M e. NN0) -> (A^M) e. RR)
23223adant3 801 . . . . . 6 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (A^M) e. RR)
2423adantr 391 . . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^M) e. RR)
2515, 21, 243jca 821 . . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 e. RR /\ (A^(N - M)) e. RR /\ (A^M) e. RR))
26 lt01 5699 . . . . . . . . . 10 |- 0 < 1
27 0re 5459 . . . . . . . . . . 11 |- 0 e. RR
28 axlttrn 5523 . . . . . . . . . . 11 |- ((0 e. RR /\ 1 e. RR /\ A e. RR) -> ((0 < 1 /\ 1 < A) -> 0 < A))
2927, 14, 28mp3an12 908 . . . . . . . . . 10 |- (A e. RR -> ((0 < 1 /\ 1 < A) -> 0 < A))
3026, 29mpani 700 . . . . . . . . 9 |- (A e. RR -> (1 < A -> 0 < A))
3130adantr 391 . . . . . . . 8 |- ((A e. RR /\ M e. NN0) -> (1 < A -> 0 < A))
32 expgt0t 6597 . . . . . . . . 9 |- ((A e. RR /\ M e. NN0 /\ 0 < A) -> 0 < (A^M))
33323expia 837 . . . . . . . 8 |- ((A e. RR /\ M e. NN0) -> (0 < A -> 0 < (A^M)))
3431, 33syld 27 . . . . . . 7 |- ((A e. RR /\ M e. NN0) -> (1 < A -> 0 < (A^M)))
35343adant3 801 . . . . . 6 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (1 < A -> 0 < (A^M)))
3635imp 350 . . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ 1 < A) -> 0 < (A^M))
3736adantrr 397 . . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 0 < (A^M))
3813, 25, 37sylanc 473 . . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 < (A^(N - M)) <-> (1 x. (A^M)) < ((A^(N - M)) x. (A^M))))
3912, 38mpbid 195 . 2 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 x. (A^M)) < ((A^(N - M)) x. (A^M)))
40 expclt 6589 . . . . . 6 |- ((A e. CC /\ M e. NN0) -> (A^M) e. CC)
41 recnt 5332 . . . . . 6 |- (A e. RR -> A e. CC)
4240, 41sylan 450 . . . . 5 |- ((A e. RR /\ M e. NN0) -> (A^M) e. CC)
43 mulid2t 5436 . . . . 5 |- ((A^M) e. CC -> (1 x. (A^M)) = (A^M))
4442, 43syl 10 . . . 4 |- ((A e. RR /\ M e. NN0) -> (1 x. (A^M)) = (A^M))
45443adant3 801 . . 3 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (1 x. (A^M)) = (A^M))
4645adantr 391 . 2 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 x. (A^M)) = (A^M))
472recnd 5334 . . . . . . 7 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> A e. CC)
4847adantr 391 . . . . . 6 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> A e. CC)
49 3simp2 791 . . . . . . 7 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> M e. NN0)
5049adantr 391 . . . . . 6 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> M e. NN0)
5148, 9, 503jca 821 . . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (A e. CC /\ (N - M) e. NN /\ M e. NN0))
5251adantrl 396 . . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A e. CC /\ (N - M) e. NN /\ M e. NN0))
53 expaddt 6604 . . . . 5 |- ((A e. CC /\ (N - M) e. NN0 /\ M e. NN0) -> (A^((N - M) + M)) = ((A^(N - M)) x. (A^M)))
5453, 18syl3an2 862 . . . 4 |- ((A e. CC /\ (N - M) e. NN /\ M e. NN0) -> (A^((N - M) + M)) = ((A^(N - M)) x. (A^M)))
5552, 54syl 10 . . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^((N - M) + M)) = ((A^(N - M)) x. (A^M)))
56 npcant 5418 . . . . . . . 8 |- ((N e. CC /\ M e. CC) -> ((N - M) + M) = N)
57 nn0cnt 6118 . . . . . . . 8 |- (N e. NN0 -> N e. CC)
58 nn0cnt 6118 . . . . . . . 8 |- (M e. NN0 -> M e. CC)
5956, 57, 58syl2an 456 . . . . . . 7 |- ((N e. NN0 /\ M e. NN0) -> ((N - M) + M) = N)
6059ancoms 438 . . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((N - M) + M) = N)
61603adant1 799 . . . . 5 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> ((N - M) + M) = N)
6261opreq2d 3983 . . . 4 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (A^((N - M) + M)) = (A^N))
6362adantr 391 . . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^((N - M) + M)) = (A^N))
6455, 63eqtr3d 1512 . 2 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> ((A^(N - M)) x. (A^M)) = (A^N))
6539, 46, 643brtr3d 2650 1 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 <