Metamath Proof Explorer

Theorem pntrlog2bndlem4

Description: Lemma for pntrlog2bnd . Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypotheses pntsval.1 
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
pntrlog2bnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntrlog2bnd.t 
|- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
Assertion pntrlog2bndlem4 
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) ) e. <_O(1)

Proof

Step Hyp Ref Expression
1 pntsval.1 
 |-  S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
2 pntrlog2bnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
3 pntrlog2bnd.t 
 |-  T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
4 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
5 4 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
6 1rp 
 |-  1 e. RR+
7 6 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
8 1red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
9 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
10 9 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
11 10 simpld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
12 8 5 11 ltled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
13 5 7 12 rpgecld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
14 13 rprege0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x e. RR /\ 0 <_ x ) )
15 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
16 14 15 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. NN0 )
17 nn0p1nn 
 |-  ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
18 16 17 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
19 18 nnrpd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. RR+ )
20 13 19 rpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ )
21 2 pntrval 
 |-  ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
22 20 21 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
23 5 18 nndivred 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR )
24 2re 
 |-  2 e. RR
25 24 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
26 flltp1 
 |-  ( x e. RR -> x < ( ( |_ ` x ) + 1 ) )
27 5 26 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( |_ ` x ) + 1 ) )
28 18 nncnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. CC )
29 28 mulridd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. 1 ) = ( ( |_ ` x ) + 1 ) )
30 27 29 breqtrrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) )
31 5 8 19 ltdivmuld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) < 1 <-> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) ) )
32 30 31 mpbird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 1 )
33 1lt2 
 |-  1 < 2
34 33 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < 2 )
35 23 8 25 32 34 lttrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 2 )
36 chpeq0 
 |-  ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR -> ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
37 23 36 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
38 35 37 mpbird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 )
39 38 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
40 22 39 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
41 40 fveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
42 0red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 e. RR )
43 20 rpge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( x / ( ( |_ ` x ) + 1 ) ) )
44 42 23 43 abssuble0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) )
45 23 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. CC )
46 45 subid1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) = ( x / ( ( |_ ` x ) + 1 ) ) )
47 41 44 46 3eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
48 16 nn0red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. RR )
49 1 pntsval2 
 |-  ( ( |_ ` x ) e. RR -> ( S ` ( |_ ` x ) ) = sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
50 48 49 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( |_ ` x ) ) = sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
51 16 nn0cnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. CC )
52 1cnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
53 51 52 pncand 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
54 53 fveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` ( |_ ` x ) ) )
55 1 pntsval2 
 |-  ( x e. RR -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
56 5 55 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
57 flidm 
 |-  ( x e. RR -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
58 5 57 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
59 58 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` ( |_ ` x ) ) ) = ( 1 ... ( |_ ` x ) ) )
60 59 sumeq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
61 56 60 eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
62 50 54 61 3eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` x ) )
63 53 fveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( T ` ( |_ ` x ) ) )
64 63 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( 2 x. ( T ` ( |_ ` x ) ) ) )
65 62 64 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) = ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) )
66 47 65 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) )
67 5 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
68 67 div1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / 1 ) = x )
69 68 fveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) = ( R ` x ) )
70 2 pntrf 
 |-  R : RR+ --> RR
71 70 ffvelcdmi 
 |-  ( x e. RR+ -> ( R ` x ) e. RR )
72 13 71 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
73 69 72 eqeltrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. RR )
74 73 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. CC )
75 74 abscld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. RR )
76 75 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. CC )
77 76 mul01d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) = 0 )
78 66 77 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) = ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - 0 ) )
79 1 pntsf 
 |-  S : RR --> RR
80 79 ffvelcdmi 
 |-  ( x e. RR -> ( S ` x ) e. RR )
81 5 80 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) e. RR )
82 relogcl 
 |-  ( a e. RR+ -> ( log ` a ) e. RR )
83 remulcl 
 |-  ( ( a e. RR /\ ( log ` a ) e. RR ) -> ( a x. ( log ` a ) ) e. RR )
84 82 83 sylan2 
 |-  ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
85 0red 
 |-  ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
86 84 85 ifclda 
 |-  ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
87 3 86 fmpti 
 |-  T : RR --> RR
88 87 ffvelcdmi 
 |-  ( ( |_ ` x ) e. RR -> ( T ` ( |_ ` x ) ) e. RR )
