Metamath Proof Explorer

Theorem pntrlog2bndlem5

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 ) )
pntrlog2bndlem5.1 
|- ( ph -> B e. RR+ )
pntrlog2bndlem5.2 
|- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
Assertion pntrlog2bndlem5 
|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / 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 pntrlog2bndlem5.1 
 |-  ( ph -> B e. RR+ )
5 pntrlog2bndlem5.2 
 |-  ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
6 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
7 6 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
8 1rp 
 |-  1 e. RR+
9 8 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
10 1red 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
11 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
12 11 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
13 12 simpld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
14 10 7 13 ltled 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
15 7 9 14 rpgecld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
16 2 pntrf 
 |-  R : RR+ --> RR
17 16 ffvelcdmi 
 |-  ( x e. RR+ -> ( R ` x ) e. RR )
18 15 17 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
19 18 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
20 19 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
21 20 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. CC )
22 15 relogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
23 22 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
24 21 23 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
25 2cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
26 7 13 rplogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
27 26 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
28 25 23 27 divcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
29 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
30 15 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
31 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
32 31 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
33 32 nnrpd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
34 30 33 rpdivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
35 16 ffvelcdmi 
 |-  ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
36 34 35 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
37 36 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
38 37 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
39 33 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
40 1red 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
41 39 40 readdcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. RR )
42 38 41 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. RR )
43 42 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. CC )
44 29 43 fsumcl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. CC )
45 28 44 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) e. CC )
46 24 45 subcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) e. CC )
47 38 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. CC )
48 29 47 fsumcl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. CC )
49 28 48 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) e. CC )
50 7 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
51 15 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
52 46 49 50 51 divdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) / x ) = ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) )
53 20 22 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
54 53 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
55 54 45 49 subsubd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) )
56 28 44 48 subdid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) )
57 29 43 47 fsumsub 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) )
58 41 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. CC )
59 1cnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
60 47 58 59 subdid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( log ` n ) + 1 ) - 1 ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) ) )
61 39 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
62 61 59 pncand 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` n ) + 1 ) - 1 ) = ( log ` n ) )
63 62 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( log ` n ) + 1 ) - 1 ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
64 47 mulridd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) = ( abs ` ( R ` ( x / n ) ) ) )
65 64 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) )
66 60 63 65 3eqtr3rd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
67 66 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
68 57 67 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
69 68 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
70 56 69 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
71 70 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
72 55 71 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
73 72 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) / x ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
74 52 73 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
75 74 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / 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. ( log ` n ) ) ) ) / x ) ) )
76 2re 
 |-  2 e. RR
77 76 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
78 77 26 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
79 29 42 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. RR )
80 78 79 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) e. RR )
81 53 80 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) e. RR )
82 81 15 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) e. RR )
83 29 38 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. RR )
84 78 83 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) e. RR )
85 84 15 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) e. RR )
86 1red 
 |-  ( ph -> 1 e. RR )
87 1 2 3 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)
88 87 a1i 
 |-  ( ph -> ( 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) )
89 32 nnred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
90 simpl 
 |-  ( ( a e. RR /\ a e. RR+ ) -> a e. RR )
91 simpr 
 |-  ( ( a e. RR /\ a e. RR+ ) -> a e. RR+ )
92 91 relogcld 
 |-  ( ( a e. RR /\ a e. RR+ ) -> ( log ` a ) e. RR )
93 90 92 remulcld 
 |-  ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
94 0red 
 |-  ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
95 93 94 ifclda 
 |-  ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
96 3 95 fmpti 
 |-  T : RR --> RR
97 96 ffvelcdmi 
 |-  ( n e. RR -> ( T ` n ) e. RR )
98 89 97 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. RR )
99 89 40 resubcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
100 96 ffvelcdmi 
 |-  ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) e. RR )
101 99 100 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. RR )
102 98 101 resubcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
103 38 102 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
104 29 103 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
105 78 104 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) e. RR )
106 53 105 resubcld 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) e. RR )
107 106 15 rerpdivcld 
 |-  ( ( ph /\ 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. RR )
108 2rp 
 |-  2 e. RR+
109 108 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR+ )
110 109 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ 2 )
111 77 26 110 divge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 / ( log ` x ) ) )
112 37 absge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( R ` ( x / n ) ) ) )
113 33 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. RR+ )
114 113 rpcnd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. CC )
115 61 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` n ) e. CC )
116 114 115 mulcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( log ` n ) ) e. CC )
117 simpr 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 < n )
118 1re 
 |-  1 e. RR
