Metamath Proof Explorer


Theorem cxp2limlem

Description: A linear factor grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion cxp2limlem A 1 < A n + n A n 0

Proof

Step Hyp Ref Expression
1 0red A 1 < A 0
2 2rp 2 +
3 rplogcl A 1 < A log A +
4 2z 2
5 rpexpcl log A + 2 log A 2 +
6 3 4 5 sylancl A 1 < A log A 2 +
7 rpdivcl 2 + log A 2 + 2 log A 2 +
8 2 6 7 sylancr A 1 < A 2 log A 2 +
9 8 rpcnd A 1 < A 2 log A 2
10 divrcnv 2 log A 2 n + 2 log A 2 n 0
11 9 10 syl A 1 < A n + 2 log A 2 n 0
12 8 rpred A 1 < A 2 log A 2
13 rerpdivcl 2 log A 2 n + 2 log A 2 n
14 12 13 sylan A 1 < A n + 2 log A 2 n
15 simpr A 1 < A n + n +
16 simpl A 1 < A A
17 1red A 1 < A 1
18 0lt1 0 < 1
19 18 a1i A 1 < A 0 < 1
20 simpr A 1 < A 1 < A
21 1 17 16 19 20 lttrd A 1 < A 0 < A
22 16 21 elrpd A 1 < A A +
23 rpre n + n
24 rpcxpcl A + n A n +
25 22 23 24 syl2an A 1 < A n + A n +
26 15 25 rpdivcld A 1 < A n + n A n +
27 26 rpred A 1 < A n + n A n
28 3 adantr A 1 < A n + log A +
29 15 28 rpmulcld A 1 < A n + n log A +
30 29 rpred A 1 < A n + n log A
31 30 resqcld A 1 < A n + n log A 2
32 31 rehalfcld A 1 < A n + n log A 2 2
33 1rp 1 +
34 rpaddcl 1 + n log A + 1 + n log A +
35 33 29 34 sylancr A 1 < A n + 1 + n log A +
36 35 rpred A 1 < A n + 1 + n log A
37 36 32 readdcld A 1 < A n + 1 + n log A + n log A 2 2
38 30 reefcld A 1 < A n + e n log A
39 32 35 ltaddrp2d A 1 < A n + n log A 2 2 < 1 + n log A + n log A 2 2
40 efgt1p2 n log A + 1 + n log A + n log A 2 2 < e n log A
41 29 40 syl A 1 < A n + 1 + n log A + n log A 2 2 < e n log A
42 32 37 38 39 41 lttrd A 1 < A n + n log A 2 2 < e n log A
43 23 adantl A 1 < A n + n
44 43 recnd A 1 < A n + n
45 44 sqcld A 1 < A n + n 2
46 2cnd A 1 < A n + 2
47 6 adantr A 1 < A n + log A 2 +
48 47 rpcnd A 1 < A n + log A 2
49 2ne0 2 0
50 49 a1i A 1 < A n + 2 0
51 47 rpne0d A 1 < A n + log A 2 0
52 45 46 48 50 51 divdiv2d A 1 < A n + n 2 2 log A 2 = n 2 log A 2 2
53 3 rpcnd A 1 < A log A
54 53 adantr A 1 < A n + log A
55 44 54 sqmuld A 1 < A n + n log A 2 = n 2 log A 2
56 55 oveq1d A 1 < A n + n log A 2 2 = n 2 log A 2 2
57 52 56 eqtr4d A 1 < A n + n 2 2 log A 2 = n log A 2 2
58 16 recnd A 1 < A A
59 58 adantr A 1 < A n + A
60 22 adantr A 1 < A n + A +
61 60 rpne0d A 1 < A n + A 0
62 59 61 44 cxpefd A 1 < A n + A n = e n log A
63 42 57 62 3brtr4d A 1 < A n + n 2 2 log A 2 < A n
64 rpexpcl n + 2 n 2 +
65 15 4 64 sylancl A 1 < A n + n 2 +
66 8 adantr A 1 < A n + 2 log A 2 +
67 65 66 rpdivcld A 1 < A n + n 2 2 log A 2 +
68 67 25 15 ltdiv2d A 1 < A n + n 2 2 log A 2 < A n n A n < n n 2 2 log A 2
69 63 68 mpbid A 1 < A n + n A n < n n 2 2 log A 2
70 9 adantr A 1 < A n + 2 log A 2
71 65 rpne0d A 1 < A n + n 2 0
72 66 rpne0d A 1 < A n + 2 log A 2 0
73 44 45 70 71 72 divdiv2d A 1 < A n + n n 2 2 log A 2 = n 2 log A 2 n 2
74 44 sqvald A 1 < A n + n 2 = n n
75 74 oveq2d A 1 < A n + n 2 log A 2 n 2 = n 2 log A 2 n n
76 rpne0 n + n 0
77 76 adantl A 1 < A n + n 0
78 70 44 44 77 77 divcan5d A 1 < A n + n 2 log A 2 n n = 2 log A 2 n
79 73 75 78 3eqtrd A 1 < A n + n n 2 2 log A 2 = 2 log A 2 n
80 69 79 breqtrd A 1 < A n + n A n < 2 log A 2 n
81 27 14 80 ltled A 1 < A n + n A n 2 log A 2 n
82 81 adantrr A 1 < A n + 0 n n A n 2 log A 2 n
83 26 rpge0d A 1 < A n + 0 n A n
84 83 adantrr A 1 < A n + 0 n 0 n A n
85 1 1 11 14 27 82 84 rlimsqz2 A 1 < A n + n A n 0