chtlepsi

Description: The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016)

		Ref	Expression
	Assertion	chtlepsi	$⊢ A \in ℝ \to θ (A) \leq ψ (A)$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ A \in ℝ \to (1 \dots ⌊A⌋) \in Fin$
2		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
3	2	adantl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
4		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
5	3 4	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \in ℝ$
6		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
7	3 6	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to 0 \leq Λ (n)$
8		ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
9		inss1	$⊢ (2 \dots ⌊A⌋) \cap ℙ \subseteq (2 \dots ⌊A⌋)$
10		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
11		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots ⌊A⌋) \subseteq (1 \dots ⌊A⌋)$
12	10 11	mp1i	$⊢ A \in ℝ \to (2 \dots ⌊A⌋) \subseteq (1 \dots ⌊A⌋)$
13	9 12	sstrid	$⊢ A \in ℝ \to (2 \dots ⌊A⌋) \cap ℙ \subseteq (1 \dots ⌊A⌋)$
14	8 13	eqsstrd	$⊢ A \in ℝ \to [0, A] \cap ℙ \subseteq (1 \dots ⌊A⌋)$
15	1 5 7 14	fsumless	$⊢ A \in ℝ \to \sum_{n \in [0, A] \cap ℙ} Λ (n) \leq \sum_{n = 1}^{⌊A⌋} Λ (n)$
16		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{n \in [0, A] \cap ℙ} \log n$
17		simpr	$⊢ (A \in ℝ \land n \in ([0, A] \cap ℙ)) \to n \in ([0, A] \cap ℙ)$
18	17	elin2d	$⊢ (A \in ℝ \land n \in ([0, A] \cap ℙ)) \to n \in ℙ$
19		vmaprm	$⊢ n \in ℙ \to Λ (n) = \log n$
20	18 19	syl	$⊢ (A \in ℝ \land n \in ([0, A] \cap ℙ)) \to Λ (n) = \log n$
21	20	sumeq2dv	$⊢ A \in ℝ \to \sum_{n \in [0, A] \cap ℙ} Λ (n) = \sum_{n \in [0, A] \cap ℙ} \log n$
22	16 21	eqtr4d	$⊢ A \in ℝ \to θ (A) = \sum_{n \in [0, A] \cap ℙ} Λ (n)$
23		chpval	$⊢ A \in ℝ \to ψ (A) = \sum_{n = 1}^{⌊A⌋} Λ (n)$
24	15 22 23	3brtr4d	$⊢ A \in ℝ \to θ (A) \leq ψ (A)$

Metamath Proof Explorer

Theorem chtlepsi

Proof