Metamath Proof Explorer

Theorem expnbnd

Description: Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007)

Ref Expression
Assertion expnbnd 
|- ( ( A e. RR /\ B e. RR /\ 1 < B ) -> E. k e. NN A < ( B ^ k ) )

Proof

Step Hyp Ref Expression
1 1nn 
 |-  1 e. NN
2 1re 
 |-  1 e. RR
3 lttr 
 |-  ( ( A e. RR /\ 1 e. RR /\ B e. RR ) -> ( ( A < 1 /\ 1 < B ) -> A < B ) )
4 2 3 mp3an2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A < 1 /\ 1 < B ) -> A < B ) )
5 4 exp4b 
 |-  ( A e. RR -> ( B e. RR -> ( A < 1 -> ( 1 < B -> A < B ) ) ) )
6 5 com34 
 |-  ( A e. RR -> ( B e. RR -> ( 1 < B -> ( A < 1 -> A < B ) ) ) )
7 6 3imp1 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ A < 1 ) -> A < B )
8 recn 
 |-  ( B e. RR -> B e. CC )
9 exp1 
 |-  ( B e. CC -> ( B ^ 1 ) = B )
10 8 9 syl 
 |-  ( B e. RR -> ( B ^ 1 ) = B )
11 10 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( B ^ 1 ) = B )
12 11 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ A < 1 ) -> ( B ^ 1 ) = B )
13 7 12 breqtrrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ A < 1 ) -> A < ( B ^ 1 ) )
14 oveq2 
 |-  ( k = 1 -> ( B ^ k ) = ( B ^ 1 ) )
15 14 breq2d 
 |-  ( k = 1 -> ( A < ( B ^ k ) <-> A < ( B ^ 1 ) ) )
16 15 rspcev 
 |-  ( ( 1 e. NN /\ A < ( B ^ 1 ) ) -> E. k e. NN A < ( B ^ k ) )
17 1 13 16 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ A < 1 ) -> E. k e. NN A < ( B ^ k ) )
18 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
19 18 adantr 
 |-  ( ( A e. RR /\ ( B e. RR /\ 1 < B ) ) -> ( A - 1 ) e. RR )
20 peano2rem 
 |-  ( B e. RR -> ( B - 1 ) e. RR )
21 20 adantr 
 |-  ( ( B e. RR /\ 1 < B ) -> ( B - 1 ) e. RR )
22 21 adantl 
 |-  ( ( A e. RR /\ ( B e. RR /\ 1 < B ) ) -> ( B - 1 ) e. RR )
23 posdif 
 |-  ( ( 1 e. RR /\ B e. RR ) -> ( 1 < B <-> 0 < ( B - 1 ) ) )
24 2 23 mpan 
 |-  ( B e. RR -> ( 1 < B <-> 0 < ( B - 1 ) ) )
25 24 biimpa 
 |-  ( ( B e. RR /\ 1 < B ) -> 0 < ( B - 1 ) )
26 25 gt0ne0d 
 |-  ( ( B e. RR /\ 1 < B ) -> ( B - 1 ) =/= 0 )
27 26 adantl 
 |-  ( ( A e. RR /\ ( B e. RR /\ 1 < B ) ) -> ( B - 1 ) =/= 0 )
28 19 22 27 redivcld 
 |-  ( ( A e. RR /\ ( B e. RR /\ 1 < B ) ) -> ( ( A - 1 ) / ( B - 1 ) ) e. RR )
29 28 adantll 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( A - 1 ) / ( B - 1 ) ) e. RR )
30 18 adantl 
 |-  ( ( 1 <_ A /\ A e. RR ) -> ( A - 1 ) e. RR )
31 subge0 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( 0 <_ ( A - 1 ) <-> 1 <_ A ) )
32 2 31 mpan2 
 |-  ( A e. RR -> ( 0 <_ ( A - 1 ) <-> 1 <_ A ) )
33 32 biimparc 
 |-  ( ( 1 <_ A /\ A e. RR ) -> 0 <_ ( A - 1 ) )
34 30 33 jca 
 |-  ( ( 1 <_ A /\ A e. RR ) -> ( ( A - 1 ) e. RR /\ 0 <_ ( A - 1 ) ) )
35 21 25 jca 
 |-  ( ( B e. RR /\ 1 < B ) -> ( ( B - 1 ) e. RR /\ 0 < ( B - 1 ) ) )
36 divge0 
 |-  ( ( ( ( A - 1 ) e. RR /\ 0 <_ ( A - 1 ) ) /\ ( ( B - 1 ) e. RR /\ 0 < ( B - 1 ) ) ) -> 0 <_ ( ( A - 1 ) / ( B - 1 ) ) )
37 34 35 36 syl2an 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> 0 <_ ( ( A - 1 ) / ( B - 1 ) ) )
38 flge0nn0 
 |-  ( ( ( ( A - 1 ) / ( B - 1 ) ) e. RR /\ 0 <_ ( ( A - 1 ) / ( B - 1 ) ) ) -> ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) e. NN0 )
