Metamath Proof Explorer

Theorem pntrlog2bndlem6

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 )
pntrlog2bndlem6.1 
|- ( ph -> A e. RR )
pntrlog2bndlem6.2 
|- ( ph -> 1 <_ A )
Assertion pntrlog2bndlem6 
|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( 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 pntrlog2bndlem6.1 
 |-  ( ph -> A e. RR )
7 pntrlog2bndlem6.2 
 |-  ( ph -> 1 <_ A )
8 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
9 8 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
10 1rp 
 |-  1 e. RR+
11 10 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
12 1red 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
13 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
14 13 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
15 14 simpld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
16 12 9 15 ltled 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
17 9 11 16 rpgecld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
18 2 pntrf 
 |-  R : RR+ --> RR
19 18 ffvelrni 
 |-  ( x e. RR+ -> ( R ` x ) e. RR )
20 17 19 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
21 20 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
22 21 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
23 17 relogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
24 22 23 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
25 2re 
 |-  2 e. RR
26 25 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
27 9 15 rplogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
28 26 27 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
29 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
30 17 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 18 ffvelrni 
 |-  ( ( 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 38 39 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
41 29 40 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
42 28 41 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. RR )
43 24 42 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 ) ) ) ) e. RR )
44 43 recnd 
 |-  ( ( 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 ) ) ) ) e. CC )
45 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) e. Fin )
46 ssun2 
 |-  ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) C_ ( ( 1 ... ( |_ ` ( x / A ) ) ) u. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) )
47 1 2 3 4 5 6 7 pntrlog2bndlem6a 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( ( 1 ... ( |_ ` ( x / A ) ) ) u. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) )
48 46 47 sseqtrrid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` x ) ) )
49 48 sselda 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
50 49 40 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
51 45 50 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
52 28 51 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. RR )
53 52 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. CC )
54 9 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
55 17 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
56 44 53 54 55 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 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` 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 ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) ) )
57 24 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
58 42 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. CC )
59 57 58 53 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 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
60 28 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
61 41 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
62 51 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
63 60 61 62 subdid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) - sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
64 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` ( x / A ) ) ) e. Fin )
65 ssun1 
 |-  ( 1 ... ( |_ ` ( x / A ) ) ) C_ ( ( 1 ... ( |_ ` ( x / A ) ) ) u. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) )
66 65 47 sseqtrrid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` ( x / A ) ) ) C_ ( 1 ... ( |_ ` x ) ) )
67 66 sselda 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
68 67 40 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
69 64 68 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
70 69 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
71 10 a1i 
 |-  ( ph -> 1 e. RR+ )
72 6 71 7 rpgecld 
 |-  ( ph -> A e. RR+ )
73 72 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR+ )
74 9 73 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / A ) e. RR )
75 reflcl 
 |-  ( ( x / A ) e. RR -> ( |_ ` ( x / A ) ) e. RR )
76 74 75 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` ( x / A ) ) e. RR )
77 76 ltp1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` ( x / A ) ) < ( ( |_ ` ( x / A ) ) + 1 ) )
78 fzdisj 
 |-  ( ( |_ ` ( x / A ) ) < ( ( |_ ` ( x / A ) ) + 1 ) -> ( ( 1 ... ( |_ ` ( x / A ) ) ) i^i ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) = (/) )
79 77 78 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 1 ... ( |_ ` ( x / A ) ) ) i^i ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) = (/) )
80 40 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
81 79 47 29 80 fsumsplit 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) = ( sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) + sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
82 70 62 81 mvrraddd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) - sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
83 82 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) - sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
84 63 83 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
85 84 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 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
86 59 85 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 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
87 86 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 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
88 56 87 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 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
89 88 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 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) )
90 43 17 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 ) ) ) ) / x ) e. RR )
91 52 17 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) e. RR )
92 1 2 3 4 5 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) )
93 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
94 93 a1i 
 |-  ( ph -> ( 1 (,) +oo ) C_ RR )
95 1red 
 |-  ( ph -> 1 e. RR )
96 25 a1i 
 |-  ( ph -> 2 e. RR )
97 4 rpred 
 |-  ( ph -> B e. RR )
98 72 relogcld 
 |-  ( ph -> ( log ` A ) e. RR )
99 98 95 readdcld 
 |-  ( ph -> ( ( log ` A ) + 1 ) e. RR )
