This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hgt750lemc

Description: An upper bound to the summatory function of the von Mangoldt function. (Contributed by Thierry Arnoux, 29-Dec-2021)

Ref Expression
Hypothesis hgt750lemc.n 
|- ( ph -> N e. NN )
Assertion hgt750lemc 
|- ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) )

Proof

Step Hyp Ref Expression
1 hgt750lemc.n 
 |-  ( ph -> N e. NN )
2 1 nnzd 
 |-  ( ph -> N e. ZZ )
3 chpvalz 
 |-  ( N e. ZZ -> ( psi ` N ) = sum_ j e. ( 1 ... N ) ( Lam ` j ) )
4 2 3 syl 
 |-  ( ph -> ( psi ` N ) = sum_ j e. ( 1 ... N ) ( Lam ` j ) )
5 fveq2 
 |-  ( x = N -> ( psi ` x ) = ( psi ` N ) )
6 oveq2 
 |-  ( x = N -> ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x ) = ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) )
7 5 6 breq12d 
 |-  ( x = N -> ( ( psi ` x ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x ) <-> ( psi ` N ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) )
8 ax-ros335 
 |-  A. x e. RR+ ( psi ` x ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x )
9 8 a1i 
 |-  ( ph -> A. x e. RR+ ( psi ` x ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x ) )
10 1 nnrpd 
 |-  ( ph -> N e. RR+ )
11 7 9 10 rspcdva 
 |-  ( ph -> ( psi ` N ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) )
12 4 11 eqbrtrrd 
 |-  ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) )