89 48 88 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( |_ ` x ) ) e. RR )
90 25 89 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( |_ ` x ) ) ) e. RR )
91 81 90 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) e. RR )
92 23 91 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. RR )
93 92 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. CC )
94 93 subid1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - 0 ) = ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) )
95 78 94 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) )
96 5 flcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. ZZ )
97 fzval3 
 |-  ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
98 96 97 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
99 98 eqcomd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
100 13 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
101 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
102 101 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
103 102 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
104 100 103 rpdivcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
105 70 ffvelcdmi 
 |-  ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
106 104 105 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
107 106 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
108 107 abscld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
109 108 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. CC )
110 6 a1i 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR+ )
111 103 110 rpaddcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. RR+ )
112 100 111 rpdivcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR+ )
113 70 ffvelcdmi 
 |-  ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
114 112 113 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
115 114 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. CC )
116 115 abscld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. RR )
117 116 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. CC )
118 109 117 negsubdi2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) = ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) )
119 118 eqcomd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) )
120 102 nncnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
121 1cnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
122 120 121 pncand 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = n )
123 122 fveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( ( n + 1 ) - 1 ) ) = ( S ` n ) )
124 122 fveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( T ` n ) )
125 rpre 
 |-  ( n e. RR+ -> n e. RR )
126 eleq1 
 |-  ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
127 id 
 |-  ( a = n -> a = n )
128 fveq2 
 |-  ( a = n -> ( log ` a ) = ( log ` n ) )
129 127 128 oveq12d 
 |-  ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
130 126 129 ifbieq1d 
 |-  ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
131 ovex 
 |-  ( n x. ( log ` n ) ) e. _V
132 c0ex 
 |-  0 e. _V
133 131 132 ifex 
 |-  if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
134 130 3 133 fvmpt 
 |-  ( n e. RR -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
135 125 134 syl 
 |-  ( n e. RR+ -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
136 iftrue 
 |-  ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
137 135 136 eqtrd 
 |-  ( n e. RR+ -> ( T ` n ) = ( n x. ( log ` n ) ) )
138 103 137 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) = ( n x. ( log ` n ) ) )
139 124 138 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( n x. ( log ` n ) ) )
140 139 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) = ( 2 x. ( n x. ( log ` n ) ) ) )
141 123 140 oveq12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) = ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) )
142 119 141 oveq12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = ( -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
143 108 116 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. RR )
144 143 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. CC )
145 102 nnred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
146 79 ffvelcdmi 
 |-  ( n e. RR -> ( S ` n ) e. RR )
147 145 146 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. RR )
148 24 a1i 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. RR )
149 103 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
150 145 149 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( log ` n ) ) e. RR )
151 148 150 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( n x. ( log ` n ) ) ) e. RR )
152 147 151 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. RR )
153 152 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. CC )
154 144 153 mulneg1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) = -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
155 142 154 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
156 99 155 sumeq12rdv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
157 fzfid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
158 143 152 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. RR )
159 158 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. CC )
160 157 159 fsumneg 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) = -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
161 156 160 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
162 95 161 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) ) = ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) )
163 oveq2 
 |-  ( m = n -> ( x / m ) = ( x / n ) )
164 163 fveq2d 
 |-  ( m = n -> ( R ` ( x / m ) ) = ( R ` ( x / n ) ) )
165 164 fveq2d 
 |-  ( m = n -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / n ) ) ) )
166 fvoveq1 
 |-  ( m = n -> ( S ` ( m - 1 ) ) = ( S ` ( n - 1 ) ) )
167 fvoveq1 
 |-  ( m = n -> ( T ` ( m - 1 ) ) = ( T ` ( n - 1 ) ) )
168 167 oveq2d 
 |-  ( m = n -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( n - 1 ) ) ) )
169 166 168 oveq12d 
 |-  ( m = n -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) )
170 165 169 jca 
 |-  ( m = n -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / n ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
171 oveq2 
 |-  ( m = ( n + 1 ) -> ( x / m ) = ( x / ( n + 1 ) ) )
172 171 fveq2d 
 |-  ( m = ( n + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( n + 1 ) ) ) )
173 172 fveq2d 
 |-  ( m = ( n + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) )
174 fvoveq1 
 |-  ( m = ( n + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( n + 1 ) - 1 ) ) )
175 fvoveq1 
 |-  ( m = ( n + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( n + 1 ) - 1 ) ) )
176 175 oveq2d 
 |-  ( m = ( n + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) )
177 174 176 oveq12d 
 |-  ( m = ( n + 1 ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) )
178 173 177 jca 
 |-  ( m = ( n + 1 ) -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) )
179 oveq2 
 |-  ( m = 1 -> ( x / m ) = ( x / 1 ) )
180 179 fveq2d 
 |-  ( m = 1 -> ( R ` ( x / m ) ) = ( R ` ( x / 1 ) ) )
181 180 fveq2d 
 |-  ( m = 1 -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) )
182 oveq1 
 |-  ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
183 1m1e0 
 |-  ( 1 - 1 ) = 0
184 182 183 eqtrdi 
 |-  ( m = 1 -> ( m - 1 ) = 0 )
185 184 fveq2d 
 |-  ( m = 1 -> ( S ` ( m - 1 ) ) = ( S ` 0 ) )
186 0re 
 |-  0 e. RR
187 fveq2 
 |-  ( a = 0 -> ( |_ ` a ) = ( |_ ` 0 ) )
188 0z 
 |-  0 e. ZZ
189 flid 
 |-  ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
190 188 189 ax-mp 
 |-  ( |_ ` 0 ) = 0
191 187 190 eqtrdi 
 |-  ( a = 0 -> ( |_ ` a ) = 0 )
192 191 oveq2d 
 |-  ( a = 0 -> ( 1 ... ( |_ ` a ) ) = ( 1 ... 0 ) )
