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	$⊢ φ \to N \in ℕ$
	Assertion	hgt750lemc	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) < 1.03883 \cdot N$

Step	Hyp	Ref	Expression
1		hgt750lemc.n	$⊢ φ \to N \in ℕ$
2	1	nnzd	$⊢ φ \to N \in ℤ$
3		chpvalz	$⊢ N \in ℤ \to ψ (N) = \sum_{j = 1}^{N} Λ (j)$
4	2 3	syl	$⊢ φ \to ψ (N) = \sum_{j = 1}^{N} Λ (j)$
5		fveq2	$⊢ x = N \to ψ (x) = ψ (N)$
6		oveq2	$⊢ x = N \to 1.03883 x = 1.03883 \cdot N$
7	5 6	breq12d	$⊢ x = N \to (ψ (x) < 1.03883 x \leftrightarrow ψ (N) < 1.03883 \cdot N)$
8		ax-ros335	$⊢ \forall x \in ℝ^{+} ψ (x) < 1.03883 x$
9	8	a1i	$⊢ φ \to \forall x \in ℝ^{+} ψ (x) < 1.03883 x$
10	1	nnrpd	$⊢ φ \to N \in ℝ^{+}$
11	7 9 10	rspcdva	$⊢ φ \to ψ (N) < 1.03883 \cdot N$
12	4 11	eqbrtrrd	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) < 1.03883 \cdot N$

Metamath Proof Explorer