Metamath Proof Explorer

Theorem selberg4lem1

Description: Lemma for selberg4 . Equation 10.4.20 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses selberg4lem1.1 
|- ( ph -> A e. RR+ )
selberg4lem1.2 
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
Assertion selberg4lem1 
|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 selberg4lem1.1 
 |-  ( ph -> A e. RR+ )
2 selberg4lem1.2 
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
3 2cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
4 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
5 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
6 5 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
7 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
8 6 7 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
9 8 6 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
10 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
11 10 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
12 1rp 
 |-  1 e. RR+
13 12 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
14 1red 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
15 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
16 15 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
17 16 simpld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
18 14 11 17 ltled 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
19 11 13 18 rpgecld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
20 19 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
21 6 nnrpd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
22 20 21 rpdivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
23 22 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
24 9 23 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
25 4 24 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
26 11 17 rplogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
27 25 26 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. RR )
28 27 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
29 19 relogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
30 29 rehalfcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. RR )
31 30 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
32 3 28 31 subdid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) )
33 29 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
34 2ne0 
 |-  2 =/= 0
35 34 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
36 33 3 35 divcan2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( log ` x ) / 2 ) ) = ( log ` x ) )
37 36 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) )
38 32 37 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) )
39 38 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) )
40 2re 
 |-  2 e. RR
41 40 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
42 27 30 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. RR )
43 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
44 2cn 
 |-  2 e. CC
45 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 2 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
46 43 44 45 mp2an 
 |-  ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1)
47 46 a1i 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
48 vmalogdivsum2 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)
49 48 a1i 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
50 41 42 47 49 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O(1) )
51 39 50 eqeltrrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) )
52 fzfid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
53 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
54 53 adantl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
55 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
56 54 55 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` m ) e. RR )
57 54 nnrpd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. RR+ )
58 57 relogcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` m ) e. RR )
59 11 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
60 59 6 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
61 60 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( x / n ) e. RR )
62 61 54 nndivred 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) / m ) e. RR )
63 chpcl 
 |-  ( ( ( x / n ) / m ) e. RR -> ( psi ` ( ( x / n ) / m ) ) e. RR )
64 62 63 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( psi ` ( ( x / n ) / m ) ) e. RR )
65 58 64 readdcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) e. RR )
66 56 65 remulcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) e. RR )
67 52 66 fsumrecl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) e. RR )
68 8 67 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) e. RR )
69 4 68 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) e. RR )
70 19 26 rpmulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
71 69 70 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
72 71 29 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) e. RR )
73 72 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) e. CC )
74 25 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
75 26 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
76 74 33 75 divcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
77 3 76 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) e. CC )
78 77 33 subcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) e. CC )
79 71 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
80 79 77 33 nnncan2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) - ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) ) )
81 69 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) e. CC )
82 11 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
83 19 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
84 81 82 33 83 75 divdiv1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
85 3 74 33 75 divassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
86 84 85 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) - ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) ) )
87 69 19 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) e. RR )
88 87 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) e. CC )
89 3 74 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
90 88 89 33 75 divsubdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) / ( log ` x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) - ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) )
91 83 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
92 68 59 91 redivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) e. RR )
93 92 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) e. CC )
94 40 a1i 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. RR )
95 94 24 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. RR )
96 95 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
97 4 93 96 fsumsub 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
98 8 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
99 67 59 91 redivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) e. RR )
100 99 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) e. CC )
101 2cnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
102 23 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
103 6 nncnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
104 6 nnne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
105 102 103 104 divcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / n ) e. CC )
106 101 105 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( log ` ( x / n ) ) / n ) ) e. CC )
107 98 100 106 subdid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) = ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) ) - ( ( Lam ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) )
108 67 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) e. CC )
109 82 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
110 98 108 109 91 divassd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) = ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) ) )
111 98 103 102 104 div32d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) = ( ( Lam ` n ) x. ( ( log ` ( x / n ) ) / n ) ) )
112 111 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( 2 x. ( ( Lam ` n ) x. ( ( log ` ( x / n ) ) / n ) ) ) )
113 101 98 105 mul12d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( Lam ` n ) x. ( ( log ` ( x / n ) ) / n ) ) ) = ( ( Lam ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) )
114 112 113 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( ( Lam ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) )
115 110 114 oveq12d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) ) - ( ( Lam ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) )
116 107 115 eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) = ( ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
117 116 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
118 68 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) e. CC )
119 4 82 118 83 fsumdivc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) )
120 24 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
121 4 3 120 fsummulc2 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
122 119 121 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
123 97 117 122 3eqtr4rd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) )
124 123 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) )
125 90 124 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) - ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) )
126 80 86 125 3eqtr2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) - ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) )
127 126 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) - ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) ) )
128 1red 
 |-  ( ph -> 1 e. RR )
