Step |
Hyp |
Ref |
Expression |
1 |
|
fzfid |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( 1 ... ( |_ ` A ) ) e. Fin ) |
2 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN ) |
3 |
2
|
adantl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN ) |
4 |
3
|
nnrpd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. RR+ ) |
5 |
4
|
relogcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. RR ) |
6 |
5
|
resqcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` n ) ^ 2 ) e. RR ) |
7 |
1 6
|
fsumrecl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) e. RR ) |
8 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
9 |
8
|
adantr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR ) |
10 |
|
relogcl |
|- ( A e. RR+ -> ( log ` A ) e. RR ) |
11 |
10
|
adantr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` A ) e. RR ) |
12 |
11
|
resqcld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` A ) ^ 2 ) e. RR ) |
13 |
|
2re |
|- 2 e. RR |
14 |
|
remulcl |
|- ( ( 2 e. RR /\ ( log ` A ) e. RR ) -> ( 2 x. ( log ` A ) ) e. RR ) |
15 |
13 11 14
|
sylancr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( 2 x. ( log ` A ) ) e. RR ) |
16 |
|
resubcl |
|- ( ( 2 e. RR /\ ( 2 x. ( log ` A ) ) e. RR ) -> ( 2 - ( 2 x. ( log ` A ) ) ) e. RR ) |
17 |
13 15 16
|
sylancr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( 2 - ( 2 x. ( log ` A ) ) ) e. RR ) |
18 |
12 17
|
readdcld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) e. RR ) |
19 |
9 18
|
remulcld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) e. RR ) |
20 |
7 19
|
resubcld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) e. RR ) |
21 |
20
|
recnd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) e. CC ) |
22 |
21
|
abscld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) e. RR ) |
23 |
|
resubcl |
|- ( ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) e. RR /\ 2 e. RR ) -> ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - 2 ) e. RR ) |
24 |
22 13 23
|
sylancl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - 2 ) e. RR ) |
25 |
|
2cn |
|- 2 e. CC |
26 |
25
|
negcli |
|- -u 2 e. CC |
27 |
|
subcl |
|- ( ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) e. CC /\ -u 2 e. CC ) -> ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) e. CC ) |
28 |
21 26 27
|
sylancl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) e. CC ) |
29 |
28
|
abscld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) ) e. RR ) |
30 |
25
|
absnegi |
|- ( abs ` -u 2 ) = ( abs ` 2 ) |
31 |
|
0le2 |
|- 0 <_ 2 |
32 |
|
absid |
|- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 ) |
33 |
13 31 32
|
mp2an |
|- ( abs ` 2 ) = 2 |
34 |
30 33
|
eqtri |
|- ( abs ` -u 2 ) = 2 |
35 |
34
|
oveq2i |
|- ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - ( abs ` -u 2 ) ) = ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - 2 ) |
36 |
|
abs2dif |
|- ( ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) e. CC /\ -u 2 e. CC ) -> ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - ( abs ` -u 2 ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) ) ) |
37 |
21 26 36
|
sylancl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - ( abs ` -u 2 ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) ) ) |
38 |
35 37
|
eqbrtrrid |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - 2 ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) ) ) |
39 |
|
fveq2 |
|- ( x = A -> ( |_ ` x ) = ( |_ ` A ) ) |
40 |
39
|
oveq2d |
|- ( x = A -> ( 1 ... ( |_ ` x ) ) = ( 1 ... ( |_ ` A ) ) ) |
41 |
40
|
sumeq1d |
|- ( x = A -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) ) |
42 |
|
id |
|- ( x = A -> x = A ) |
43 |
|
fveq2 |
|- ( x = A -> ( log ` x ) = ( log ` A ) ) |
44 |
43
|
oveq1d |
|- ( x = A -> ( ( log ` x ) ^ 2 ) = ( ( log ` A ) ^ 2 ) ) |
45 |
43
|
oveq2d |
|- ( x = A -> ( 2 x. ( log ` x ) ) = ( 2 x. ( log ` A ) ) ) |
46 |
45
|
oveq2d |
|- ( x = A -> ( 2 - ( 2 x. ( log ` x ) ) ) = ( 2 - ( 2 x. ( log ` A ) ) ) ) |
47 |
44 46
|
oveq12d |
|- ( x = A -> ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) = ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) |
48 |
42 47
|
oveq12d |
|- ( x = A -> ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) = ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) |
49 |
41 48
|
oveq12d |
|- ( x = A -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) |
50 |
|
eqid |
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) |
51 |
|
ovex |
|- ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) e. _V |
52 |
49 50 51
|
fvmpt3i |
|- ( A e. RR+ -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` A ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) |
53 |
52
|
adantr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` A ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) |
54 |
|
1rp |
|- 1 e. RR+ |
55 |
|
fveq2 |
|- ( x = 1 -> ( |_ ` x ) = ( |_ ` 1 ) ) |
56 |
|
1z |
|- 1 e. ZZ |
57 |
|
flid |
|- ( 1 e. ZZ -> ( |_ ` 1 ) = 1 ) |
58 |
56 57
|
ax-mp |
|- ( |_ ` 1 ) = 1 |
59 |
55 58
|
eqtrdi |
|- ( x = 1 -> ( |_ ` x ) = 1 ) |
60 |
59
|
oveq2d |
|- ( x = 1 -> ( 1 ... ( |_ ` x ) ) = ( 1 ... 1 ) ) |
61 |
60
|
sumeq1d |
|- ( x = 1 -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) = sum_ n e. ( 1 ... 1 ) ( ( log ` n ) ^ 2 ) ) |
62 |
|
0cn |
|- 0 e. CC |
63 |
|
fveq2 |
|- ( n = 1 -> ( log ` n ) = ( log ` 1 ) ) |
64 |
|
log1 |
|- ( log ` 1 ) = 0 |
65 |
63 64
|
eqtrdi |
|- ( n = 1 -> ( log ` n ) = 0 ) |
66 |
65
|
sq0id |
|- ( n = 1 -> ( ( log ` n ) ^ 2 ) = 0 ) |
67 |
66
|
fsum1 |
|- ( ( 1 e. ZZ /\ 0 e. CC ) -> sum_ n e. ( 1 ... 1 ) ( ( log ` n ) ^ 2 ) = 0 ) |
68 |
56 62 67
|
mp2an |
|- sum_ n e. ( 1 ... 1 ) ( ( log ` n ) ^ 2 ) = 0 |
69 |
61 68
|
eqtrdi |
|- ( x = 1 -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) = 0 ) |
70 |
|
id |
|- ( x = 1 -> x = 1 ) |
71 |
|
fveq2 |
|- ( x = 1 -> ( log ` x ) = ( log ` 1 ) ) |
72 |
71 64
|
eqtrdi |
|- ( x = 1 -> ( log ` x ) = 0 ) |
73 |
72
|
sq0id |
|- ( x = 1 -> ( ( log ` x ) ^ 2 ) = 0 ) |
74 |
72
|
oveq2d |
|- ( x = 1 -> ( 2 x. ( log ` x ) ) = ( 2 x. 0 ) ) |
75 |
|
2t0e0 |
|- ( 2 x. 0 ) = 0 |
76 |
74 75
|
eqtrdi |
|- ( x = 1 -> ( 2 x. ( log ` x ) ) = 0 ) |
77 |
76
|
oveq2d |
|- ( x = 1 -> ( 2 - ( 2 x. ( log ` x ) ) ) = ( 2 - 0 ) ) |
78 |
25
|
subid1i |
|- ( 2 - 0 ) = 2 |
79 |
77 78
|
eqtrdi |
|- ( x = 1 -> ( 2 - ( 2 x. ( log ` x ) ) ) = 2 ) |
80 |
73 79
|
oveq12d |
|- ( x = 1 -> ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) = ( 0 + 2 ) ) |
81 |
25
|
addid2i |
|- ( 0 + 2 ) = 2 |
82 |
80 81
|
eqtrdi |
|- ( x = 1 -> ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) = 2 ) |
83 |
70 82
|
oveq12d |
|- ( x = 1 -> ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) = ( 1 x. 2 ) ) |
84 |
25
|
mulid2i |
|- ( 1 x. 2 ) = 2 |
85 |
83 84
|
eqtrdi |
|- ( x = 1 -> ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) = 2 ) |
86 |
69 85
|
oveq12d |
|- ( x = 1 -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) = ( 0 - 2 ) ) |
87 |
|
df-neg |
|- -u 2 = ( 0 - 2 ) |
88 |
86 87
|
eqtr4di |
|- ( x = 1 -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) = -u 2 ) |
89 |
88 50 51
|
fvmpt3i |
|- ( 1 e. RR+ -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` 1 ) = -u 2 ) |
90 |
54 89
|
mp1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` 1 ) = -u 2 ) |
91 |
53 90
|
oveq12d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` 1 ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) ) |
92 |
91
|
fveq2d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` 1 ) ) ) = ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) ) ) |
93 |
|
ioorp |
|- ( 0 (,) +oo ) = RR+ |
94 |
93
|
eqcomi |
|- RR+ = ( 0 (,) +oo ) |
95 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
96 |
56
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. ZZ ) |
97 |
|
1red |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. RR ) |
98 |
|
pnfxr |
|- +oo e. RR* |
99 |
98
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> +oo e. RR* ) |
100 |
|
1re |
|- 1 e. RR |
101 |
|
1nn0 |
|- 1 e. NN0 |
102 |
100 101
|
nn0addge1i |
|- 1 <_ ( 1 + 1 ) |
103 |
102
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ ( 1 + 1 ) ) |
104 |
|
0red |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 0 e. RR ) |
105 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
106 |
105
|
adantl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> x e. RR ) |
107 |
|
simpr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> x e. RR+ ) |
108 |
107
|
relogcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( log ` x ) e. RR ) |
109 |
108
|
resqcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( log ` x ) ^ 2 ) e. RR ) |
110 |
|
remulcl |
|- ( ( 2 e. RR /\ ( log ` x ) e. RR ) -> ( 2 x. ( log ` x ) ) e. RR ) |
111 |
13 108 110
|
sylancr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 2 x. ( log ` x ) ) e. RR ) |
112 |
|
resubcl |
|- ( ( 2 e. RR /\ ( 2 x. ( log ` x ) ) e. RR ) -> ( 2 - ( 2 x. ( log ` x ) ) ) e. RR ) |
113 |
13 111 112
|
sylancr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 2 - ( 2 x. ( log ` x ) ) ) e. RR ) |
114 |
109 113
|
readdcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) e. RR ) |
115 |
106 114
|
remulcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) e. RR ) |
116 |
|
nnrp |
|- ( x e. NN -> x e. RR+ ) |
117 |
116 109
|
sylan2 |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. NN ) -> ( ( log ` x ) ^ 2 ) e. RR ) |
118 |
|
reelprrecn |
|- RR e. { RR , CC } |
119 |
118
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> RR e. { RR , CC } ) |
120 |
106
|
recnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> x e. CC ) |
121 |
|
1red |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> 1 e. RR ) |
122 |
|
recn |
|- ( x e. RR -> x e. CC ) |
123 |
122
|
adantl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR ) -> x e. CC ) |
124 |
|
1red |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR ) -> 1 e. RR ) |
125 |
119
|
dvmptid |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) ) |
126 |
|
rpssre |
|- RR+ C_ RR |
127 |
126
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> RR+ C_ RR ) |
128 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
129 |
128
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
130 |
|
iooretop |
|- ( 0 (,) +oo ) e. ( topGen ` ran (,) ) |
131 |
93 130
|
eqeltrri |
|- RR+ e. ( topGen ` ran (,) ) |
132 |
131
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> RR+ e. ( topGen ` ran (,) ) ) |
133 |
119 123 124 125 127 129 128 132
|
dvmptres |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> x ) ) = ( x e. RR+ |-> 1 ) ) |
134 |
114
|
recnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) e. CC ) |
135 |
|
resubcl |
|- ( ( ( 2 x. ( log ` x ) ) e. RR /\ 2 e. RR ) -> ( ( 2 x. ( log ` x ) ) - 2 ) e. RR ) |
136 |
111 13 135
|
sylancl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( 2 x. ( log ` x ) ) - 2 ) e. RR ) |
137 |
136 107
|
rerpdivcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) e. RR ) |
138 |
109
|
recnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( log ` x ) ^ 2 ) e. CC ) |
139 |
111
|
recnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 2 x. ( log ` x ) ) e. CC ) |
140 |
107
|
rpreccld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 1 / x ) e. RR+ ) |
141 |
140
|
rpcnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 1 / x ) e. CC ) |
142 |
139 141
|
mulcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) e. CC ) |
143 |
|
cnelprrecn |
|- CC e. { RR , CC } |
144 |
143
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> CC e. { RR , CC } ) |
145 |
108
|
recnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( log ` x ) e. CC ) |
146 |
|
sqcl |
|- ( y e. CC -> ( y ^ 2 ) e. CC ) |
147 |
146
|
adantl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ y e. CC ) -> ( y ^ 2 ) e. CC ) |
148 |
|
simpr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ y e. CC ) -> y e. CC ) |
149 |
|
mulcl |
|- ( ( 2 e. CC /\ y e. CC ) -> ( 2 x. y ) e. CC ) |
150 |
25 148 149
|
sylancr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ y e. CC ) -> ( 2 x. y ) e. CC ) |
151 |
|
dvrelog |
|- ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) ) |
152 |
|
relogf1o |
|- ( log |` RR+ ) : RR+ -1-1-onto-> RR |
153 |
|
f1of |
|- ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR ) |
154 |
152 153
|
mp1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log |` RR+ ) : RR+ --> RR ) |
155 |
154
|
feqmptd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) ) |
156 |
|
fvres |
|- ( x e. RR+ -> ( ( log |` RR+ ) ` x ) = ( log ` x ) ) |
157 |
156
|
mpteq2ia |
|- ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) = ( x e. RR+ |-> ( log ` x ) ) |
158 |
155 157
|
eqtrdi |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) ) |
159 |
158
|
oveq2d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) ) |
160 |
151 159
|
syl5reqr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) ) |
161 |
|
2nn |
|- 2 e. NN |
162 |
|
dvexp |
|- ( 2 e. NN -> ( CC _D ( y e. CC |-> ( y ^ 2 ) ) ) = ( y e. CC |-> ( 2 x. ( y ^ ( 2 - 1 ) ) ) ) ) |
163 |
161 162
|
mp1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( CC _D ( y e. CC |-> ( y ^ 2 ) ) ) = ( y e. CC |-> ( 2 x. ( y ^ ( 2 - 1 ) ) ) ) ) |
164 |
|
2m1e1 |
|- ( 2 - 1 ) = 1 |
165 |
164
|
oveq2i |
|- ( y ^ ( 2 - 1 ) ) = ( y ^ 1 ) |
166 |
|
exp1 |
|- ( y e. CC -> ( y ^ 1 ) = y ) |
167 |
165 166
|
syl5eq |
|- ( y e. CC -> ( y ^ ( 2 - 1 ) ) = y ) |
168 |
167
|
oveq2d |
|- ( y e. CC -> ( 2 x. ( y ^ ( 2 - 1 ) ) ) = ( 2 x. y ) ) |
169 |
168
|
mpteq2ia |
|- ( y e. CC |-> ( 2 x. ( y ^ ( 2 - 1 ) ) ) ) = ( y e. CC |-> ( 2 x. y ) ) |
170 |
163 169
|
eqtrdi |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( CC _D ( y e. CC |-> ( y ^ 2 ) ) ) = ( y e. CC |-> ( 2 x. y ) ) ) |
171 |
|
oveq1 |
|- ( y = ( log ` x ) -> ( y ^ 2 ) = ( ( log ` x ) ^ 2 ) ) |
172 |
|
oveq2 |
|- ( y = ( log ` x ) -> ( 2 x. y ) = ( 2 x. ( log ` x ) ) ) |
173 |
119 144 145 140 147 150 160 170 171 172
|
dvmptco |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( ( log ` x ) ^ 2 ) ) ) = ( x e. RR+ |-> ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) ) ) |
174 |
113
|
recnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 2 - ( 2 x. ( log ` x ) ) ) e. CC ) |
175 |
|
ovexd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 0 - ( 2 x. ( 1 / x ) ) ) e. _V ) |
176 |
|
2cnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> 2 e. CC ) |
177 |
|
0red |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> 0 e. RR ) |
178 |
|
2cnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR ) -> 2 e. CC ) |
179 |
|
0red |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR ) -> 0 e. RR ) |
180 |
|
2cnd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 2 e. CC ) |
181 |
119 180
|
dvmptc |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR |-> 2 ) ) = ( x e. RR |-> 0 ) ) |
182 |
119 178 179 181 127 129 128 132
|
dvmptres |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> 2 ) ) = ( x e. RR+ |-> 0 ) ) |
183 |
|
mulcl |
|- ( ( 2 e. CC /\ ( 1 / x ) e. CC ) -> ( 2 x. ( 1 / x ) ) e. CC ) |
184 |
25 141 183
|
sylancr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 2 x. ( 1 / x ) ) e. CC ) |
185 |
119 145 140 160 180
|
dvmptcmul |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( 2 x. ( log ` x ) ) ) ) = ( x e. RR+ |-> ( 2 x. ( 1 / x ) ) ) ) |
186 |
119 176 177 182 139 184 185
|
dvmptsub |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( 2 - ( 2 x. ( log ` x ) ) ) ) ) = ( x e. RR+ |-> ( 0 - ( 2 x. ( 1 / x ) ) ) ) ) |
187 |
119 138 142 173 174 175 186
|
dvmptadd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) = ( x e. RR+ |-> ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) + ( 0 - ( 2 x. ( 1 / x ) ) ) ) ) ) |
188 |
139 176 141
|
subdird |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( 2 x. ( log ` x ) ) - 2 ) x. ( 1 / x ) ) = ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) - ( 2 x. ( 1 / x ) ) ) ) |
189 |
136
|
recnd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( 2 x. ( log ` x ) ) - 2 ) e. CC ) |
190 |
|
rpne0 |
|- ( x e. RR+ -> x =/= 0 ) |
191 |
190
|
adantl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> x =/= 0 ) |
192 |
189 120 191
|
divrecd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) = ( ( ( 2 x. ( log ` x ) ) - 2 ) x. ( 1 / x ) ) ) |
193 |
|
df-neg |
|- -u ( 2 x. ( 1 / x ) ) = ( 0 - ( 2 x. ( 1 / x ) ) ) |
194 |
193
|
oveq2i |
|- ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) + -u ( 2 x. ( 1 / x ) ) ) = ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) + ( 0 - ( 2 x. ( 1 / x ) ) ) ) |
195 |
142 184
|
negsubd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) + -u ( 2 x. ( 1 / x ) ) ) = ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) - ( 2 x. ( 1 / x ) ) ) ) |
196 |
194 195
|
syl5eqr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) + ( 0 - ( 2 x. ( 1 / x ) ) ) ) = ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) - ( 2 x. ( 1 / x ) ) ) ) |
197 |
188 192 196
|
3eqtr4rd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) + ( 0 - ( 2 x. ( 1 / x ) ) ) ) = ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) ) |
198 |
197
|
mpteq2dva |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( x e. RR+ |-> ( ( ( 2 x. ( log ` x ) ) x. ( 1 / x ) ) + ( 0 - ( 2 x. ( 1 / x ) ) ) ) ) = ( x e. RR+ |-> ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) ) ) |
199 |
187 198
|
eqtrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) = ( x e. RR+ |-> ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) ) ) |
200 |
119 120 121 133 134 137 199
|
dvmptmul |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) = ( x e. RR+ |-> ( ( 1 x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) + ( ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) x. x ) ) ) ) |
201 |
134
|
mulid2d |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 1 x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) = ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) |
202 |
138 139 176
|
subsub2d |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( log ` x ) ^ 2 ) - ( ( 2 x. ( log ` x ) ) - 2 ) ) = ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) |
203 |
201 202
|
eqtr4d |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( 1 x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) = ( ( ( log ` x ) ^ 2 ) - ( ( 2 x. ( log ` x ) ) - 2 ) ) ) |
204 |
189 120 191
|
divcan1d |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) x. x ) = ( ( 2 x. ( log ` x ) ) - 2 ) ) |
205 |
203 204
|
oveq12d |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( 1 x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) + ( ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) x. x ) ) = ( ( ( ( log ` x ) ^ 2 ) - ( ( 2 x. ( log ` x ) ) - 2 ) ) + ( ( 2 x. ( log ` x ) ) - 2 ) ) ) |
206 |
138 189
|
npcand |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( ( ( log ` x ) ^ 2 ) - ( ( 2 x. ( log ` x ) ) - 2 ) ) + ( ( 2 x. ( log ` x ) ) - 2 ) ) = ( ( log ` x ) ^ 2 ) ) |
207 |
205 206
|
eqtrd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( 1 x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) + ( ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) x. x ) ) = ( ( log ` x ) ^ 2 ) ) |
208 |
207
|
mpteq2dva |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( x e. RR+ |-> ( ( 1 x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) + ( ( ( ( 2 x. ( log ` x ) ) - 2 ) / x ) x. x ) ) ) = ( x e. RR+ |-> ( ( log ` x ) ^ 2 ) ) ) |
209 |
200 208
|
eqtrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) = ( x e. RR+ |-> ( ( log ` x ) ^ 2 ) ) ) |
210 |
|
fveq2 |
|- ( x = n -> ( log ` x ) = ( log ` n ) ) |
211 |
210
|
oveq1d |
|- ( x = n -> ( ( log ` x ) ^ 2 ) = ( ( log ` n ) ^ 2 ) ) |
212 |
|
simp32 |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> x <_ n ) |
213 |
|
simp2l |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> x e. RR+ ) |
214 |
|
simp2r |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> n e. RR+ ) |
215 |
213 214
|
logled |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( x <_ n <-> ( log ` x ) <_ ( log ` n ) ) ) |
216 |
212 215
|
mpbid |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( log ` x ) <_ ( log ` n ) ) |
217 |
213
|
relogcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( log ` x ) e. RR ) |
218 |
214
|
relogcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( log ` n ) e. RR ) |
219 |
|
simp31 |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> 1 <_ x ) |
220 |
|
logleb |
|- ( ( 1 e. RR+ /\ x e. RR+ ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) ) |
221 |
54 213 220
|
sylancr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) ) |
222 |
219 221
|
mpbid |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( log ` 1 ) <_ ( log ` x ) ) |
223 |
64 222
|
eqbrtrrid |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> 0 <_ ( log ` x ) ) |
224 |
214
|
rpred |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> n e. RR ) |
225 |
|
1red |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> 1 e. RR ) |
226 |
213
|
rpred |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> x e. RR ) |
227 |
225 226 224 219 212
|
letrd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> 1 <_ n ) |
228 |
224 227
|
logge0d |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> 0 <_ ( log ` n ) ) |
229 |
217 218 223 228
|
le2sqd |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( ( log ` x ) <_ ( log ` n ) <-> ( ( log ` x ) ^ 2 ) <_ ( ( log ` n ) ^ 2 ) ) ) |
230 |
216 229
|
mpbid |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( ( log ` x ) ^ 2 ) <_ ( ( log ` n ) ^ 2 ) ) |
231 |
|
relogcl |
|- ( x e. RR+ -> ( log ` x ) e. RR ) |
232 |
231
|
ad2antrl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. RR ) |
233 |
232
|
sqge0d |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( ( log ` x ) ^ 2 ) ) |
234 |
54
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. RR+ ) |
235 |
|
simpl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR+ ) |
236 |
|
1le1 |
|- 1 <_ 1 |
237 |
236
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ 1 ) |
238 |
|
simpr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ A ) |
239 |
9
|
rexrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR* ) |
240 |
|
pnfge |
|- ( A e. RR* -> A <_ +oo ) |
241 |
239 240
|
syl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A <_ +oo ) |
242 |
94 95 96 97 99 103 104 115 109 117 209 211 230 50 233 234 235 237 238 241 44
|
dvfsum2 |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` n ) ^ 2 ) - ( x x. ( ( ( log ` x ) ^ 2 ) + ( 2 - ( 2 x. ( log ` x ) ) ) ) ) ) ) ` 1 ) ) ) <_ ( ( log ` A ) ^ 2 ) ) |
243 |
92 242
|
eqbrtrrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) - -u 2 ) ) <_ ( ( log ` A ) ^ 2 ) ) |
244 |
24 29 12 38 243
|
letrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - 2 ) <_ ( ( log ` A ) ^ 2 ) ) |
245 |
13
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 2 e. RR ) |
246 |
22 245 12
|
lesubaddd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) - 2 ) <_ ( ( log ` A ) ^ 2 ) <-> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) <_ ( ( ( log ` A ) ^ 2 ) + 2 ) ) ) |
247 |
244 246
|
mpbid |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) <_ ( ( ( log ` A ) ^ 2 ) + 2 ) ) |