HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem expmwordit 6606
Description: Weak mantissa ordering relationship for exponentiation.
Assertion
Ref Expression
expmwordit |- (((A e. RR /\ B e. RR /\ N e. NN0) /\ (0 <_ A /\ A <_ B)) -> (A^N) <_ (B^N))
Proof of Theorem expmwordit
StepHypRef Expression
1 lemul12itOLD 5843 . . . . . . . . . 10 |- (((((A^k) e. RR /\ (B^k) e. RR) /\ (0 <_ (A^k) /\ (A^k) <_ (B^k))) /\ ((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B))) -> ((A^k) x. A) <_ ((B^k) x. B))
2 reexpclt 6580 . . . . . . . . . . . . . . 15 |- ((A e. RR /\ k e. NN0) -> (A^k) e. RR)
32adantlr 393 . . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR) /\ k e. NN0) -> (A^k) e. RR)
43adantlr 393 . . . . . . . . . . . . 13 |- ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) -> (A^k) e. RR)
54adantr 389 . . . . . . . . . . . 12 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> (A^k) e. RR)
6 reexpclt 6580 . . . . . . . . . . . . . . 15 |- ((B e. RR /\ k e. NN0) -> (B^k) e. RR)
76adantll 392 . . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR) /\ k e. NN0) -> (B^k) e. RR)
87adantlr 393 . . . . . . . . . . . . 13 |- ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) -> (B^k) e. RR)
98adantr 389 . . . . . . . . . . . 12 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> (B^k) e. RR)
105, 9jca 288 . . . . . . . . . . 11 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> ((A^k) e. RR /\ (B^k) e. RR))
11 expge0t 6591 . . . . . . . . . . . . . . . 16 |- ((A e. RR /\ k e. NN0 /\ 0 <_ A) -> 0 <_ (A^k))
12113expa 833 . . . . . . . . . . . . . . 15 |- (((A e. RR /\ k e. NN0) /\ 0 <_ A) -> 0 <_ (A^k))
1312an1rs 489 . . . . . . . . . . . . . 14 |- (((A e. RR /\ 0 <_ A) /\ k e. NN0) -> 0 <_ (A^k))
1413adantllr 397 . . . . . . . . . . . . 13 |- ((((A e. RR /\ B e. RR) /\ 0 <_ A) /\ k e. NN0) -> 0 <_ (A^k))
1514adantlrr 399 . . . . . . . . . . . 12 |- ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) -> 0 <_ (A^k))
1615anim1i 334 . . . . . . . . . . 11 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> (0 <_ (A^k) /\ (A^k) <_ (B^k)))
1710, 16jca 288 . . . . . . . . . 10 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> (((A^k) e. RR /\ (B^k) e. RR) /\ (0 <_ (A^k) /\ (A^k) <_ (B^k))))
18 simpll 412 . . . . . . . . . 10 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> ((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)))
191, 17, 18sylanc 471 . . . . . . . . 9 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> ((A^k) x. A) <_ ((B^k) x. B))
20 expp1t 6574 . . . . . . . . . . . . 13 |- ((A e. CC /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
21 recnt 5313 . . . . . . . . . . . . 13 |- (A e. RR -> A e. CC)
2220, 21sylan 448 . . . . . . . . . . . 12 |- ((A e. RR /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
2322adantlr 393 . . . . . . . . . . 11 |- (((A e. RR /\ B e. RR) /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
2423adantlr 393 . . . . . . . . . 10 |- ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
2524adantr 389 . . . . . . . . 9 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> (A^(k + 1)) = ((A^k) x. A))
26 expp1t 6574 . . . . . . . . . . . . 13 |- ((B e. CC /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
27 recnt 5313 . . . . . . . . . . . . 13 |- (B e. RR -> B e. CC)
2826, 27sylan 448 . . . . . . . . . . . 12 |- ((B e. RR /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
2928adantll 392 . . . . . . . . . . 11 |- (((A e. RR /\ B e. RR) /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
3029adantlr 393 . . . . . . . . . 10 |- ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
3130adantr 389 . . . . . . . . 9 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> (B^(k + 1)) = ((B^k) x. B))
3219, 25, 313brtr4d 2645 . . . . . . . 8 |- (((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) /\ (A^k) <_ (B^k)) -> (A^(k + 1)) <_ (B^(k + 1)))
3332ex 373 . . . . . . 7 |- ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) /\ k e. NN0) -> ((A^k) <_ (B^k) -> (A^(k + 1)) <_ (B^(k + 1))))
3433expcom 374 . . . . . 6 |- (k e. NN0 -> (((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) -> ((A^k) <_ (B^k) -> (A^(k + 1)) <_ (B^(k + 1)))))
3534a2d 13 . . . . 5 |- (k e. NN0 -> ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) -> (A^k) <_ (B^k)) -> (((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) -> (A^(k + 1)) <_ (B^(k + 1)))))
36 exp0t 6571 . . . . . . . . . 10 |- (A e. CC -> (A^0) = 1)
3736adantr 389 . . . . . . . . 9 |- ((A e. CC /\ B e. CC) -> (A^0) = 1)
38 1re 5435 . . . . . . . . . 10 |- 1 e. RR
3938leid 5610 . . . . . . . . 9 |- 1 <_ 1
4037, 39syl6eqbr 2652 . . . . . . . 8 |- ((A e. CC /\ B e. CC) -> (A^0) <_ 1)
41 exp0t 6571 . . . . . . . . 9 |- (B e. CC -> (B^0) = 1)
4241adantl 388 . . . . . . . 8 |- ((A e. CC /\ B e. CC) -> (B^0) = 1)
4340, 42breqtrrd 2641 . . . . . . 7 |- ((A e. CC /\ B e. CC) -> (A^0) <_ (B^0))
4443, 21, 27syl2an 454 . . . . . 6 |- ((A e. RR /\ B e. RR) -> (A^0) <_ (B^0))
4544adantr 389 . . . . 5 |- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) -> (A^0) <_ (B^0))
46 opreq2 3969 . . . . . . 7 |- (j = 0 -> (A^j) = (A^0))
47 opreq2 3969 . . . . . . 7 |- (j = 0 -> (B^j) = (B^0))
4846, 47breq12d 2631 . . . . . 6 |- (j = 0 -> ((A^j) <_ (B^j) <-> (A^0) <_ (B^0)))
4948imbi2d 612 . . . . 5 |- (j = 0 -> ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) -> (A^j) <_ (B^j)) <-> (((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B)) -> (A^0) <_ (B^0))))
50 opreq2 3969 . . . . . . 7 |- (j = k -> (A^j) = (A^k))
51 opreq2 3969 . . . . . . 7 |- (j = k -> (B^j) = (B^k))
5250, 51breq12d 2631 . . . . . 6 |- (j = k -> ((A^j) <_ (B^j) <-> (A^k) <_ (B^k)))
5352imbi2d 612 . . . . 5 |- (j = k -> ((((A e. RR /\ B e. RR) /\ (0 <_ A /\ A <_ B