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 syl5eq
 |-  ( 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 mulid2d
 |-  ( ( ( 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) )