Metamath Proof Explorer

Theorem vmadivsum

Description: The sum of the von Mangoldt function over n is asymptotic to log x + O(1) . Equation 9.2.13 of Shapiro, p. 331. (Contributed by Mario Carneiro, 16-Apr-2016)

Ref Expression
Assertion vmadivsum 
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 rpssre 
 |-  RR+ C_ RR
3 1 2 ssexi 
 |-  RR+ e. _V
4 3 a1i 
 |-  ( T. -> RR+ e. _V )
5 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. _V )
6 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. _V )
7 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) )
8 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) )
9 4 5 6 7 8 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) )
10 9 mptru 
 |-  ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) )
11 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
12 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
13 12 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
14 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
15 13 14 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
16 15 13 nndivred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
17 11 16 fsumrecl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR )
18 17 recnd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
19 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
20 19 recnd 
 |-  ( x e. RR+ -> ( log ` x ) e. CC )
21 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
22 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
23 faccl 
 |-  ( ( |_ ` x ) e. NN0 -> ( ! ` ( |_ ` x ) ) e. NN )
24 21 22 23 3syl 
 |-  ( x e. RR+ -> ( ! ` ( |_ ` x ) ) e. NN )
25 24 nnrpd 
 |-  ( x e. RR+ -> ( ! ` ( |_ ` x ) ) e. RR+ )
26 25 relogcld 
 |-  ( x e. RR+ -> ( log ` ( ! ` ( |_ ` x ) ) ) e. RR )
27 rerpdivcl 
 |-  ( ( ( log ` ( ! ` ( |_ ` x ) ) ) e. RR /\ x e. RR+ ) -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. RR )
28 26 27 mpancom 
 |-  ( x e. RR+ -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. RR )
29 28 recnd 
 |-  ( x e. RR+ -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. CC )
30 18 20 29 nnncan2d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) )
31 30 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) )
32 10 31 eqtri 
 |-  ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) )
33 1red 
 |-  ( T. -> 1 e. RR )
34 chpo1ub 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)
35 34 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) )
36 rpre 
 |-  ( x e. RR+ -> x e. RR )
37 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
38 36 37 syl 
 |-  ( x e. RR+ -> ( psi ` x ) e. RR )
39 rerpdivcl 
 |-  ( ( ( psi ` x ) e. RR /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR )
40 38 39 mpancom 
 |-  ( x e. RR+ -> ( ( psi ` x ) / x ) e. RR )
41 40 recnd 
 |-  ( x e. RR+ -> ( ( psi ` x ) / x ) e. CC )
42 41 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. CC )
43 18 29 subcld 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. CC )
44 43 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. CC )
45 36 adantr 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
46 16 45 remulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. x ) e. RR )
47 nndivre 
 |-  ( ( x e. RR /\ n e. NN ) -> ( x / n ) e. RR )
48 36 12 47 syl2an 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
49 reflcl 
 |-  ( ( x / n ) e. RR -> ( |_ ` ( x / n ) ) e. RR )
50 48 49 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. RR )
51 15 50 remulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) e. RR )
52 46 51 resubcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) e. RR )
53 48 50 resubcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) e. RR )
54 1red 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
55 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
56 13 55 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
57 fracle1 
 |-  ( ( x / n ) e. RR -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) <_ 1 )
58 48 57 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) <_ 1 )
59 53 54 15 56 58 lemul2ad 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) <_ ( ( Lam ` n ) x. 1 ) )
60 15 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
61 48 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
62 50 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. CC )
63 60 61 62 subdid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) = ( ( ( Lam ` n ) x. ( x / n ) ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
64 rpcn 
 |-  ( x e. RR+ -> x e. CC )
65 64 adantr 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
66 13 nnrpd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
67 rpcnne0 
 |-  ( n e. RR+ -> ( n e. CC /\ n =/= 0 ) )
68 66 67 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. CC /\ n =/= 0 ) )
69 div23 
 |-  ( ( ( Lam ` n ) e. CC /\ x e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( Lam ` n ) x. x ) / n ) = ( ( ( Lam ` n ) / n ) x. x ) )
70 divass 
 |-  ( ( ( Lam ` n ) e. CC /\ x e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( Lam ` n ) x. x ) / n ) = ( ( Lam ` n ) x. ( x / n ) ) )
71 69 70 eqtr3d 
 |-  ( ( ( Lam ` n ) e. CC /\ x e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( Lam ` n ) / n ) x. x ) = ( ( Lam ` n ) x. ( x / n ) ) )
