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 ( 𝜑𝑁 ∈ ℕ )
Assertion hgt750lemc ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) )

Proof

Step Hyp Ref Expression
1 hgt750lemc.n ( 𝜑𝑁 ∈ ℕ )
2 1 nnzd ( 𝜑𝑁 ∈ ℤ )
3 chpvalz ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) )
4 2 3 syl ( 𝜑 → ( ψ ‘ 𝑁 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) )
5 fveq2 ( 𝑥 = 𝑁 → ( ψ ‘ 𝑥 ) = ( ψ ‘ 𝑁 ) )
6 oveq2 ( 𝑥 = 𝑁 → ( ( 1 . 0 3 8 8 3 ) · 𝑥 ) = ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) )
7 5 6 breq12d ( 𝑥 = 𝑁 → ( ( ψ ‘ 𝑥 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑥 ) ↔ ( ψ ‘ 𝑁 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) )
8 ax-ros335 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑥 )
9 8 a1i ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑥 ) )
10 1 nnrpd ( 𝜑𝑁 ∈ ℝ+ )
11 7 9 10 rspcdva ( 𝜑 → ( ψ ‘ 𝑁 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) )
12 4 11 eqbrtrrd ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) )