Metamath Proof Explorer

Theorem 2vmadivsumlem

Description: Lemma for 2vmadivsum . (Contributed by Mario Carneiro, 30-May-2016)

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

Proof

Step Hyp Ref Expression
1 2vmadivsum.1 
 |-  ( ph -> A e. RR+ )
2 2vmadivsum.2 
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ A )
3 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)
4 3 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) )
5 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
6 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
7 6 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
8 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
9 7 8 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
10 9 7 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
11 fzfid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
12 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
13 12 adantl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
14 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
15 13 14 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` m ) e. RR )
16 15 13 nndivred 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) / m ) e. RR )
17 11 16 fsumrecl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) e. RR )
18 10 17 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) e. RR )
19 5 18 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) e. RR )
20 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
21 20 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
22 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
23 22 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
24 23 simpld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
25 21 24 rplogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
26 19 25 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) e. RR )
27 1rp 
 |-  1 e. RR+
28 27 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
29 1red 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
30 29 21 24 ltled 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
31 21 28 30 rpgecld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
32 31 relogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
33 32 rehalfcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. RR )
34 26 33 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. RR )
35 34 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
36 31 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
37 7 nnrpd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
38 36 37 rpdivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
39 38 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
40 10 39 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
41 5 40 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
42 41 25 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. RR )
43 42 33 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 )
44 43 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
45 19 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) e. CC )
46 41 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
47 32 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
48 25 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
49 45 46 47 48 divsubdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
50 10 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
51 17 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) e. CC )
52 39 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
53 50 51 52 subdid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) = ( ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
54 53 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
55 18 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) e. CC )
56 40 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
57 5 55 56 fsumsub 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
58 54 57 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
59 58 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) )
60 26 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) e. CC )
61 42 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
62 33 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
63 60 61 62 nnncan2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
64 49 59 63 3eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) )
65 64 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) )
66 1red 
 |-  ( ph -> 1 e. RR )
67 5 10 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR )
68 67 25 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. RR )
69 1 rpred 
 |-  ( ph -> A e. RR )
70 69 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR )
71 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
72 1cnd 
 |-  ( ph -> 1 e. CC )
73 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
74 71 72 73 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
75 68 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. CC )
76 1cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
77 67 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
78 77 47 47 48 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 ) ) ) )
79 77 47 subcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
80 79 47 48 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 ) ) ) )
81 47 48 dividd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
82 81 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 ) )
83 78 80 82 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 ) )
84 83 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 ) ) )
85 67 32 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR )
86 29 25 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
87 31 ex 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
88 87 ssrdv 
 |-  ( ph -> ( 1 (,) +oo ) C_ RR+ )
89 vmadivsum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
90 89 a1i 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
91 88 90 o1res2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
92 divlogrlim 
 |-  ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0
93 rlimo1 
 |-  ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
94 92 93 mp1i 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
95 85 86 91 94 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
96 84 95 eqeltrrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) e. O(1) )
97 75 76 96 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) ) )
98 74 97 mpbird 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. O(1) )
99 69 recnd 
 |-  ( ph -> A e. CC )
100 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ A e. CC ) -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
101 71 99 100 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
102 68 70 98 101 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) ) e. O(1) )
103 68 70 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) e. RR )
104 17 39 resubcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) e. RR )
105 10 104 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) e. RR )
106 5 105 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) e. RR )
107 106 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) e. CC )
108 107 47 48 divcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) e. CC )
109 107 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) e. RR )
110 67 70 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) e. RR )
111 105 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) e. CC )
112 111 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) e. RR )
113 5 112 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) e. RR )
114 5 111 fsumabs 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) )
115 70 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. RR )
116 10 115 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. A ) e. RR )
117 104 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) e. CC )
118 50 117 absmuld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) = ( ( abs ` ( ( Lam ` n ) / n ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) )
119 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
120 7 119 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
121 9 37 120 divge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
122 10 121 absidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) / n ) ) = ( ( Lam ` n ) / n ) )
123 122 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( Lam ` n ) / n ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) = ( ( ( Lam ` n ) / n ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) )
124 118 123 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) = ( ( ( Lam ` n ) / n ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) )
125 117 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) e. RR )
126 fveq2 
 |-  ( i = m -> ( Lam ` i ) = ( Lam ` m ) )
127 id 
 |-  ( i = m -> i = m )
128 126 127 oveq12d 
 |-  ( i = m -> ( ( Lam ` i ) / i ) = ( ( Lam ` m ) / m ) )
129 128 cbvsumv 
 |-  sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) = sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` m ) / m )
130 fveq2 
 |-  ( y = ( x / n ) -> ( |_ ` y ) = ( |_ ` ( x / n ) ) )
131 130 oveq2d 
 |-  ( y = ( x / n ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` ( x / n ) ) ) )
132 131 sumeq1d 
 |-  ( y = ( x / n ) -> sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` m ) / m ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) )
133 129 132 eqtrid 
 |-  ( y = ( x / n ) -> sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) )
134 fveq2 
 |-  ( y = ( x / n ) -> ( log ` y ) = ( log ` ( x / n ) ) )
135 133 134 oveq12d 
 |-  ( y = ( x / n ) -> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) )
136 135 fveq2d 
 |-  ( y = ( x / n ) -> ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) )
137 136 breq1d 
 |-  ( y = ( x / n ) -> ( ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ A <-> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) <_ A ) )
138 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ A )
139 38 rpred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
140 7 nncnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
141 140 mullidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
142 fznnfl 
 |-  ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
143 21 142 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
144 143 simplbda 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
145 141 144 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
146 1red 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
147 21 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
148 146 147 37 lemuldivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
149 145 148 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
150 1re 
 |-  1 e. RR
151 elicopnf 
 |-  ( 1 e. RR -> ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) ) )
152 150 151 ax-mp 
 |-  ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) )
153 139 149 152 sylanbrc 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. ( 1 [,) +oo ) )
154 137 138 153 rspcdva 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) <_ A )
155 125 115 10 121 154 lemul2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) <_ ( ( ( Lam ` n ) / n ) x. A ) )
156 124 155 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) <_ ( ( ( Lam ` n ) / n ) x. A ) )
157 5 112 116 156 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. A ) )
158 99 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. CC )
159 5 158 50 fsummulc1 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. A ) )
160 157 159 breqtrrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) )
161 109 113 110 114 160 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) )
162 109 110 25 161 lediv1dd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) / ( log ` x ) ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) / ( log ` x ) ) )
163 107 47 48 absdivd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) / ( abs ` ( log ` x ) ) ) )
164 25 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( log ` x ) )
165 32 164 absidd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( log ` x ) ) = ( log ` x ) )
166 165 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) / ( abs ` ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) / ( log ` x ) ) )
167 163 166 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) ) / ( log ` x ) ) )
168 5 10 121 fsumge0 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
169 67 25 168 divge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) )
170 1 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR+ )
171 170 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ A )
172 68 70 169 171 mulge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) )
173 103 172 absidd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) )
174 77 158 47 48 div23d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) )
175 173 174 eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) / ( log ` x ) ) )
176 162 167 175 3brtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) ) )
177 176 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) x. A ) ) )
178 66 102 103 108 177 o1le 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. O(1) )
179 65 178 eqeltrrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O(1) )
180 35 44 179 o1dif 
 |-  ( ph -> ( ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) ) )
181 4 180 mpbird 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )