Metamath Proof Explorer


Theorem vmadivsumb

Description: Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion vmadivsumb
|- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ c

Proof

Step Hyp Ref Expression
1 1re
 |-  1 e. RR
2 elicopnf
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
3 1 2 mp1i
 |-  ( T. -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
4 3 simprbda
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> x e. RR )
5 1rp
 |-  1 e. RR+
6 5 a1i
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 1 e. RR+ )
7 3 simplbda
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x )
8 4 6 7 rpgecld
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> x e. RR+ )
9 8 ex
 |-  ( T. -> ( x e. ( 1 [,) +oo ) -> x e. RR+ ) )
10 9 ssrdv
 |-  ( T. -> ( 1 [,) +oo ) C_ RR+ )
11 rpssre
 |-  RR+ C_ RR
12 10 11 sstrdi
 |-  ( T. -> ( 1 [,) +oo ) C_ RR )
13 1 a1i
 |-  ( T. -> 1 e. RR )
14 fzfid
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
15 elfznn
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
16 15 adantl
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
17 vmacl
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
18 16 17 syl
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
19 18 16 nndivred
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
20 14 19 fsumrecl
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR )
21 8 relogcld
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( log ` x ) e. RR )
22 20 21 resubcld
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR )
23 22 recnd
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
24 vmadivsum
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
25 24 a1i
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
26 10 25 o1res2
 |-  ( T. -> ( x e. ( 1 [,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
27 fzfid
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( 1 ... ( |_ ` y ) ) e. Fin )
28 elfznn
 |-  ( n e. ( 1 ... ( |_ ` y ) ) -> n e. NN )
29 28 adantl
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. NN )
30 29 17 syl
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( Lam ` n ) e. RR )
31 30 29 nndivred
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
32 27 31 fsumrecl
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) e. RR )
33 simprl
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR )
34 5 a1i
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> 1 e. RR+ )
35 simprr
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> 1 <_ y )
36 33 34 35 rpgecld
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR+ )
37 36 relogcld
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( log ` y ) e. RR )
38 32 37 readdcld
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) e. RR )
39 22 adantr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR )
40 39 recnd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
41 40 abscld
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. RR )
42 20 adantr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR )
43 8 adantr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR+ )
44 43 relogcld
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. RR )
45 42 44 readdcld
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) e. RR )
46 38 ad2ant2r
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) e. RR )
47 42 recnd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
48 44 recnd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. CC )
49 47 48 abs2dif2d
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) + ( abs ` ( log ` x ) ) ) )
50 16 nnrpd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
51 vmage0
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
52 16 51 syl
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
53 18 50 52 divge0d
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
54 14 19 53 fsumge0
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
55 54 adantr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
56 42 55 absidd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) )
57 21 adantr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. RR )
58 4 adantr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR )
59 7 adantr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 <_ x )
60 58 59 logge0d
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( log ` x ) )
61 57 60 absidd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( log ` x ) ) = ( log ` x ) )
62 56 61 oveq12d
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) + ( abs ` ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) )
63 49 62 breqtrd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) )
64 32 ad2ant2r
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) e. RR )
65 36 ad2ant2r
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR+ )
66 65 relogcld
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` y ) e. RR )
67 fzfid
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 1 ... ( |_ ` y ) ) e. Fin )
68 28 adantl
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. NN )
69 68 17 syl
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( Lam ` n ) e. RR )
70 69 68 nndivred
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
71 68 nnrpd
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. RR+ )
72 68 51 syl
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> 0 <_ ( Lam ` n ) )
73 69 71 72 divge0d
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
74 simprll
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR )
75 simprr
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x < y )
76 58 74 75 ltled
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x <_ y )
77 flword2
 |-  ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) )
78 58 74 76 77 syl3anc
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) )
79 fzss2
 |-  ( ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) -> ( 1 ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` y ) ) )
80 78 79 syl
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 1 ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` y ) ) )
81 67 70 73 80 fsumless
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) <_ sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) )
82 74 43 76 rpgecld
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR+ )
83 43 82 logled
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( x <_ y <-> ( log ` x ) <_ ( log ` y ) ) )
84 76 83 mpbid
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) <_ ( log ` y ) )
85 42 44 64 66 81 84 le2addd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) )
86 41 45 46 63 85 letrd
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) )
87 12 13 23 26 38 86 o1bddrp
 |-  ( T. -> E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ c )
88 87 mptru
 |-  E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ c