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