193 fz10 
 |-  ( 1 ... 0 ) = (/)
194 192 193 eqtrdi 
 |-  ( a = 0 -> ( 1 ... ( |_ ` a ) ) = (/) )
195 194 sumeq1d 
 |-  ( a = 0 -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) = sum_ i e. (/) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
196 sum0 
 |-  sum_ i e. (/) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) = 0
197 195 196 eqtrdi 
 |-  ( a = 0 -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) = 0 )
198 197 1 132 fvmpt 
 |-  ( 0 e. RR -> ( S ` 0 ) = 0 )
199 186 198 ax-mp 
 |-  ( S ` 0 ) = 0
200 185 199 eqtrdi 
 |-  ( m = 1 -> ( S ` ( m - 1 ) ) = 0 )
201 184 fveq2d 
 |-  ( m = 1 -> ( T ` ( m - 1 ) ) = ( T ` 0 ) )
202 rpne0 
 |-  ( a e. RR+ -> a =/= 0 )
203 202 necon2bi 
 |-  ( a = 0 -> -. a e. RR+ )
204 203 iffalsed 
 |-  ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
205 204 3 132 fvmpt 
 |-  ( 0 e. RR -> ( T ` 0 ) = 0 )
206 186 205 ax-mp 
 |-  ( T ` 0 ) = 0
207 201 206 eqtrdi 
 |-  ( m = 1 -> ( T ` ( m - 1 ) ) = 0 )
208 207 oveq2d 
 |-  ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. 0 ) )
209 2t0e0 
 |-  ( 2 x. 0 ) = 0
210 208 209 eqtrdi 
 |-  ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = 0 )
211 200 210 oveq12d 
 |-  ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( 0 - 0 ) )
212 0m0e0 
 |-  ( 0 - 0 ) = 0
213 211 212 eqtrdi 
 |-  ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 )
214 181 213 jca 
 |-  ( m = 1 -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 ) )
215 oveq2 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( x / m ) = ( x / ( ( |_ ` x ) + 1 ) ) )
216 215 fveq2d 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) )
217 216 fveq2d 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
218 fvoveq1 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
219 fvoveq1 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
220 219 oveq2d 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) )
221 218 220 oveq12d 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) )
222 217 221 jca 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) )
223 nnuz 
 |-  NN = ( ZZ>= ` 1 )
224 18 223 eleqtrdi 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
225 13 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> x e. RR+ )
226 elfznn 
 |-  ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
227 226 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
228 227 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR+ )
229 225 228 rpdivcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( x / m ) e. RR+ )
230 70 ffvelcdmi 
 |-  ( ( x / m ) e. RR+ -> ( R ` ( x / m ) ) e. RR )
