HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem expnbndt 6585
Description: Exponentiation with a mantissa greater than 1 has no upper bound.
Assertion
Ref Expression
expnbndt |- ((A e. RR /\ B e. RR /\ 1 < B) -> E.k e. NN A < (B^k))
Distinct variable groups:   A,k   B,k
Proof of Theorem expnbndt
StepHypRef Expression
1 opreq2 3954 . . . . 5 |- (k = 1 -> (B^k) = (B^1))
21breq2d 2620 . . . 4 |- (k = 1 -> (A < (B^k) <-> A < (B^1)))
32rcla4ev 1868 . . 3 |- ((1 e. NN /\ A < (B^1)) -> E.k e. NN A < (B^k))
4 1nn 5882 . . . 4 |- 1 e. NN
54a1i 8 . . 3 |- (((A e. RR /\ B e. RR /\ 1 < B) /\ A < 1) -> 1 e. NN)
6 1re 5407 . . . . . . . 8 |- 1 e. RR
7 axlttrn 5476 . . . . . . . 8 |- ((A e. RR /\ 1 e. RR /\ B e. RR) -> ((A < 1 /\ 1 < B) -> A < B))
86, 7mp3an2 901 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A < 1 /\ 1 < B) -> A < B))
98exp4b 379 . . . . . 6 |- (A e. RR -> (B e. RR -> (A < 1 -> (1 < B -> A < B))))
109com34 36 . . . . 5 |- (A e. RR -> (B e. RR -> (1 < B -> (A < 1 -> A < B))))
11103imp1 844 . . . 4 |- (((A e. RR /\ B e. RR /\ 1 < B) /\ A < 1) -> A < B)
12 recnt 5285 . . . . . . 7 |- (B e. RR -> B e. CC)
13 exp1t 6505 . . . . . . 7 |- (B e. CC -> (B^1) = B)
1412, 13syl 10 . . . . . 6 |- (B e. RR -> (B^1) = B)
15143ad2ant2 799 . . . . 5 |- ((A e. RR /\ B e. RR /\ 1 < B) -> (B^1) = B)
1615adantr 389 . . . 4 |- (((A e. RR /\ B e. RR /\ 1 < B) /\ A < 1) -> (B^1) = B)
1711, 16breqtrrd 2631 . . 3 |- (((A e. RR /\ B e. RR /\ 1 < B) /\ A < 1) -> A < (B^1))
183, 5, 17sylanc 471 . 2 |- (((A e. RR /\ B e. RR /\ 1 < B) /\ A < 1) -> E.k e. NN A < (B^k))
19 opreq2 3954 . . . . . . . 8 |- (k = ((|_` ((A - 1) / (B - 1))) + 1) -> (B^k) = (B^((|_` ((A - 1) / (B - 1))) + 1)))
2019breq2d 2620 . . . . . . 7 |- (k = ((|_` ((A - 1) / (B - 1))) + 1) -> (A < (B^k) <-> A < (B^((|_` ((A - 1) / (B - 1))) + 1))))
2120rcla4ev 1868 . . . . . 6 |- ((((|_` ((A - 1) / (B - 1))) + 1) e. NN /\ A < (B^((|_` ((A - 1) / (B - 1))) + 1))) -> E.k e. NN A < (B^k))
22 flge0nn0t 6185 . . . . . . . 8 |- ((((A - 1) / (B - 1)) e. RR /\ 0 <_ ((A - 1) / (B - 1))) -> (|_` ((A - 1) / (B - 1))) e. NN0)
23 redivclt 5756 . . . . . . . . . 10 |- (((A - 1) e. RR /\ (B - 1) e. RR /\ (B - 1) =/= 0) -> ((A - 1) / (B - 1)) e. RR)
24 peano2rem 5414 . . . . . . . . . . 11 |- (A e. RR -> (A - 1) e. RR)
2524adantr 389 . . . . . . . . . 10 |- ((A e. RR /\ (B e. RR /\ 1 < B)) -> (A - 1) e. RR)
26 peano2rem 5414 . . . . . . . . . . . 12 |- (B e. RR -> (B - 1) e. RR)
2726adantr 389 . . . . . . . . . . 11 |- ((B e. RR /\ 1 < B) -> (B - 1) e. RR)
2827adantl 388 . . . . . . . . . 10 |- ((A e. RR /\ (B e. RR /\ 1 < B)) -> (B - 1) e. RR)
29 posdift 5627 . . . . . . . . . . . . . 14 |- ((1 e. RR /\ B e. RR) -> (1 < B <-> 0 < (B - 1)))
306, 29mpan 693 . . . . . . . . . . . . 13 |- (B e. RR -> (1 < B <-> 0 < (B - 1)))
3130biimpa 416 . . . . . . . . . . . 12 |- ((B e. RR /\ 1 < B) -> 0 < (B - 1))
32 gt0ne0t 5592 . . . . . . . . . . . . 13 |- (((B - 1) e. RR /\ 0 < (B - 1)) -> (B - 1) =/= 0)
3332, 26sylan 448 . . . . . . . . . . . 12 |- ((B e. RR /\ 0 < (B - 1)) -> (B - 1) =/= 0)
3431, 33syldan 467 . . . . . . . . . . 11 |- ((B e. RR /\ 1 < B) -> (B - 1) =/= 0)
3534adantl 388 . . . . . . . . . 10 |- ((A e. RR /\ (B e. RR /\ 1 < B)) -> (B - 1) =/= 0)
3623, 25, 28, 35syl3anc 856 . . . . . . . . 9 |- ((A e. RR /\ (B e. RR /\ 1 < B)) -> ((A - 1) / (B - 1)) e. RR)
3736adantll 392 . . . . . . . 8 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> ((A - 1) / (B - 1)) e. RR)
38 divge0t 5810 . . . . . . . . 9 |- ((((A - 1) e. RR /\ 0 <_ (A - 1)) /\ ((B - 1) e. RR /\ 0 < (B - 1))) -> 0 <_ ((A - 1) / (B - 1)))
3924adantl 388 . . . . . . . . . 10 |- ((1 <_ A /\ A e. RR) -> (A - 1) e. RR)
40 subge0t 5647 . . . . . . . . . . . 12 |- ((A e. RR /\ 1 e. RR) -> (0 <_ (A - 1) <-> 1 <_ A))
416, 40mpan2 694 . . . . . . . . . . 11 |- (A e. RR -> (0 <_ (A - 1) <-> 1 <_ A))
4241biimparc 419 . . . . . . . . . 10 |- ((1 <_ A /\ A e. RR) -> 0 <_ (A - 1))
4339, 42jca 288 . . . . . . . . 9 |- ((1 <_ A /\ A e. RR) -> ((A - 1) e. RR /\ 0 <_ (A - 1)))
4427, 31jca 288 . . . . . . . . 9 |- ((B e. RR /\ 1 < B) -> ((B - 1) e. RR /\ 0 < (B - 1)))
4538, 43, 44syl2an 454 . . . . . . . 8 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> 0 <_ ((A - 1) / (B - 1)))
4622, 37, 45sylanc 471 . . . . . . 7 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> (|_` ((A - 1) / (B - 1))) e. NN0)
47 nn0p1nnt 6122 . . . . . . 7 |- ((|_` ((A - 1) / (B - 1))) e. NN0 -> ((|_` ((A - 1) / (B - 1))) + 1) e. NN)
4846, 47syl 10 . . . . . 6 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> ((|_` ((A - 1) / (B - 1))) + 1) e. NN)
49 simplr 413 . . . . . . 7 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> A e. RR)
50 axmulrcl 5246 . . . . . . . . 9 |- (((B - 1) e. RR /\ ((|_` ((A - 1) / (B - 1))) + 1) e. RR) -> ((B - 1) x. ((|_` ((A - 1) / (B - 1))) + 1)) e. RR)
5127adantl 388 . . . . . . . . 9 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> (B - 1) e. RR)
52 peano2nn0 6071 . . . . . . . . . . 11 |- ((|_` ((A - 1) / (B - 1))) e. NN0 -> ((|_` ((A - 1) / (B - 1))) + 1) e. NN0)
5346, 52syl 10 . . . . . . . . . 10 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> ((|_` ((A - 1) / (B - 1))) + 1) e. NN0)
54 nn0ret 6055 . . . . . . . . . 10 |- (((|_` ((A - 1) / (B - 1))) + 1) e. NN0 -> ((|_` ((A - 1) / (B - 1))) + 1) e. RR)
5553, 54syl 10 . . . . . . . . 9 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> ((|_` ((A - 1) / (B - 1))) + 1) e. RR)
5650, 51, 55sylanc 471 . . . . . . . 8 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> ((B - 1) x. ((|_` ((A - 1) / (B - 1))) + 1)) e. RR)
57 peano2re 5408 . . . . . . . 8 |- (((B - 1) x. ((|_` ((A - 1) / (B - 1))) + 1)) e. RR -> (((B - 1) x. ((|_` ((A - 1) / (B - 1))) + 1)) + 1) e. RR)
5856, 57syl 10 . . . . . . 7 |- (((1 <_ A /\ A e. RR) /\ (B e. RR /\ 1 < B)) -> (((B - 1) x. ((|_` ((A - 1) / (B - 1))) + 1)) + 1) e. RR)
59 reexpclt 6512 . . . . . . . 8 |- ((B e. RR /\ ((|_` ((A - 1) / (B - 1))) + 1) e. NN0) -> (B^((|_` ((A - 1) / (B - 1))) + 1)) e. RR)
60 simprl 414 . . . . . . . 8 |- (((1 <_ A /\