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 A1<An+nAn0

Proof

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