129 1 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR+ )
130 129 rpred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR )
131 4 9 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR )
132 131 26 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. RR )
133 1 rpcnd 
 |-  ( ph -> A e. CC )
134 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ A e. CC ) -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
135 43 133 134 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
136 1cnd 
 |-  ( ph -> 1 e. CC )
137 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
138 43 136 137 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
139 132 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. CC )
140 1cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
141 131 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
142 141 33 33 75 divsubdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - ( ( log ` x ) / ( log ` x ) ) ) )
143 141 33 subcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
144 143 33 75 divrecd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) )
145 33 75 dividd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
146 145 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - ( ( log ` x ) / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) )
147 142 144 146 3eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) )
148 147 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) )
149 131 29 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR )
150 14 26 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
151 19 ex 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
152 151 ssrdv 
 |-  ( ph -> ( 1 (,) +oo ) C_ RR+ )
153 vmadivsum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
154 153 a1i 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
155 152 154 o1res2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
156 divlogrlim 
 |-  ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0
157 rlimo1 
 |-  ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
158 156 157 mp1i 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
159 149 150 155 158 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
160 148 159 eqeltrrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) e. O(1) )
161 139 140 160 o1dif 
 |-  ( ph -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) ) )
162 138 161 mpbird 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. O(1) )
163 130 132 135 162 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) ) e. O(1) )
164 130 132 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. RR )
165 23 6 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / n ) e. RR )
166 94 165 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( log ` ( x / n ) ) / n ) ) e. RR )
167 99 166 resubcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) e. RR )
168 8 167 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. RR )
169 4 168 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. RR )
170 169 26 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) e. RR )
171 170 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) e. CC )
172 169 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. CC )
173 172 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) e. RR )
174 130 131 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) e. RR )
175 100 106 subcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) e. CC )
176 98 175 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. CC )
177 176 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) e. RR )
178 4 177 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) e. RR )
179 168 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. CC )
180 4 179 fsumabs 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) )
181 130 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. RR )
182 181 9 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. ( ( Lam ` n ) / n ) ) e. RR )
183 175 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. RR )
184 181 6 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A / n ) e. RR )
185 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
186 6 185 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
187 108 109 103 91 104 divdiv2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) x. n ) / x ) )
188 108 103 109 91 div23d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) x. n ) / x ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) )
189 187 188 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) )
190 101 105 103 mulassd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) = ( 2 x. ( ( ( log ` ( x / n ) ) / n ) x. n ) ) )
191 102 103 104 divcan1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) / n ) x. n ) = ( log ` ( x / n ) ) )
192 191 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( log ` ( x / n ) ) / n ) x. n ) ) = ( 2 x. ( log ` ( x / n ) ) ) )
193 190 192 eqtr2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( log ` ( x / n ) ) ) = ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) )
194 189 193 oveq12d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) = ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) - ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) ) )
195 100 106 103 subdird 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) = ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) - ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) ) )
196 194 195 eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) = ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) )
197 196 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) = ( abs ` ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) ) )
198 175 103 absmuld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) ) = ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. ( abs ` n ) ) )
199 6 nnred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
200 21 rpge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ n )
201 199 200 absidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` n ) = n )
202 201 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. ( abs ` n ) ) = ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. n ) )
203 197 198 202 3eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) = ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. n ) )
204 fveq2 
 |-  ( i = m -> ( Lam ` i ) = ( Lam ` m ) )
205 fveq2 
 |-  ( i = m -> ( log ` i ) = ( log ` m ) )
206 oveq2 
 |-  ( i = m -> ( y / i ) = ( y / m ) )
207 206 fveq2d 
 |-  ( i = m -> ( psi ` ( y / i ) ) = ( psi ` ( y / m ) ) )
208 205 207 oveq12d 
 |-  ( i = m -> ( ( log ` i ) + ( psi ` ( y / i ) ) ) = ( ( log ` m ) + ( psi ` ( y / m ) ) ) )
209 204 208 oveq12d 
 |-  ( i = m -> ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) = ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( y / m ) ) ) ) )
210 209 cbvsumv 
 |-  sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( y / m ) ) ) )
211 fveq2 
 |-  ( y = ( x / n ) -> ( |_ ` y ) = ( |_ ` ( x / n ) ) )