100 97 99 remulcld 
 |-  ( ph -> ( B x. ( ( log ` A ) + 1 ) ) e. RR )
101 96 100 remulcld 
 |-  ( ph -> ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) e. RR )
102 51 27 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) e. RR )
103 97 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR )
104 73 relogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` A ) e. RR )
105 104 12 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` A ) + 1 ) e. RR )
106 103 105 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( B x. ( ( log ` A ) + 1 ) ) e. RR )
107 9 106 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( B x. ( ( log ` A ) + 1 ) ) ) 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 103 9 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( B x. x ) e. RR )
112 49 31 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n e. NN )
113 112 nnrecred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
114 45 113 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) e. RR )
115 111 114 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( B x. x ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) ) e. RR )
116 27 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( log ` x ) e. RR+ )
117 50 116 rerpdivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) e. RR )
118 103 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> B e. RR )
119 9 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> x e. RR )
120 118 119 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( B x. x ) e. RR )
121 120 113 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( B x. x ) x. ( 1 / n ) ) e. RR )
122 49 38 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
123 119 112 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
124 118 123 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( B x. ( x / n ) ) e. RR )
125 49 33 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n e. RR+ )
126 125 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
127 17 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> x e. RR+ )
128 127 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( log ` x ) e. RR )
129 49 37 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
130 129 absge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( R ` ( x / n ) ) ) )
131 elfzle2 
 |-  ( n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) -> n <_ ( |_ ` x ) )
132 131 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n <_ ( |_ ` x ) )
133 112 nnzd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n e. ZZ )
134 flge 
 |-  ( ( x e. RR /\ n e. ZZ ) -> ( n <_ x <-> n <_ ( |_ ` x ) ) )
135 119 133 134 syl2anc 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( n <_ x <-> n <_ ( |_ ` x ) ) )
136 132 135 mpbird 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n <_ x )
137 125 127 logled 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( n <_ x <-> ( log ` n ) <_ ( log ` x ) ) )
138 136 137 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( log ` n ) <_ ( log ` x ) )
139 126 128 122 130 138 lemul2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) <_ ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` x ) ) )
140 50 122 116 ledivmul2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) <_ ( abs ` ( R ` ( x / n ) ) ) <-> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) <_ ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` x ) ) ) )
141 139 140 mpbird 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) <_ ( abs ` ( R ` ( x / n ) ) ) )
142 123 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
143 49 34 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
144 143 rpne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( x / n ) =/= 0 )
145 129 142 144 absdivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) )
146 17 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ x )
147 146 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> 0 <_ x )
148 119 125 147 divge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> 0 <_ ( x / n ) )
149 123 148 absidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` ( x / n ) ) = ( x / n ) )
150 149 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
151 145 150 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
152 fveq2 
 |-  ( y = ( x / n ) -> ( R ` y ) = ( R ` ( x / n ) ) )
153 id 
 |-  ( y = ( x / n ) -> y = ( x / n ) )
154 152 153 oveq12d 
 |-  ( y = ( x / n ) -> ( ( R ` y ) / y ) = ( ( R ` ( x / n ) ) / ( x / n ) ) )
155 154 fveq2d 
 |-  ( y = ( x / n ) -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) )
156 155 breq1d 
 |-  ( y = ( x / n ) -> ( ( abs ` ( ( R ` y ) / y ) ) <_ B <-> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B ) )
157 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
158 156 157 143 rspcdva 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B )
159 151 158 eqbrtrrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) <_ B )
160 122 118 143 ledivmul2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) <_ B <-> ( abs ` ( R ` ( x / n ) ) ) <_ ( B x. ( x / n ) ) ) )
161 159 160 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) <_ ( B x. ( x / n ) ) )
162 117 122 124 141 161 letrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) <_ ( B x. ( x / n ) ) )
163 118 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> B e. CC )
164 54 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> x e. CC )
165 112 nncnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n e. CC )
166 112 nnne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> n =/= 0 )
167 163 164 165 166 divassd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( B x. x ) / n ) = ( B x. ( x / n ) ) )
168 163 164 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( B x. x ) e. CC )
169 168 165 166 divrecd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( B x. x ) / n ) = ( ( B x. x ) x. ( 1 / n ) ) )
170 167 169 eqtr3d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( B x. ( x / n ) ) = ( ( B x. x ) x. ( 1 / n ) ) )
171 162 170 breqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) <_ ( ( B x. x ) x. ( 1 / n ) ) )
172 45 117 121 171 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) <_ sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( B x. x ) x. ( 1 / n ) ) )
173 23 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
174 49 80 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
175 27 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
176 45 173 174 175 fsumdivc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) = sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) )
177 103 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. CC )
178 177 54 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( B x. x ) e. CC )
179 113 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
180 45 178 179 fsummulc2 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( B x. x ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) ) = sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( B x. x ) x. ( 1 / n ) ) )
181 172 176 180 3brtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) <_ ( ( B x. x ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) ) )
182 4 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR+ )
183 182 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ B )
184 103 9 183 146 mulge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( B x. x ) )
185 32 nnrecred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
186 29 185 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
187 23 104 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) - ( log ` A ) ) e. RR )
188 23 12 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. RR )
189 67 185 syldan 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( 1 / n ) e. RR )
190 64 189 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) e. RR )
191 harmonicubnd 
 |-  ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