39 29 37 38 syl2anc 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) e. NN0 )
40 nn0p1nn 
 |-  ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) e. NN0 -> ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. NN )
41 39 40 syl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. NN )
42 simplr 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> A e. RR )
43 21 adantl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( B - 1 ) e. RR )
44 peano2nn0 
 |-  ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) e. NN0 -> ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. NN0 )
45 39 44 syl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. NN0 )
46 45 nn0red 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. RR )
47 43 46 remulcld 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) e. RR )
48 peano2re 
 |-  ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) e. RR -> ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) e. RR )
49 47 48 syl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) e. RR )
50 simprl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> B e. RR )
51 reexpcl 
 |-  ( ( B e. RR /\ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. NN0 ) -> ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) e. RR )
52 50 45 51 syl2anc 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) e. RR )
53 flltp1 
 |-  ( ( ( A - 1 ) / ( B - 1 ) ) e. RR -> ( ( A - 1 ) / ( B - 1 ) ) < ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) )
54 29 53 syl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( A - 1 ) / ( B - 1 ) ) < ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) )
55 30 adantr 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( A - 1 ) e. RR )
56 25 adantl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> 0 < ( B - 1 ) )
57 ltdivmul 
 |-  ( ( ( A - 1 ) e. RR /\ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. RR /\ ( ( B - 1 ) e. RR /\ 0 < ( B - 1 ) ) ) -> ( ( ( A - 1 ) / ( B - 1 ) ) < ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) <-> ( A - 1 ) < ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) ) )
58 55 46 43 56 57 syl112anc 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( ( A - 1 ) / ( B - 1 ) ) < ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) <-> ( A - 1 ) < ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) ) )
59 54 58 mpbid 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( A - 1 ) < ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) )
60 ltsubadd 
 |-  ( ( A e. RR /\ 1 e. RR /\ ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) e. RR ) -> ( ( A - 1 ) < ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) <-> A < ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) ) )
61 2 60 mp3an2 
 |-  ( ( A e. RR /\ ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) e. RR ) -> ( ( A - 1 ) < ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) <-> A < ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) ) )
62 42 47 61 syl2anc 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( A - 1 ) < ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) <-> A < ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) ) )
63 59 62 mpbid 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> A < ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) )
64 0lt1 
 |-  0 < 1
65 0re 
 |-  0 e. RR
66 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ B e. RR ) -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) )
67 65 2 66 mp3an12 
 |-  ( B e. RR -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) )
68 64 67 mpani 
 |-  ( B e. RR -> ( 1 < B -> 0 < B ) )
69 ltle 
 |-  ( ( 0 e. RR /\ B e. RR ) -> ( 0 < B -> 0 <_ B ) )
70 65 69 mpan 
 |-  ( B e. RR -> ( 0 < B -> 0 <_ B ) )
71 68 70 syld 
 |-  ( B e. RR -> ( 1 < B -> 0 <_ B ) )
72 71 imp 
 |-  ( ( B e. RR /\ 1 < B ) -> 0 <_ B )
73 72 adantl 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> 0 <_ B )
74 bernneq2 
 |-  ( ( B e. RR /\ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. NN0 /\ 0 <_ B ) -> ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) <_ ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) )
75 50 45 73 74 syl3anc 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> ( ( ( B - 1 ) x. ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) + 1 ) <_ ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) )
76 42 49 52 63 75 ltletrd 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> A < ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) )
77 oveq2 
 |-  ( k = ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) -> ( B ^ k ) = ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) )
78 77 breq2d 
 |-  ( k = ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) -> ( A < ( B ^ k ) <-> A < ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) ) )
79 78 rspcev 
 |-  ( ( ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) e. NN /\ A < ( B ^ ( ( |_ ` ( ( A - 1 ) / ( B - 1 ) ) ) + 1 ) ) ) -> E. k e. NN A < ( B ^ k ) )
80 41 76 79 syl2anc 
 |-  ( ( ( 1 <_ A /\ A e. RR ) /\ ( B e. RR /\ 1 < B ) ) -> E. k e. NN A < ( B ^ k ) )
81 80 exp43 
 |-  ( 1 <_ A -> ( A e. RR -> ( B e. RR -> ( 1 < B -> E. k e. NN A < ( B ^ k ) ) ) ) )
82 81 com4l 
 |-  ( A e. RR -> ( B e. RR -> ( 1 < B -> ( 1 <_ A -> E. k e. NN A < ( B ^ k ) ) ) ) )
83 82 3imp1 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ 1 <_ A ) -> E. k e. NN A < ( B ^ k ) )
84 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> A e. RR )
85 1red 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 1 e. RR )
86 17 83 84 85 ltlecasei 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> E. k e. NN A < ( B ^ k ) )