231 229 230 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. RR )
232 231 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. CC )
233 232 abscld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. RR )
234 233 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. CC )
235 227 nnred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR )
236 1red 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 1 e. RR )
237 235 236 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( m - 1 ) e. RR )
238 79 ffvelcdmi 
 |-  ( ( m - 1 ) e. RR -> ( S ` ( m - 1 ) ) e. RR )
239 237 238 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( S ` ( m - 1 ) ) e. RR )
240 24 a1i 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 2 e. RR )
241 87 ffvelcdmi 
 |-  ( ( m - 1 ) e. RR -> ( T ` ( m - 1 ) ) e. RR )
242 237 241 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( T ` ( m - 1 ) ) e. RR )
243 240 242 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( 2 x. ( T ` ( m - 1 ) ) ) e. RR )
244 239 243 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. RR )
245 244 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. CC )
246 170 178 214 222 224 234 245 fsumparts 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) ) = ( ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) ) )
247 147 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. CC )
248 87 ffvelcdmi 
 |-  ( n e. RR -> ( T ` n ) e. RR )
249 145 248 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. RR )
250 148 249 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. RR )
251 250 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. CC )
252 1red 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
253 145 252 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
254 79 ffvelcdmi 
 |-  ( ( n - 1 ) e. RR -> ( S ` ( n - 1 ) ) e. RR )
255 253 254 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. RR )
256 255 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. CC )
257 87 ffvelcdmi 
 |-  ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) e. RR )
258 253 257 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. RR )
259 148 258 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. RR )
260 259 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. CC )
261 247 251 256 260 sub4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( 2 x. ( T ` n ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( 2 x. ( T ` n ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
262 124 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) = ( 2 x. ( T ` n ) ) )
263 123 262 oveq12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) = ( ( S ` n ) - ( 2 x. ( T ` n ) ) ) )
264 263 oveq1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( 2 x. ( T ` n ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
265 2cnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
266 249 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. CC )
267 258 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. CC )
268 265 266 267 subdid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) = ( ( 2 x. ( T ` n ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) )
269 268 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( 2 x. ( T ` n ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
270 261 264 269 3eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
271 270 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
272 99 271 sumeq12rdv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
273 246 272 eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
274 157 159 fsumcl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. CC )
275 93 274 subnegd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) = ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) )
276 162 273 275 3eqtr3rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
277 13 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
278 277 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
279 67 278 mulcomd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) = ( ( log ` x ) x. x ) )
280 276 279 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( ( log ` x ) x. x ) ) )
281 147 255 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. RR )
282 249 258 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
283 148 282 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
284 281 283 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) e. RR )
285 108 284 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. RR )
286 157 285 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. RR )
287 286 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. CC )
288 5 11 rplogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
289 288 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
290 13 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
291 287 278 67 289 290 divdiv1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( ( log ` x ) x. x ) ) )
292 280 291 eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) )
293 292 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) ) )
294 72 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
295 294 abscld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
296 295 277 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
297 108 281 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
298 157 297 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
299 298 288 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) e. RR )
300 296 299 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) e. RR )
301 300 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) e. CC )
302 287 278 289 divcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) e. CC )
303 301 302 67 290 divdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) / x ) = ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) ) )
304 296 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
305 299 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) e. CC )
306 304 305 302 subsubd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) )
307 2cnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
308 266 267 subcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. CC )
309 109 308 mulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
310 157 307 309 fsummulc2 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
311 281 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. CC )
312 265 308 mulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
313 311 312 nncand 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) = ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) )
314 313 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
315 284 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) e. CC )
316 109 311 315 subdid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) )
317 109 265 308 mul12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) = ( 2 x. ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
318 314 316 317 3eqtr3d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) = ( 2 x. ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
319 318 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
320 297 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. CC )
321 285 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. CC )
322 157 320 321 fsumsub 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) )
323 310 319 322 3eqtr2rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) = ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
324 323 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) / ( log ` x ) ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) / ( log ` x ) ) )
325 298 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. CC )
326 325 287 278 289 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) )
327 108 282 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
328 157 327 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
329 328 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
330 307 329 278 289 div23d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) / ( log ` x ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
331 324 326 330 3eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
332 331 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
333 306 332 eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
334 333 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) / x ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) )
335 293 303 334 3eqtr2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) )
336 335 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) ) )
337 300 13 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) e. RR )
338 157 158 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. RR )
339 92 338 readdcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) e. RR )
340 13 288 rpmulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
341 339 340 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
342 1 2 pntrlog2bndlem1 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) ) e. <_O(1)
343 342 a1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) ) e. <_O(1) )
344 340 rpcnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
345 340 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) =/= 0 )
346 93 274 344 345 divdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
347 91 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) e. CC )
348 45 347 344 345 divassd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
349 348 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
350 346 349 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
351 350 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) )
352 91 340 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
353 23 352 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. RR )
354 338 340 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
355 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
356 355 a1i 
 |-  ( T. -> ( 1 (,) +oo ) C_ RR )
357 1red 
 |-  ( T. -> 1 e. RR )
358 23 8 32 ltled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) <_ 1 )
359 358 adantrr 
 |-  ( ( T. /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) <_ 1 )
360 356 23 357 357 359 ello1d 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( x / ( ( |_ ` x ) + 1 ) ) ) e. <_O(1) )
361 81 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) e. CC )
362 90 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( |_ ` x ) ) ) e. CC )
363 361 362 344 345 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) = ( ( ( S ` x ) / ( x x. ( log ` x ) ) ) - ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) ) )
364 363 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) / ( x x. ( log ` x ) ) ) - ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) ) ) )
365 81 340 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) / ( x x. ( log ` x ) ) ) e. RR )
366 90 340 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
367 2cnd 
 |-  ( T. -> 2 e. CC )
368 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 2 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
369 355 367 368 sylancr 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
370 365 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) / ( x x. ( log ` x ) ) ) e. CC )
371 81 13 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) / x ) e. RR )
372 371 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) / x ) e. CC )
373 307 278 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( log ` x ) ) e. CC )
374 372 373 278 289 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) / ( log ` x ) ) = ( ( ( ( S ` x ) / x ) / ( log ` x ) ) - ( ( 2 x. ( log ` x ) ) / ( log ` x ) ) ) )
375 25 277 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( log ` x ) ) e. RR )
376 371 375 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) e. RR )
377 376 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) e. CC )
378 377 278 289 divrecd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) / ( log ` x ) ) = ( ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) x. ( 1 / ( log ` x ) ) ) )
379 361 67 278 290 289 divdiv1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( S ` x ) / x ) / ( log ` x ) ) = ( ( S ` x ) / ( x x. ( log ` x ) ) ) )
380 307 278 289 divcan4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( log ` x ) ) / ( log ` x ) ) = 2 )
381 379 380 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( S ` x ) / x ) / ( log ` x ) ) - ( ( 2 x. ( log ` x ) ) / ( log ` x ) ) ) = ( ( ( S ` x ) / ( x x. ( log ` x ) ) ) - 2 ) )
382 374 378 381 3eqtr3rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( S ` x ) / ( x x. ( log ` x ) ) ) - 2 ) = ( ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) x. ( 1 / ( log ` x ) ) ) )
383 382 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) / ( x x. ( log ` x ) ) ) - 2 ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) x. ( 1 / ( log ` x ) ) ) ) )
384 8 288 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
385 13 ex 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
386 385 ssrdv 
 |-  ( T. -> ( 1 (,) +oo ) C_ RR+ )
