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 )