119 113 rpred 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. RR )
120 difrp 
 |-  ( ( 1 e. RR /\ n e. RR ) -> ( 1 < n <-> ( n - 1 ) e. RR+ ) )
121 118 119 120 sylancr 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 < n <-> ( n - 1 ) e. RR+ ) )
122 117 121 mpbid 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n - 1 ) e. RR+ )
123 122 relogcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. RR )
124 123 recnd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. CC )
125 114 124 mulcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( log ` ( n - 1 ) ) ) e. CC )
126 116 125 124 subsubd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( log ` n ) ) - ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) ) = ( ( ( n x. ( log ` n ) ) - ( n x. ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) )
127 rpre 
 |-  ( n e. RR+ -> n e. RR )
128 eleq1 
 |-  ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
129 id 
 |-  ( a = n -> a = n )
130 fveq2 
 |-  ( a = n -> ( log ` a ) = ( log ` n ) )
131 129 130 oveq12d 
 |-  ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
132 128 131 ifbieq1d 
 |-  ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
133 ovex 
 |-  ( n x. ( log ` n ) ) e. _V
134 c0ex 
 |-  0 e. _V
135 133 134 ifex 
 |-  if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
136 132 3 135 fvmpt 
 |-  ( n e. RR -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
137 127 136 syl 
 |-  ( n e. RR+ -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
138 iftrue 
 |-  ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
139 137 138 eqtrd 
 |-  ( n e. RR+ -> ( T ` n ) = ( n x. ( log ` n ) ) )
140 113 139 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` n ) = ( n x. ( log ` n ) ) )
141 rpre 
 |-  ( ( n - 1 ) e. RR+ -> ( n - 1 ) e. RR )
142 eleq1 
 |-  ( a = ( n - 1 ) -> ( a e. RR+ <-> ( n - 1 ) e. RR+ ) )
143 id 
 |-  ( a = ( n - 1 ) -> a = ( n - 1 ) )
144 fveq2 
 |-  ( a = ( n - 1 ) -> ( log ` a ) = ( log ` ( n - 1 ) ) )
145 143 144 oveq12d 
 |-  ( a = ( n - 1 ) -> ( a x. ( log ` a ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
146 142 145 ifbieq1d 
 |-  ( a = ( n - 1 ) -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
147 ovex 
 |-  ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) e. _V
148 147 134 ifex 
 |-  if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) e. _V
149 146 3 148 fvmpt 
 |-  ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
150 141 149 syl 
 |-  ( ( n - 1 ) e. RR+ -> ( T ` ( n - 1 ) ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
151 iftrue 
 |-  ( ( n - 1 ) e. RR+ -> if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
152 150 151 eqtrd 
 |-  ( ( n - 1 ) e. RR+ -> ( T ` ( n - 1 ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
153 122 152 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` ( n - 1 ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
154 1cnd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. CC )
155 114 154 124 subdird 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) = ( ( n x. ( log ` ( n - 1 ) ) ) - ( 1 x. ( log ` ( n - 1 ) ) ) ) )
156 124 mullidd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 x. ( log ` ( n - 1 ) ) ) = ( log ` ( n - 1 ) ) )
157 156 oveq2d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( log ` ( n - 1 ) ) ) - ( 1 x. ( log ` ( n - 1 ) ) ) ) = ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) )
158 153 155 157 3eqtrd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` ( n - 1 ) ) = ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) )
159 140 158 oveq12d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( ( n x. ( log ` n ) ) - ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) ) )
160 114 115 124 subdid 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( n x. ( log ` n ) ) - ( n x. ( log ` ( n - 1 ) ) ) ) )
161 160 oveq1d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) = ( ( ( n x. ( log ` n ) ) - ( n x. ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) )
162 126 159 161 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) )
163 113 relogcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` n ) e. RR )
164 163 123 resubcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. RR )
165 164 recnd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. CC )
166 114 154 165 subdird 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( 1 x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) ) )
167 165 mullidd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( log ` n ) - ( log ` ( n - 1 ) ) ) )
168 167 oveq2d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( 1 x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) ) = ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) )
169 119 164 remulcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) e. RR )
170 169 recnd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) e. CC )
171 170 115 124 subsub3d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) )
172 166 168 171 3eqtrd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) )
173 114 154 npcand 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) + 1 ) = n )
174 173 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( ( n - 1 ) + 1 ) ) = ( log ` n ) )
175 174 oveq1d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` ( ( n - 1 ) + 1 ) ) - ( log ` ( n - 1 ) ) ) = ( ( log ` n ) - ( log ` ( n - 1 ) ) ) )
176 logdifbnd 
 |-  ( ( n - 1 ) e. RR+ -> ( ( log ` ( ( n - 1 ) + 1 ) ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
177 122 176 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` ( ( n - 1 ) + 1 ) ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
178 175 177 eqbrtrrd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
179 1red 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. RR )
180 164 179 122 lemuldiv2d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) <_ 1 <-> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) ) )
181 178 180 mpbird 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) <_ 1 )
182 172 181 eqbrtrrd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) <_ 1 )
183 169 123 readdcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) e. RR )
184 183 163 179 lesubadd2d 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) <_ 1 <-> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) ) )
185 182 184 mpbid 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
186 162 185 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
187 fveq2 
 |-  ( n = 1 -> ( T ` n ) = ( T ` 1 ) )
188 id 
 |-  ( a = 1 -> a = 1 )
189 188 8 eqeltrdi 
 |-  ( a = 1 -> a e. RR+ )
190 189 iftrued 
 |-  ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = ( a x. ( log ` a ) ) )