212 211 oveq2d 
 |-  ( y = ( x / n ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` ( x / n ) ) ) )
213 fvoveq1 
 |-  ( y = ( x / n ) -> ( psi ` ( y / m ) ) = ( psi ` ( ( x / n ) / m ) ) )
214 213 oveq2d 
 |-  ( y = ( x / n ) -> ( ( log ` m ) + ( psi ` ( y / m ) ) ) = ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) )
215 214 oveq2d 
 |-  ( y = ( x / n ) -> ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( y / m ) ) ) ) = ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) )
216 215 adantr 
 |-  ( ( y = ( x / n ) /\ m e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( y / m ) ) ) ) = ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) )
217 212 216 sumeq12dv 
 |-  ( y = ( x / n ) -> sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( y / m ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) )
218 210 217 eqtrid 
 |-  ( y = ( x / n ) -> sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) )
219 id 
 |-  ( y = ( x / n ) -> y = ( x / n ) )
220 218 219 oveq12d 
 |-  ( y = ( x / n ) -> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) )
221 fveq2 
 |-  ( y = ( x / n ) -> ( log ` y ) = ( log ` ( x / n ) ) )
222 221 oveq2d 
 |-  ( y = ( x / n ) -> ( 2 x. ( log ` y ) ) = ( 2 x. ( log ` ( x / n ) ) ) )
223 220 222 oveq12d 
 |-  ( y = ( x / n ) -> ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) )
224 223 fveq2d 
 |-  ( y = ( x / n ) -> ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) = ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) )
225 224 breq1d 
 |-  ( y = ( x / n ) -> ( ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A <-> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) <_ A ) )
226 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
227 103 mullidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
228 fznnfl 
 |-  ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
229 11 228 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
230 229 simplbda 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
231 227 230 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
232 1red 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
233 232 59 21 lemuldivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
234 231 233 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
235 1re 
 |-  1 e. RR
236 elicopnf 
 |-  ( 1 e. RR -> ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) ) )
237 235 236 ax-mp 
 |-  ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) )
238 60 234 237 sylanbrc 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. ( 1 [,) +oo ) )
239 225 226 238 rspcdva 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) <_ A )
240 203 239 eqbrtrrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. n ) <_ A )
241 183 181 21 lemuldivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. n ) <_ A <-> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) <_ ( A / n ) ) )
242 240 241 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) <_ ( A / n ) )
243 183 184 8 186 242 lemul2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) <_ ( ( Lam ` n ) x. ( A / n ) ) )
244 98 175 absmuld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) = ( ( abs ` ( Lam ` n ) ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) )
245 8 186 absidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( Lam ` n ) ) = ( Lam ` n ) )
246 245 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( Lam ` n ) ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) = ( ( Lam ` n ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) )
247 244 246 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) = ( ( Lam ` n ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) )
248 133 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. CC )
249 248 98 103 104 div12d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. ( ( Lam ` n ) / n ) ) = ( ( Lam ` n ) x. ( A / n ) ) )
250 243 247 249 3brtr4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) <_ ( A x. ( ( Lam ` n ) / n ) ) )
251 4 177 182 250 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( A x. ( ( Lam ` n ) / n ) ) )
252 133 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. CC )
253 9 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
254 4 252 253 fsummulc2 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( A x. ( ( Lam ` n ) / n ) ) )
255 251 254 breqtrrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) <_ ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) )
256 173 178 174 180 255 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) <_ ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) )
257 173 174 26 256 lediv1dd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) / ( log ` x ) ) <_ ( ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) / ( log ` x ) ) )
258 252 141 33 75 divassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) / ( log ` x ) ) = ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) )
259 257 258 breqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) / ( log ` x ) ) <_ ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) )
260 172 33 75 absdivd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) / ( abs ` ( log ` x ) ) ) )
261 26 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( log ` x ) )
262 29 261 absidd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( log ` x ) ) = ( log ` x ) )
263 262 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) / ( abs ` ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) / ( log ` x ) ) )
264 260 263 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) / ( log ` x ) ) )
265 129 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ A )
266 8 21 186 divge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
267 4 9 266 fsumge0 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
268 131 26 267 divge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) )
269 130 132 265 268 mulge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) )
270 164 269 absidd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) ) = ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) )
271 259 264 270 3brtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) ) <_ ( abs ` ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) ) )
272 271 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) ) <_ ( abs ` ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) ) )
273 128 163 164 171 272 o1le 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) ) e. O(1) )
274 127 273 eqeltrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) - ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) ) e. O(1) )
275 73 78 274 o1dif 
 |-  ( ph -> ( ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) ) )
276 51 275 mpbird 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) )