387 1 selbergs 
 |-  ( x e. RR+ |-> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
388 387 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
389 386 388 o1res2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
390 divlogrlim 
 |-  ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0
391 rlimo1 
 |-  ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
392 390 391 mp1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
393 376 384 389 392 o1mul2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
394 383 393 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) / ( x x. ( log ` x ) ) ) - 2 ) ) e. O(1) )
395 370 307 394 o1dif 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( S ` x ) / ( x x. ( log ` x ) ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) ) )
396 369 395 mpbird 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( S ` x ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
397 24 a1i 
 |-  ( T. -> 2 e. RR )
398 5 277 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR )
399 2rp 
 |-  2 e. RR+
400 399 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR+ )
401 400 rpge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ 2 )
402 flge1nn 
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
403 5 12 402 syl2anc 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. NN )
404 403 nnrpd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. RR+ )
405 rpre 
 |-  ( ( |_ ` x ) e. RR+ -> ( |_ ` x ) e. RR )
406 eleq1 
 |-  ( a = ( |_ ` x ) -> ( a e. RR+ <-> ( |_ ` x ) e. RR+ ) )
407 id 
 |-  ( a = ( |_ ` x ) -> a = ( |_ ` x ) )
408 fveq2 
 |-  ( a = ( |_ ` x ) -> ( log ` a ) = ( log ` ( |_ ` x ) ) )
