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)