191 fveq2 
 |-  ( a = 1 -> ( log ` a ) = ( log ` 1 ) )
192 log1 
 |-  ( log ` 1 ) = 0
193 191 192 eqtrdi 
 |-  ( a = 1 -> ( log ` a ) = 0 )
194 188 193 oveq12d 
 |-  ( a = 1 -> ( a x. ( log ` a ) ) = ( 1 x. 0 ) )
195 ax-1cn 
 |-  1 e. CC
196 195 mul01i 
 |-  ( 1 x. 0 ) = 0
197 194 196 eqtrdi 
 |-  ( a = 1 -> ( a x. ( log ` a ) ) = 0 )
198 190 197 eqtrd 
 |-  ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
199 198 3 134 fvmpt 
 |-  ( 1 e. RR -> ( T ` 1 ) = 0 )
200 118 199 ax-mp 
 |-  ( T ` 1 ) = 0
201 187 200 eqtrdi 
 |-  ( n = 1 -> ( T ` n ) = 0 )
202 oveq1 
 |-  ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
203 1m1e0 
 |-  ( 1 - 1 ) = 0
204 202 203 eqtrdi 
 |-  ( n = 1 -> ( n - 1 ) = 0 )
205 204 fveq2d 
 |-  ( n = 1 -> ( T ` ( n - 1 ) ) = ( T ` 0 ) )
206 0re 
 |-  0 e. RR
207 rpne0 
 |-  ( a e. RR+ -> a =/= 0 )
208 207 necon2bi 
 |-  ( a = 0 -> -. a e. RR+ )
209 208 iffalsed 
 |-  ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
210 209 3 134 fvmpt 
 |-  ( 0 e. RR -> ( T ` 0 ) = 0 )
211 206 210 ax-mp 
 |-  ( T ` 0 ) = 0
212 205 211 eqtrdi 
 |-  ( n = 1 -> ( T ` ( n - 1 ) ) = 0 )
213 201 212 oveq12d 
 |-  ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( 0 - 0 ) )
214 0m0e0 
 |-  ( 0 - 0 ) = 0
215 213 214 eqtrdi 
 |-  ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
216 215 eqcoms 
 |-  ( 1 = n -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
217 216 adantl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
218 0red 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 e. RR )
219 32 nnge1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
220 89 219 logge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( log ` n ) )
221 39 lep1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) <_ ( ( log ` n ) + 1 ) )
222 218 39 41 220 221 letrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( log ` n ) + 1 ) )
223 222 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> 0 <_ ( ( log ` n ) + 1 ) )
224 217 223 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
225 elfzle1 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> 1 <_ n )
226 225 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
227 40 89 leloed 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 <_ n <-> ( 1 < n \/ 1 = n ) ) )
228 226 227 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 < n \/ 1 = n ) )
229 186 224 228 mpjaodan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
230 102 41 38 112 229 lemul2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) <_ ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) )
231 29 103 42 230 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) )
232 104 79 78 111 231 lemul2ad 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) <_ ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) )
233 105 80 53 232 lesub2dd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) <_ ( ( ( 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 ) ) ) ) ) ) )
234 81 106 15 233 lediv1dd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / 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 ) )
235 234 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / 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 ) )
236 86 88 107 82 235 lo1le 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) ) e. <_O(1) )
237 108 a1i 
 |-  ( ph -> 2 e. RR+ )
