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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
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 ) · 𝑁 ) )