Metamath Proof Explorer

Theorem vmalogdivsum

Description: The sum sum_ n <_ x , Lam ( n ) log n / n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ) . Exercise 9.1.7 of Shapiro, p. 336. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion vmalogdivsum 
|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
2 1 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
3 1rp 
 |-  1 e. RR+
4 3 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5 1red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
6 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
7 6 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
8 7 simpld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
9 5 2 8 ltled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
10 2 4 9 rpgecld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
11 10 ex 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
12 11 ssrdv 
 |-  ( T. -> ( 1 (,) +oo ) C_ RR+ )
13 vmadivsum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
14 13 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
15 12 14 o1res2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
16 fzfid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
17 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
18 17 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
19 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
20 18 19 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
21 20 18 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
22 21 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
23 16 22 fsumcl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
24 10 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
25 24 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
26 23 25 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
27 18 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
28 27 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
29 21 28 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. RR )
30 16 29 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. RR )
31 2 8 rplogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
32 30 31 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) e. RR )
33 24 rehalfcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. RR )
34 32 33 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. RR )
35 34 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
36 33 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
37 23 36 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) e. CC )
38 32 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) e. CC )
39 37 38 36 nnncan2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) )
40 23 36 36 subsub4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) - ( ( log ` x ) / 2 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( ( log ` x ) / 2 ) + ( ( log ` x ) / 2 ) ) ) )
41 25 2halvesd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) / 2 ) + ( ( log ` x ) / 2 ) ) = ( log ` x ) )
42 41 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( ( log ` x ) / 2 ) + ( ( log ` x ) / 2 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) )
43 40 42 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) - ( ( log ` x ) / 2 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) )
44 43 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) )
45 23 36 38 sub32d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) - ( ( log ` x ) / 2 ) ) )
46 10 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
47 46 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` x ) e. RR )
48 21 47 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) e. RR )
49 48 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) e. CC )
50 29 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. CC )
51 16 49 50 fsumsub 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
52 46 27 relogdivd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) = ( ( log ` x ) - ( log ` n ) ) )
53 52 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) = ( ( ( Lam ` n ) / n ) x. ( ( log ` x ) - ( log ` n ) ) ) )
54 25 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` x ) e. CC )
55 28 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
56 22 54 55 subdid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( ( log ` x ) - ( log ` n ) ) ) = ( ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
57 53 56 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) = ( ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
58 57 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
59 20 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
60 18 nncnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
61 18 nnne0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
62 59 60 61 divcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
63 16 25 62 fsummulc1 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) )
64 63 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
65 51 58 64 3eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
66 65 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) / ( log ` x ) ) )
67 23 25 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) e. CC )
68 30 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. CC )
69 31 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
70 67 68 25 69 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) / ( log ` x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) )
71 23 25 69 divcan4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) / ( log ` x ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
72 71 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( log ` x ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) )
73 66 70 72 3eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) )
74 73 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 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 ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) - ( ( log ` x ) / 2 ) ) )
75 45 74 eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` x ) / 2 ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) )
76 39 44 75 3eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) )
77 76 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) )
78 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)
79 77 78 eqeltrdi 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O(1) )
80 26 35 79 o1dif 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) ) )
81 15 80 mpbid 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
82 81 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)