Metamath Proof Explorer


Theorem cxp2lim

Description: Any power grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion cxp2lim A B 1 < B n + n A B n 0

Proof

Step Hyp Ref Expression
1 1re 1
2 elicopnf 1 n 1 +∞ n 1 n
3 1 2 ax-mp n 1 +∞ n 1 n
4 3 simplbi n 1 +∞ n
5 0red n 1 +∞ 0
6 1red n 1 +∞ 1
7 0lt1 0 < 1
8 7 a1i n 1 +∞ 0 < 1
9 3 simprbi n 1 +∞ 1 n
10 5 6 4 8 9 ltletrd n 1 +∞ 0 < n
11 4 10 elrpd n 1 +∞ n +
12 11 ssriv 1 +∞ +
13 resmpt 1 +∞ + n + n A B n 1 +∞ = n 1 +∞ n A B n
14 12 13 ax-mp n + n A B n 1 +∞ = n 1 +∞ n A B n
15 0red A B 1 < B 0
16 12 a1i A B 1 < B 1 +∞ +
17 rpre n + n
18 17 adantl A B 1 < B n + n
19 rpge0 n + 0 n
20 19 adantl A B 1 < B n + 0 n
21 simpl2 A B 1 < B n + B
22 0red A B 1 < B n + 0
23 1red A B 1 < B n + 1
24 7 a1i A B 1 < B n + 0 < 1
25 simpl3 A B 1 < B n + 1 < B
26 22 23 21 24 25 lttrd A B 1 < B n + 0 < B
27 21 26 elrpd A B 1 < B n + B +
28 27 18 rpcxpcld A B 1 < B n + B n +
29 simp1 A B 1 < B A
30 ifcl A 1 if 1 A A 1
31 29 1 30 sylancl A B 1 < B if 1 A A 1
32 1red A B 1 < B 1
33 7 a1i A B 1 < B 0 < 1
34 max1 1 A 1 if 1 A A 1
35 1 29 34 sylancr A B 1 < B 1 if 1 A A 1
36 15 32 31 33 35 ltletrd A B 1 < B 0 < if 1 A A 1
37 31 36 elrpd A B 1 < B if 1 A A 1 +
38 37 rprecred A B 1 < B 1 if 1 A A 1
39 38 adantr A B 1 < B n + 1 if 1 A A 1
40 28 39 rpcxpcld A B 1 < B n + B n 1 if 1 A A 1 +
41 31 recnd A B 1 < B if 1 A A 1
42 41 adantr A B 1 < B n + if 1 A A 1
43 18 20 40 42 divcxpd A B 1 < B n + n B n 1 if 1 A A 1 if 1 A A 1 = n if 1 A A 1 B n 1 if 1 A A 1 if 1 A A 1
44 37 adantr A B 1 < B n + if 1 A A 1 +
45 44 rpne0d A B 1 < B n + if 1 A A 1 0
46 42 45 recid2d A B 1 < B n + 1 if 1 A A 1 if 1 A A 1 = 1
47 46 oveq2d A B 1 < B n + B n 1 if 1 A A 1 if 1 A A 1 = B n 1
48 28 39 42 cxpmuld A B 1 < B n + B n 1 if 1 A A 1 if 1 A A 1 = B n 1 if 1 A A 1 if 1 A A 1
49 28 rpcnd A B 1 < B n + B n
50 49 cxp1d A B 1 < B n + B n 1 = B n
51 47 48 50 3eqtr3d A B 1 < B n + B n 1 if 1 A A 1 if 1 A A 1 = B n
52 51 oveq2d A B 1 < B n + n if 1 A A 1 B n 1 if 1 A A 1 if 1 A A 1 = n if 1 A A 1 B n
53 43 52 eqtrd A B 1 < B n + n B n 1 if 1 A A 1 if 1 A A 1 = n if 1 A A 1 B n
54 53 mpteq2dva A B 1 < B n + n B n 1 if 1 A A 1 if 1 A A 1 = n + n if 1 A A 1 B n
55 ovexd A B 1 < B n + n B n 1 if 1 A A 1 V
56 18 recnd A B 1 < B n + n
57 38 recnd A B 1 < B 1 if 1 A A 1
58 57 adantr A B 1 < B n + 1 if 1 A A 1
59 56 58 mulcomd A B 1 < B n + n 1 if 1 A A 1 = 1 if 1 A A 1 n
60 59 oveq2d A B 1 < B n + B n 1 if 1 A A 1 = B 1 if 1 A A 1 n
61 27 18 58 cxpmuld A B 1 < B n + B n 1 if 1 A A 1 = B n 1 if 1 A A 1
62 27 39 56 cxpmuld A B 1 < B n + B 1 if 1 A A 1 n = B 1 if 1 A A 1 n
63 60 61 62 3eqtr3d A B 1 < B n + B n 1 if 1 A A 1 = B 1 if 1 A A 1 n
64 63 oveq2d A B 1 < B n + n B n 1 if 1 A A 1 = n B 1 if 1 A A 1 n
65 64 mpteq2dva A B 1 < B n + n B n 1 if 1 A A 1 = n + n B 1 if 1 A A 1 n
66 simp2 A B 1 < B B
67 simp3 A B 1 < B 1 < B
68 15 32 66 33 67 lttrd A B 1 < B 0 < B
69 66 68 elrpd A B 1 < B B +
70 69 38 rpcxpcld A B 1 < B B 1 if 1 A A 1 +
71 70 rpred A B 1 < B B 1 if 1 A A 1
72 57 1cxpd A B 1 < B 1 1 if 1 A A 1 = 1
73 0le1 0 1
74 73 a1i A B 1 < B 0 1
75 69 rpge0d A B 1 < B 0 B
76 37 rpreccld A B 1 < B 1 if 1 A A 1 +
77 32 74 66 75 76 cxplt2d A B 1 < B 1 < B 1 1 if 1 A A 1 < B 1 if 1 A A 1
78 67 77 mpbid A B 1 < B 1 1 if 1 A A 1 < B 1 if 1 A A 1
79 72 78 eqbrtrrd A B 1 < B 1 < B 1 if 1 A A 1
80 cxp2limlem B 1 if 1 A A 1 1 < B 1 if 1 A A 1 n + n B 1 if 1 A A 1 n 0
81 71 79 80 syl2anc A B 1 < B n + n B 1 if 1 A A 1 n 0
82 65 81 eqbrtrd A B 1 < B n + n B n 1 if 1 A A 1 0
83 55 82 37 rlimcxp A B 1 < B n + n B n 1 if 1 A A 1 if 1 A A 1 0
84 54 83 eqbrtrrd A B 1 < B n + n if 1 A A 1 B n 0
85 16 84 rlimres2 A B 1 < B n 1 +∞ n if 1 A A 1 B n 0
86 simpr A B 1 < B n + n +
87 31 adantr A B 1 < B n + if 1 A A 1
88 86 87 rpcxpcld A B 1 < B n + n if 1 A A 1 +
89 88 28 rpdivcld A B 1 < B n + n if 1 A A 1 B n +
90 89 rpred A B 1 < B n + n if 1 A A 1 B n
91 11 90 sylan2 A B 1 < B n 1 +∞ n if 1 A A 1 B n
92 simpl1 A B 1 < B n + A
93 86 92 rpcxpcld A B 1 < B n + n A +
94 93 28 rpdivcld A B 1 < B n + n A B n +
95 11 94 sylan2 A B 1 < B n 1 +∞ n A B n +
96 95 rpred A B 1 < B n 1 +∞ n A B n
97 11 93 sylan2 A B 1 < B n 1 +∞ n A +
98 97 rpred A B 1 < B n 1 +∞ n A
99 11 88 sylan2 A B 1 < B n 1 +∞ n if 1 A A 1 +
100 99 rpred A B 1 < B n 1 +∞ n if 1 A A 1
101 11 28 sylan2 A B 1 < B n 1 +∞ B n +
102 4 adantl A B 1 < B n 1 +∞ n
103 9 adantl A B 1 < B n 1 +∞ 1 n
104 simpl1 A B 1 < B n 1 +∞ A
105 31 adantr A B 1 < B n 1 +∞ if 1 A A 1
106 max2 1 A A if 1 A A 1
107 1 104 106 sylancr A B 1 < B n 1 +∞ A if 1 A A 1
108 102 103 104 105 107 cxplead A B 1 < B n 1 +∞ n A n if 1 A A 1
109 98 100 101 108 lediv1dd A B 1 < B n 1 +∞ n A B n n if 1 A A 1 B n
110 109 adantrr A B 1 < B n 1 +∞ 0 n n A B n n if 1 A A 1 B n
111 95 rpge0d A B 1 < B n 1 +∞ 0 n A B n
112 111 adantrr A B 1 < B n 1 +∞ 0 n 0 n A B n
113 15 15 85 91 96 110 112 rlimsqz2 A B 1 < B n 1 +∞ n A B n 0
114 14 113 eqbrtrid A B 1 < B n + n A B n 1 +∞ 0
115 94 rpcnd A B 1 < B n + n A B n
116 115 fmpttd A B 1 < B n + n A B n : +
117 rpssre +
118 117 a1i A B 1 < B +
119 116 118 32 rlimresb A B 1 < B n + n A B n 0 n + n A B n 1 +∞ 0
120 114 119 mpbird A B 1 < B n + n A B n 0