Metamath Proof Explorer

Theorem log2sumbnd

Description: Bound on the difference between sum_ n <_ A , log ^ 2 ( n ) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Assertion log2sumbnd 
|- ( ( 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 ) )

Proof

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 addlidi 
 |-  ( 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 mullidi 
 |-  ( 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 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
129 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
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 128 129 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 relogf1o 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
152 f1of 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
153 151 152 mp1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( log |` RR+ ) : RR+ --> RR )
154 153 feqmptd 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) )
155 fvres 
 |-  ( x e. RR+ -> ( ( log |` RR+ ) ` x ) = ( log ` x ) )
156 155 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) = ( x e. RR+ |-> ( log ` x ) )
157 154 156 eqtrdi 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
158 157 oveq2d 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) )
159 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
160 158 159 eqtr3di 
 |-  ( ( 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 eqtrid 
 |-  ( 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 128 129 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 eqtr3id 
 |-  ( ( ( 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 mullidd 
 |-  ( ( ( 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 ) )