Metamath Proof Explorer

Theorem vmalogdivsum2

Description: The sum sum_ n <_ x , Lam ( n ) log ( x / 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 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)

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
2 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN )
3 2 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN )
4 3 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. RR+ )
5 4 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` k ) e. RR )
6 5 3 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` k ) / k ) e. RR )
7 1 6 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. RR )
8 7 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. CC )
9 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
10 9 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
11 1rp 
 |-  1 e. RR+
12 11 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
13 1red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
14 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
15 14 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
16 15 simpld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
17 13 10 16 ltled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
18 10 12 17 rpgecld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
19 18 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
20 19 resqcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. RR )
21 20 rehalfcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. RR )
22 21 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. CC )
23 19 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
24 10 16 rplogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
25 24 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
26 8 22 23 25 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) / ( log ` x ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) ) )
27 7 21 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) e. RR )
28 27 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) e. CC )
29 28 23 25 divrecd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) / ( log ` x ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) )
30 20 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. CC )
31 2cnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
32 2ne0 
 |-  2 =/= 0
33 32 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
34 30 31 23 33 25 divdiv32d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) )
35 23 sqvald 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) = ( ( log ` x ) x. ( log ` x ) ) )
36 35 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) )
37 23 23 25 divcan3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) = ( log ` x ) )
38 36 37 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( log ` x ) )
39 38 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) = ( ( log ` x ) / 2 ) )
40 34 39 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( log ` x ) / 2 ) )
41 40 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) )
42 26 29 41 3eqtr3rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) )
43 42 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) ) )
44 24 rprecred 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
45 18 ex 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
46 45 ssrdv 
 |-  ( T. -> ( 1 (,) +oo ) C_ RR+ )
47 eqid 
 |-  ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) = ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) )
48 47 logdivsum 
 |-  ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) : RR+ --> RR /\ ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~>r /\ ( ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) ~~>r 1 /\ 1 e. RR+ /\ _e <_ 1 ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) ` 1 ) - 1 ) ) <_ ( ( log ` 1 ) / 1 ) ) )
49 48 simp2i 
 |-  ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~>r
50 rlimdmo1 
 |-  ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~>r -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) )
51 49 50 mp1i 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) )
52 46 51 o1res2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) )
53 divlogrlim 
 |-  ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0
54 rlimo1 
 |-  ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
