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 e. RR /\ 1 < A ) -> ( n e. RR+ |-> ( n / ( A ^c n ) ) ) ~~>r 0 )

Proof

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