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 ) )