72 60 65 68 71 syl3anc 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. x ) = ( ( Lam ` n ) x. ( x / n ) ) )
73 72 oveq1d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) = ( ( ( Lam ` n ) x. ( x / n ) ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
74 63 73 eqtr4d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) = ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
75 60 mulid1d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. 1 ) = ( Lam ` n ) )
76 59 74 75 3brtr3d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) <_ ( Lam ` n ) )
77 11 52 15 76 fsumle 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )
78 16 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
79 11 64 78 fsummulc1 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. x ) )
80 logfac2 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( log ` ( ! ` ( |_ ` x ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) )
81 21 80 syl 
 |-  ( x e. RR+ -> ( log ` ( ! ` ( |_ ` x ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) )
82 79 81 oveq12d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
83 46 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. x ) e. CC )
84 51 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) e. CC )
85 11 83 84 fsumsub 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
86 82 85 eqtr4d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
87 chpval 
 |-  ( x e. RR -> ( psi ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )
88 36 87 syl 
 |-  ( x e. RR+ -> ( psi ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )
89 77 86 88 3brtr4d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) <_ ( psi ` x ) )
90 17 36 remulcld 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) e. RR )
91 90 26 resubcld 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR )
92 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
93 lediv1 
 |-  ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR /\ ( psi ` x ) e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) <_ ( psi ` x ) <-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) <_ ( ( psi ` x ) / x ) ) )
94 91 38 92 93 syl3anc 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) <_ ( psi ` x ) <-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) <_ ( ( psi ` x ) / x ) ) )
95 89 94 mpbid 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) <_ ( ( psi ` x ) / x ) )
96 90 recnd 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) e. CC )
97 26 recnd 
 |-  ( x e. RR+ -> ( log ` ( ! ` ( |_ ` x ) ) ) e. CC )
98 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
99 divsubdir 
 |-  ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) e. CC /\ ( log ` ( ! ` ( |_ ` x ) ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) )
100 96 97 98 99 syl3anc 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) )
101 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
102 18 64 101 divcan4d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
103 102 oveq1d 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) )
104 100 103 eqtr2d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) )
105 104 fveq2d 
 |-  ( x e. RR+ -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) )
106 rerpdivcl 
 |-  ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR /\ x e. RR+ ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) e. RR )
107 91 106 mpancom 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) e. RR )
108 flle 
 |-  ( ( x / n ) e. RR -> ( |_ ` ( x / n ) ) <_ ( x / n ) )
109 48 108 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) <_ ( x / n ) )
110 48 50 subge0d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 <_ ( ( x / n ) - ( |_ ` ( x / n ) ) ) <-> ( |_ ` ( x / n ) ) <_ ( x / n ) ) )
111 109 110 mpbird 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( x / n ) - ( |_ ` ( x / n ) ) ) )
112 15 53 56 111 mulge0d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) )
113 112 74 breqtrd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
114 11 52 113 fsumge0 
 |-  ( x e. RR+ -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) )
115 114 86 breqtrrd 
 |-  ( x e. RR+ -> 0 <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) )
116 divge0 
 |-  ( ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR /\ 0 <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) )
117 91 115 92 116 syl21anc 
 |-  ( x e. RR+ -> 0 <_ ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) )
118 107 117 absidd 
 |-  ( x e. RR+ -> ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) )
119 105 118 eqtrd 
 |-  ( x e. RR+ -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) )
120 chpge0 
 |-  ( x e. RR -> 0 <_ ( psi ` x ) )
121 36 120 syl 
 |-  ( x e. RR+ -> 0 <_ ( psi ` x ) )
122 divge0 
 |-  ( ( ( ( psi ` x ) e. RR /\ 0 <_ ( psi ` x ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( psi ` x ) / x ) )
123 38 121 92 122 syl21anc 
 |-  ( x e. RR+ -> 0 <_ ( ( psi ` x ) / x ) )
124 40 123 absidd 
 |-  ( x e. RR+ -> ( abs ` ( ( psi ` x ) / x ) ) = ( ( psi ` x ) / x ) )
125 95 119 124 3brtr4d 
 |-  ( x e. RR+ -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) <_ ( abs ` ( ( psi ` x ) / x ) ) )
126 125 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) <_ ( abs ` ( ( psi ` x ) / x ) ) )
127 33 35 42 44 126 o1le 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) )
128 127 mptru 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1)
129 logfacrlim 
 |-  ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ~~>r 1
130 rlimo1 
 |-  ( ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ~~>r 1 -> ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) )
131 129 130 ax-mp 
 |-  ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1)
132 o1sub 
 |-  ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) /\ ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) e. O(1) )
133 128 131 132 mp2an 
 |-  ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) e. O(1)
134 32 133 eqeltrri 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)