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 ) |