238 237 4 rpmulcld 
 |-  ( ph -> ( 2 x. B ) e. RR+ )
239 238 rpred 
 |-  ( ph -> ( 2 x. B ) e. RR )
240 239 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR )
241 10 26 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
242 10 241 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. RR )
243 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
244 lo1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ ( 2 x. B ) e. RR ) -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. B ) ) e. <_O(1) )
245 243 239 244 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. B ) ) e. <_O(1) )
246 lo1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. RR ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
247 243 86 246 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
248 divlogrlim 
 |-  ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0
249 rlimo1 
 |-  ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
250 248 249 mp1i 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
251 241 250 o1lo1d 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. <_O(1) )
252 10 241 247 251 lo1add 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 + ( 1 / ( log ` x ) ) ) ) e. <_O(1) )
253 238 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR+ )
254 253 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 x. B ) )
255 240 242 245 252 254 lo1mul 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. <_O(1) )
256 240 242 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. RR )
257 83 15 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
258 22 10 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. RR )
259 4 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR+ )
260 259 rpred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR )
261 258 260 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) x. B ) e. RR )
262 32 nnrecred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
263 29 262 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
264 263 260 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) e. RR )
265 38 30 rerpdivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
266 260 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. RR )
267 262 266 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / n ) x. B ) e. RR )
268 34 rpcnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
269 34 rpne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) =/= 0 )
270 37 268 269 absdivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) )
271 7 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
272 271 32 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
273 34 rpge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( x / n ) )
274 272 273 absidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( x / n ) ) = ( x / n ) )
275 274 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
276 270 275 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
277 50 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
278 89 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
279 51 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
280 32 nnne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
281 47 277 278 279 280 divdiv2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. n ) / x ) )
282 47 278 277 279 div23d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. n ) / x ) = ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) )
283 276 281 282 3eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) )
284 fveq2 
 |-  ( y = ( x / n ) -> ( R ` y ) = ( R ` ( x / n ) ) )
285 id 
 |-  ( y = ( x / n ) -> y = ( x / n ) )
286 284 285 oveq12d 
 |-  ( y = ( x / n ) -> ( ( R ` y ) / y ) = ( ( R ` ( x / n ) ) / ( x / n ) ) )
287 286 fveq2d 
 |-  ( y = ( x / n ) -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) )
288 287 breq1d 
 |-  ( y = ( x / n ) -> ( ( abs ` ( ( R ` y ) / y ) ) <_ B <-> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B ) )
289 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
290 288 289 34 rspcdva 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B )
291 283 290 eqbrtrrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) <_ B )
292 265 266 33 lemuldivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) <_ B <-> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( B / n ) ) )
293 291 292 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( B / n ) )
294 266 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. CC )
295 294 278 280 divrec2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( B / n ) = ( ( 1 / n ) x. B ) )
296 293 295 breqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( ( 1 / n ) x. B ) )
297 29 265 267 296 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 / n ) x. B ) )
298 29 50 47 51 fsumdivc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) / x ) )
299 259 rpcnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. CC )
300 262 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
301 29 299 300 fsummulc1 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 / n ) x. B ) )
302 297 298 301 3brtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) )
303 259 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ B )
304 harmonicubnd 
 |-  ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
305 7 14 304 syl2anc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
306 263 258 260 303 305 lemul1ad 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) <_ ( ( ( log ` x ) + 1 ) x. B ) )
307 257 264 261 302 306 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( ( ( log ` x ) + 1 ) x. B ) )
308 257 261 78 111 307 lemul2ad 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) ) <_ ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
309 28 48 50 51 divassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) = ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) ) )
310 242 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. CC )
311 25 299 310 mul32d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) x. B ) )
312 1cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
313 23 312 23 27 divdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) / ( log ` x ) ) = ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) )
314 23 27 dividd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
315 314 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) = ( 1 + ( 1 / ( log ` x ) ) ) )
316 313 315 eqtr2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) = ( ( ( log ` x ) + 1 ) / ( log ` x ) ) )
317 316 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
318 23 312 addcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
319 25 23 318 27 div32d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
320 317 319 eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) )
321 320 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) x. B ) = ( ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) x. B ) )
322 28 318 299 mulassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) x. B ) = ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
323 311 321 322 3eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
324 308 309 323 3brtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) <_ ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
325 324 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) <_ ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
326 86 255 256 85 325 lo1le 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) e. <_O(1) )
327 82 85 236 326 lo1add 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) ) e. <_O(1) )
328 75 327 eqeltrrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) )