409 407 408 oveq12d 
 |-  ( a = ( |_ ` x ) -> ( a x. ( log ` a ) ) = ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) )
410 406 409 ifbieq1d 
 |-  ( a = ( |_ ` x ) -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( ( |_ ` x ) e. RR+ , ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) , 0 ) )
411 ovex 
 |-  ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) e. _V
412 411 132 ifex 
 |-  if ( ( |_ ` x ) e. RR+ , ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) , 0 ) e. _V
413 410 3 412 fvmpt 
 |-  ( ( |_ ` x ) e. RR -> ( T ` ( |_ ` x ) ) = if ( ( |_ ` x ) e. RR+ , ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) , 0 ) )
414 405 413 syl 
 |-  ( ( |_ ` x ) e. RR+ -> ( T ` ( |_ ` x ) ) = if ( ( |_ ` x ) e. RR+ , ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) , 0 ) )
415 iftrue 
 |-  ( ( |_ ` x ) e. RR+ -> if ( ( |_ ` x ) e. RR+ , ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) , 0 ) = ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) )
416 414 415 eqtrd 
 |-  ( ( |_ ` x ) e. RR+ -> ( T ` ( |_ ` x ) ) = ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) )
417 404 416 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( |_ ` x ) ) = ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) )
418 404 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` ( |_ ` x ) ) e. RR )
419 16 nn0ge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( |_ ` x ) )
420 403 nnge1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ ( |_ ` x ) )
421 48 420 logge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( log ` ( |_ ` x ) ) )
422 flle 
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
423 5 422 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) <_ x )
424 404 13 logled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) <_ x <-> ( log ` ( |_ ` x ) ) <_ ( log ` x ) ) )
425 423 424 mpbid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` ( |_ ` x ) ) <_ ( log ` x ) )
426 48 5 418 277 419 421 423 425 lemul12ad 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) <_ ( x x. ( log ` x ) ) )
427 417 426 eqbrtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( |_ ` x ) ) <_ ( x x. ( log ` x ) ) )
428 89 398 25 401 427 lemul2ad 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( |_ ` x ) ) ) <_ ( 2 x. ( x x. ( log ` x ) ) ) )
429 90 25 340 ledivmul2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) <_ 2 <-> ( 2 x. ( T ` ( |_ ` x ) ) ) <_ ( 2 x. ( x x. ( log ` x ) ) ) ) )
430 428 429 mpbird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) <_ 2 )
431 430 adantrr 
 |-  ( ( T. /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) <_ 2 )
432 356 366 357 397 431 ello1d 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) ) e. <_O(1) )
433 0red 
 |-  ( T. -> 0 e. RR )
434 48 418 419 421 mulge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( ( |_ ` x ) x. ( log ` ( |_ ` x ) ) ) )
435 434 417 breqtrrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( T ` ( |_ ` x ) ) )
436 25 89 401 435 mulge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 x. ( T ` ( |_ ` x ) ) ) )
437 90 340 436 divge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) )
438 366 433 437 o1lo12 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) ) e. <_O(1) ) )
439 432 438 mpbird 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
440 365 366 396 439 o1sub2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) / ( x x. ( log ` x ) ) ) - ( ( 2 x. ( T ` ( |_ ` x ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. O(1) )
441 364 440 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
442 352 441 o1lo1d 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. <_O(1) )
443 23 352 360 442 43 lo1mul 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. <_O(1) )
444 1 selbergsb 
 |-  E. c e. RR+ A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c
445 simpl 
 |-  ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c ) -> c e. RR+ )
446 simpr 
 |-  ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c )
447 1 2 445 446 pntrlog2bndlem3 
 |-  ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c ) -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
448 447 rexlimiva 
 |-  ( E. c e. RR+ A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
449 444 448 mp1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
450 354 449 o1lo1d 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. <_O(1) )
451 353 354 443 450 lo1add 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) / ( x x. ( log ` x ) ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. <_O(1) )
452 351 451 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. <_O(1) )
453 337 341 343 452 lo1add 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. <_O(1) )
454 336 453 eqeltrrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) ) e. <_O(1) )
455 454 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) ) e. <_O(1)