Metamath Proof Explorer


Theorem expmulnbnd

Description: Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion expmulnbnd A B 1 < B j 0 k j A k < B k

Proof

Step Hyp Ref Expression
1 2re 2
2 simp1 A B 1 < B A
3 remulcl 2 A 2 A
4 1 2 3 sylancr A B 1 < B 2 A
5 simp3 A B 1 < B 1 < B
6 1re 1
7 simp2 A B 1 < B B
8 difrp 1 B 1 < B B 1 +
9 6 7 8 sylancr A B 1 < B 1 < B B 1 +
10 5 9 mpbid A B 1 < B B 1 +
11 4 10 rerpdivcld A B 1 < B 2 A B 1
12 expnbnd 2 A B 1 B 1 < B n 2 A B 1 < B n
13 11 7 5 12 syl3anc A B 1 < B n 2 A B 1 < B n
14 2nn0 2 0
15 nnnn0 n n 0
16 15 ad2antrl A B 1 < B n 2 A B 1 < B n n 0
17 nn0mulcl 2 0 n 0 2 n 0
18 14 16 17 sylancr A B 1 < B n 2 A B 1 < B n 2 n 0
19 2 ad2antrr A B 1 < B n 2 A B 1 < B n k 2 n A
20 2nn 2
21 simprl A B 1 < B n 2 A B 1 < B n n
22 nnmulcl 2 n 2 n
23 20 21 22 sylancr A B 1 < B n 2 A B 1 < B n 2 n
24 eluznn 2 n k 2 n k
25 23 24 sylan A B 1 < B n 2 A B 1 < B n k 2 n k
26 25 nnred A B 1 < B n 2 A B 1 < B n k 2 n k
27 19 26 remulcld A B 1 < B n 2 A B 1 < B n k 2 n A k
28 0re 0
29 ifcl A 0 if 0 A A 0
30 19 28 29 sylancl A B 1 < B n 2 A B 1 < B n k 2 n if 0 A A 0
31 remulcl 2 if 0 A A 0 2 if 0 A A 0
32 1 30 31 sylancr A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0
33 simplrl A B 1 < B n 2 A B 1 < B n k 2 n n
34 33 nnred A B 1 < B n 2 A B 1 < B n k 2 n n
35 26 34 resubcld A B 1 < B n 2 A B 1 < B n k 2 n k n
36 32 35 remulcld A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0 k n
37 7 ad2antrr A B 1 < B n 2 A B 1 < B n k 2 n B
38 25 nnnn0d A B 1 < B n 2 A B 1 < B n k 2 n k 0
39 reexpcl B k 0 B k
40 37 38 39 syl2anc A B 1 < B n 2 A B 1 < B n k 2 n B k
41 remulcl 2 k n 2 k n
42 1 35 41 sylancr A B 1 < B n 2 A B 1 < B n k 2 n 2 k n
43 38 nn0ge0d A B 1 < B n 2 A B 1 < B n k 2 n 0 k
44 max1 0 A 0 if 0 A A 0
45 28 19 44 sylancr A B 1 < B n 2 A B 1 < B n k 2 n 0 if 0 A A 0
46 remulcl 2 n 2 n
47 1 34 46 sylancr A B 1 < B n 2 A B 1 < B n k 2 n 2 n
48 eluzle k 2 n 2 n k
49 48 adantl A B 1 < B n 2 A B 1 < B n k 2 n 2 n k
50 47 26 26 49 leadd2dd A B 1 < B n 2 A B 1 < B n k 2 n k + 2 n k + k
51 26 recnd A B 1 < B n 2 A B 1 < B n k 2 n k
52 51 2timesd A B 1 < B n 2 A B 1 < B n k 2 n 2 k = k + k
53 50 52 breqtrrd A B 1 < B n 2 A B 1 < B n k 2 n k + 2 n 2 k
54 remulcl 2 k 2 k
55 1 26 54 sylancr A B 1 < B n 2 A B 1 < B n k 2 n 2 k
56 leaddsub k 2 n 2 k k + 2 n 2 k k 2 k 2 n
57 26 47 55 56 syl3anc A B 1 < B n 2 A B 1 < B n k 2 n k + 2 n 2 k k 2 k 2 n
58 53 57 mpbid A B 1 < B n 2 A B 1 < B n k 2 n k 2 k 2 n
59 2cnd A B 1 < B n 2 A B 1 < B n k 2 n 2
60 34 recnd A B 1 < B n 2 A B 1 < B n k 2 n n
61 59 51 60 subdid A B 1 < B n 2 A B 1 < B n k 2 n 2 k n = 2 k 2 n
62 58 61 breqtrrd A B 1 < B n 2 A B 1 < B n k 2 n k 2 k n
63 max2 0 A A if 0 A A 0
64 28 19 63 sylancr A B 1 < B n 2 A B 1 < B n k 2 n A if 0 A A 0
65 26 42 19 30 43 45 62 64 lemul12bd A B 1 < B n 2 A B 1 < B n k 2 n k A 2 k n if 0 A A 0
66 19 recnd A B 1 < B n 2 A B 1 < B n k 2 n A
67 66 51 mulcomd A B 1 < B n 2 A B 1 < B n k 2 n A k = k A
68 30 recnd A B 1 < B n 2 A B 1 < B n k 2 n if 0 A A 0
69 35 recnd A B 1 < B n 2 A B 1 < B n k 2 n k n
70 59 68 69 mul32d A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0 k n = 2 k n if 0 A A 0
71 65 67 70 3brtr4d A B 1 < B n 2 A B 1 < B n k 2 n A k 2 if 0 A A 0 k n
72 10 ad2antrr A B 1 < B n 2 A B 1 < B n k 2 n B 1 +
73 72 rpred A B 1 < B n 2 A B 1 < B n k 2 n B 1
74 73 35 remulcld A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n
75 33 nnnn0d A B 1 < B n 2 A B 1 < B n k 2 n n 0
76 reexpcl B n 0 B n
77 37 75 76 syl2anc A B 1 < B n 2 A B 1 < B n k 2 n B n
78 74 77 remulcld A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n B n
79 simplrr A B 1 < B n 2 A B 1 < B n k 2 n 2 A B 1 < B n
80 1 19 3 sylancr A B 1 < B n 2 A B 1 < B n k 2 n 2 A
81 80 77 72 ltdivmuld A B 1 < B n 2 A B 1 < B n k 2 n 2 A B 1 < B n 2 A < B 1 B n
82 79 81 mpbid A B 1 < B n 2 A B 1 < B n k 2 n 2 A < B 1 B n
83 5 ad2antrr A B 1 < B n 2 A B 1 < B n k 2 n 1 < B
84 posdif 1 B 1 < B 0 < B 1
85 6 37 84 sylancr A B 1 < B n 2 A B 1 < B n k 2 n 1 < B 0 < B 1
86 83 85 mpbid A B 1 < B n 2 A B 1 < B n k 2 n 0 < B 1
87 33 nnzd A B 1 < B n 2 A B 1 < B n k 2 n n
88 28 a1i A B 1 < B n 2 A B 1 < B n k 2 n 0
89 6 a1i A B 1 < B n 2 A B 1 < B n k 2 n 1
90 0lt1 0 < 1
91 90 a1i A B 1 < B n 2 A B 1 < B n k 2 n 0 < 1
92 88 89 37 91 83 lttrd A B 1 < B n 2 A B 1 < B n k 2 n 0 < B
93 expgt0 B n 0 < B 0 < B n
94 37 87 92 93 syl3anc A B 1 < B n 2 A B 1 < B n k 2 n 0 < B n
95 73 77 86 94 mulgt0d A B 1 < B n 2 A B 1 < B n k 2 n 0 < B 1 B n
96 oveq2 A = if 0 A A 0 2 A = 2 if 0 A A 0
97 96 breq1d A = if 0 A A 0 2 A < B 1 B n 2 if 0 A A 0 < B 1 B n
98 2t0e0 2 0 = 0
99 oveq2 0 = if 0 A A 0 2 0 = 2 if 0 A A 0
100 98 99 eqtr3id 0 = if 0 A A 0 0 = 2 if 0 A A 0
101 100 breq1d 0 = if 0 A A 0 0 < B 1 B n 2 if 0 A A 0 < B 1 B n
102 97 101 ifboth 2 A < B 1 B n 0 < B 1 B n 2 if 0 A A 0 < B 1 B n
103 82 95 102 syl2anc A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0 < B 1 B n
104 73 77 remulcld A B 1 < B n 2 A B 1 < B n k 2 n B 1 B n
105 simpr A B 1 < B n 2 A B 1 < B n k 2 n k 2 n
106 60 2timesd A B 1 < B n 2 A B 1 < B n k 2 n 2 n = n + n
107 106 fveq2d A B 1 < B n 2 A B 1 < B n k 2 n 2 n = n + n
108 105 107 eleqtrd A B 1 < B n 2 A B 1 < B n k 2 n k n + n
109 eluzsub n n k n + n k n n
110 87 87 108 109 syl3anc A B 1 < B n 2 A B 1 < B n k 2 n k n n
111 eluznn n k n n k n
112 33 110 111 syl2anc A B 1 < B n 2 A B 1 < B n k 2 n k n
113 112 nngt0d A B 1 < B n 2 A B 1 < B n k 2 n 0 < k n
114 ltmul1 2 if 0 A A 0 B 1 B n k n 0 < k n 2 if 0 A A 0 < B 1 B n 2 if 0 A A 0 k n < B 1 B n k n
115 32 104 35 113 114 syl112anc A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0 < B 1 B n 2 if 0 A A 0 k n < B 1 B n k n
116 103 115 mpbid A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0 k n < B 1 B n k n
117 73 recnd A B 1 < B n 2 A B 1 < B n k 2 n B 1
118 77 recnd A B 1 < B n 2 A B 1 < B n k 2 n B n
119 117 118 69 mul32d A B 1 < B n 2 A B 1 < B n k 2 n B 1 B n k n = B 1 k n B n
120 116 119 breqtrd A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0 k n < B 1 k n B n
121 peano2re B 1 k n B 1 k n + 1
122 74 121 syl A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n + 1
123 112 nnnn0d A B 1 < B n 2 A B 1 < B n k 2 n k n 0
124 reexpcl B k n 0 B k n
125 37 123 124 syl2anc A B 1 < B n 2 A B 1 < B n k 2 n B k n
126 74 ltp1d A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n < B 1 k n + 1
127 88 37 92 ltled A B 1 < B n 2 A B 1 < B n k 2 n 0 B
128 bernneq2 B k n 0 0 B B 1 k n + 1 B k n
129 37 123 127 128 syl3anc A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n + 1 B k n
130 74 122 125 126 129 ltletrd A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n < B k n
131 37 recnd A B 1 < B n 2 A B 1 < B n k 2 n B
132 92 gt0ne0d A B 1 < B n 2 A B 1 < B n k 2 n B 0
133 eluzelz k 2 n k
134 133 adantl A B 1 < B n 2 A B 1 < B n k 2 n k
135 expsub B B 0 k n B k n = B k B n
136 131 132 134 87 135 syl22anc A B 1 < B n 2 A B 1 < B n k 2 n B k n = B k B n
137 130 136 breqtrd A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n < B k B n
138 ltmuldiv B 1 k n B k B n 0 < B n B 1 k n B n < B k B 1 k n < B k B n
139 74 40 77 94 138 syl112anc A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n B n < B k B 1 k n < B k B n
140 137 139 mpbird A B 1 < B n 2 A B 1 < B n k 2 n B 1 k n B n < B k
141 36 78 40 120 140 lttrd A B 1 < B n 2 A B 1 < B n k 2 n 2 if 0 A A 0 k n < B k
142 27 36 40 71 141 lelttrd A B 1 < B n 2 A B 1 < B n k 2 n A k < B k
143 142 ralrimiva A B 1 < B n 2 A B 1 < B n k 2 n A k < B k
144 fveq2 j = 2 n j = 2 n
145 144 raleqdv j = 2 n k j A k < B k k 2 n A k < B k
146 145 rspcev 2 n 0 k 2 n A k < B k j 0 k j A k < B k
147 18 143 146 syl2anc A B 1 < B n 2 A B 1 < B n j 0 k j A k < B k
148 13 147 rexlimddv A B 1 < B j 0 k j A k < B k