192 9 16 191 syl2anc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
193 17 73 relogdivd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` ( x / A ) ) = ( ( log ` x ) - ( log ` A ) ) )
194 17 73 rpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / A ) e. RR+ )
195 harmoniclbnd 
 |-  ( ( x / A ) e. RR+ -> ( log ` ( x / A ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) )
196 194 195 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` ( x / A ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) )
197 193 196 eqbrtrrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) - ( log ` A ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) )
198 186 187 188 190 192 197 le2subd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) ) <_ ( ( ( log ` x ) + 1 ) - ( ( log ` x ) - ( log ` A ) ) ) )
199 67 31 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> n e. NN )
200 199 nnrecred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( 1 / n ) e. RR )
201 64 200 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) e. RR )
202 201 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) e. CC )
203 114 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) e. CC )
204 32 nncnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
205 32 nnne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
206 204 205 reccld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
207 79 47 29 206 fsumsplit 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) = ( sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) + sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) ) )
208 202 203 207 mvrladdd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( 1 / n ) ) = sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) )
209 1cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
210 104 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` A ) e. CC )
211 173 209 210 pnncand 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) - ( ( log ` x ) - ( log ` A ) ) ) = ( 1 + ( log ` A ) ) )
212 209 210 211 comraddd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) - ( ( log ` x ) - ( log ` A ) ) ) = ( ( log ` A ) + 1 ) )
213 198 208 212 3brtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` A ) + 1 ) )
214 114 105 111 184 213 lemul2ad 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( B x. x ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) ) <_ ( ( B x. x ) x. ( ( log ` A ) + 1 ) ) )
215 105 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` A ) + 1 ) e. CC )
216 177 54 215 mulassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( B x. x ) x. ( ( log ` A ) + 1 ) ) = ( B x. ( x x. ( ( log ` A ) + 1 ) ) ) )
217 177 54 215 mul12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( B x. ( x x. ( ( log ` A ) + 1 ) ) ) = ( x x. ( B x. ( ( log ` A ) + 1 ) ) ) )
218 216 217 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( B x. x ) x. ( ( log ` A ) + 1 ) ) = ( x x. ( B x. ( ( log ` A ) + 1 ) ) ) )
219 214 218 breqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( B x. x ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( 1 / n ) ) <_ ( x x. ( B x. ( ( log ` A ) + 1 ) ) ) )
220 102 115 107 181 219 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) <_ ( x x. ( B x. ( ( log ` A ) + 1 ) ) ) )
221 102 107 26 110 220 lemul2ad 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) ) <_ ( 2 x. ( x x. ( B x. ( ( log ` A ) + 1 ) ) ) ) )
222 2cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
223 222 173 62 175 div32d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) = ( 2 x. ( sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) / ( log ` x ) ) ) )
224 210 209 addcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` A ) + 1 ) e. CC )
225 177 224 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( B x. ( ( log ` A ) + 1 ) ) e. CC )
226 54 222 225 mul12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) ) = ( 2 x. ( x x. ( B x. ( ( log ` A ) + 1 ) ) ) ) )
227 221 223 226 3brtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) <_ ( x x. ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) ) )
228 101 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) e. RR )
229 52 228 17 ledivmuld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) <_ ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) <-> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) <_ ( x x. ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) ) ) )
230 227 229 mpbird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) <_ ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) )
231 230 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) <_ ( 2 x. ( B x. ( ( log ` A ) + 1 ) ) ) )
232 94 91 95 101 231 ello1d 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) ) e. <_O(1) )
233 90 91 92 232 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 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) / x ) ) ) e. <_O(1) )
234 89 233 eqeltrrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) )