55 53 54 mp1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
56 27 44 52 55 o1mul2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
57 43 56 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
58 8 23 25 divcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) e. CC )
59 23 halfcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
60 58 59 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
61 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
62 61 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
63 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
64 62 63 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
65 64 62 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
66 18 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
67 62 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
68 66 67 rpdivcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
69 68 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
70 65 69 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
71 1 70 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
72 71 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
73 24 rpcnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
74 72 73 25 divcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
75 73 halfcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
76 74 75 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
77 58 74 59 nnncan2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
78 8 72 23 25 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
79 fzfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
80 64 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` n ) e. RR )
81 62 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. NN )
82 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
83 82 adantl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
84 81 83 nnmulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n x. m ) e. NN )
85 80 84 nndivred 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` n ) / ( n x. m ) ) e. RR )
86 79 85 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) e. RR )
87 86 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) e. CC )
88 70 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
89 1 87 88 fsumsub 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
90 64 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
91 62 nncnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
92 62 nnne0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
93 90 91 92 divcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
94 83 nnrecred 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. RR )
95 79 94 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. RR )
96 95 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. CC )
97 69 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
98 93 96 97 subdid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
99 90 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` n ) e. CC )
100 91 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. CC )
101 83 nncnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. CC )
102 92 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n =/= 0 )
103 83 nnne0d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m =/= 0 )
104 99 100 101 102 103 divdiv1d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` n ) / n ) / m ) = ( ( Lam ` n ) / ( n x. m ) ) )
105 99 100 102 divcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
106 105 101 103 divrecd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` n ) / n ) / m ) = ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) )
107 104 106 eqtr3d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` n ) / ( n x. m ) ) = ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) )
108 107 sumeq2dv 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) )
109 101 103 reccld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. CC )
110 79 93 109 fsummulc2 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) )
111 108 110 eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) = ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) )
112 111 oveq1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
113 98 112 eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
114 113 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
115 vmasum 
 |-  ( k e. NN -> sum_ n e. { y e. NN | y || k } ( Lam ` n ) = ( log ` k ) )
116 3 115 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> sum_ n e. { y e. NN | y || k } ( Lam ` n ) = ( log ` k ) )
117 116 oveq1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. { y e. NN | y || k } ( Lam ` n ) / k ) = ( ( log ` k ) / k ) )
118 fzfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... k ) e. Fin )
119 dvdsssfz1 
 |-  ( k e. NN -> { y e. NN | y || k } C_ ( 1 ... k ) )
120 3 119 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || k } C_ ( 1 ... k ) )
121 118 120 ssfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || k } e. Fin )
122 3 nncnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. CC )
123 ssrab2 
 |-  { y e. NN | y || k } C_ NN
124 simprr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. { y e. NN | y || k } )
125 123 124 sselid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. NN )
126 125 63 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( Lam ` n ) e. RR )
127 126 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( Lam ` n ) e. CC )
128 127 anassrs 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ n e. { y e. NN | y || k } ) -> ( Lam ` n ) e. CC )
129 3 nnne0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k =/= 0 )
130 121 122 128 129 fsumdivc 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. { y e. NN | y || k } ( Lam ` n ) / k ) = sum_ n e. { y e. NN | y || k } ( ( Lam ` n ) / k ) )
131 117 130 eqtr3d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` k ) / k ) = sum_ n e. { y e. NN | y || k } ( ( Lam ` n ) / k ) )
132 131 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) = sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( Lam ` n ) / k ) )
133 oveq2 
 |-  ( k = ( n x. m ) -> ( ( Lam ` n ) / k ) = ( ( Lam ` n ) / ( n x. m ) ) )
134 2 ad2antrl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. NN )
135 134 nncnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. CC )
136 134 nnne0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k =/= 0 )
137 127 135 136 divcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( ( Lam ` n ) / k ) e. CC )
138 133 10 137 dvdsflsumcom 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( Lam ` n ) / k ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) )
139 132 138 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) )
140 139 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
141 89 114 140 3eqtr4rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) )
142 141 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - 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 ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) )
143 77 78 142 3eqtr2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( 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 ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) )
144 143 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) )
145 1red 
 |-  ( T. -> 1 e. RR )
146 1 65 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR )
147 146 24 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. RR )
148 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
149 ax-1cn 
 |-  1 e. CC
150 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
151 148 149 150 mp2an 
 |-  ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1)
152 151 a1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
153 147 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. CC )
154 12 rpcnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
155 146 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
156 155 23 23 25 divsubdird 
 |-  ( ( T. /\ 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 ) ) ) )
157 155 23 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
158 157 23 25 divrecd 
 |-  ( ( T. /\ 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 ) ) ) )
159 23 25 dividd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
160 159 oveq2d 
 |-  ( ( T. /\ 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 ) )
161 156 158 160 3eqtr3rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) )
162 161 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) )
163 146 19 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR )
164 vmadivsum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
165 164 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
166 46 165 o1res2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
167 163 44 166 55 o1mul2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
168 162 167 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) e. O(1) )
169 153 154 168 o1dif 
 |-  ( T. -> ( ( 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) ) )
170 152 169 mpbird 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. O(1) )
171 147 170 o1lo1d 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. <_O(1) )
172 95 69 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) e. RR )
173 65 172 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR )
174 1 173 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR )
175 174 24 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) e. RR )
176 1red 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
177 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
178 62 177 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
179 64 67 178 divge0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
180 68 rpred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
181 91 mullidd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
182 fznnfl 
 |-  ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
183 10 182 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
184 183 simplbda 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
185 181 184 eqbrtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
186 10 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
187 176 186 67 lemuldivd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
188 185 187 mpbid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
189 harmonicubnd 
 |-  ( ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) )
190 180 188 189 syl2anc 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) )
191 95 69 176 lesubadd2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) <_ 1 <-> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) ) )
192 190 191 mpbird 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) <_ 1 )
193 172 176 65 179 192 lemul2ad 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ ( ( ( Lam ` n ) / n ) x. 1 ) )
194 93 mulridd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. 1 ) = ( ( Lam ` n ) / n ) )
195 193 194 breqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ ( ( Lam ` n ) / n ) )
196 1 173 65 195 fsumle 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
197 174 146 24 196 lediv1dd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) )
198 197 adantrr 
 |-  ( ( T. /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) )
199 145 171 147 175 198 lo1le 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. <_O(1) )
200 0red 
 |-  ( T. -> 0 e. RR )
201 harmoniclbnd 
 |-  ( ( x / n ) e. RR+ -> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) )
202 68 201 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) )
203 95 69 subge0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 <_ ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) <-> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) )
204 202 203 mpbird 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) )
205 65 172 179 204 mulge0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) )
206 1 173 205 fsumge0 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) )
207 174 24 206 divge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) )
208 175 200 207 o1lo12 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. <_O(1) ) )
209 199 208 mpbird 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. O(1) )
210 144 209 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( 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) )
211 60 76 210 o1dif 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( 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) ) )
212 57 211 mpbid 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
213 212 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)