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 ⊢ φ → N ∈ ℕ
Assertion hgt750lemc ⊢ φ → ∑ j = 1 N Λ ⁡ j < 1.03883 ⋅ N

Proof

Step Hyp Ref Expression
1 hgt750lemc.n ⊢ φ → N ∈ ℕ
2 1 nnzd ⊢ φ → N ∈ ℤ
3 chpvalz ⊢ N ∈ ℤ → ψ ⁡ N = ∑ j = 1 N Λ ⁡ j
4 2 3 syl ⊢ φ → ψ ⁡ N = ∑ j = 1 N Λ ⁡ j
5 fveq2 ⊢ x = N → ψ ⁡ x = ψ ⁡ N
6 oveq2 ⊢ x = N → 1.03883 ⁢ x = 1.03883 ⋅ N
7 5 6 breq12d ⊢ x = N → ψ ⁡ x < 1.03883 ⁢ x ↔ ψ ⁡ N < 1.03883 ⋅ N
8 ax-ros335 ⊢ ∀ x ∈ ℝ + ψ ⁡ x < 1.03883 ⁢ x
9 8 a1i ⊢ φ → ∀ x ∈ ℝ + ψ ⁡ x < 1.03883 ⁢ x
10 1 nnrpd ⊢ φ → N ∈ ℝ +
11 7 9 10 rspcdva ⊢ φ → ψ ⁡ N < 1.03883 ⋅ N
12 4 11 eqbrtrrd ⊢ φ → ∑ j = 1 N Λ ⁡ j < 1.03883 ⋅ N