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 ) )