Theorem 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 \theta \left(A\right)\le \psi \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$$⊢A\in ℝ\to \left(1\dots ⌊A⌋\right)\in \mathrm{Fin}$$
2		elfznn	$$⊢n\in \left(1\dots ⌊A⌋\right)\to n\in \mathbb{N}$$
3	2	adantl	$$⊢\left(A\in ℝ\wedge n\in \left(1\dots ⌊A⌋\right)\right)\to n\in \mathbb{N}$$
4		vmacl	$$⊢n\in \mathbb{N}\to \Lambda \left(n\right)\in ℝ$$
5	3 4	syl	$$⊢\left(A\in ℝ\wedge n\in \left(1\dots ⌊A⌋\right)\right)\to \Lambda \left(n\right)\in ℝ$$
6		vmage0	$$⊢n\in \mathbb{N}\to 0\le \Lambda \left(n\right)$$
7	3 6	syl	$$⊢\left(A\in ℝ\wedge n\in \left(1\dots ⌊A⌋\right)\right)\to 0\le \Lambda \left(n\right)$$
8		ppisval	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}=\left(2\dots ⌊A⌋\right)\cap \mathbb{P}$$
9		inss1	$$⊢\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\subseteq \left(2\dots ⌊A⌋\right)$$
10		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
11		fzss1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to \left(2\dots ⌊A⌋\right)\subseteq \left(1\dots ⌊A⌋\right)$$
12	10 11	mp1i	$$⊢A\in ℝ\to \left(2\dots ⌊A⌋\right)\subseteq \left(1\dots ⌊A⌋\right)$$
13	9 12	sstrid	$$⊢A\in ℝ\to \left(2\dots ⌊A⌋\right)\cap \mathbb{P}\subseteq \left(1\dots ⌊A⌋\right)$$
14	8 13	eqsstrd	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}\subseteq \left(1\dots ⌊A⌋\right)$$
15	1 5 7 14	fsumless	$$⊢A\in ℝ\to \sum _{n\in \left[0,A\right]\cap \mathbb{P}}\Lambda \left(n\right)\le \sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)$$
16		chtval	$$⊢A\in ℝ\to \theta \left(A\right)=\sum _{n\in \left[0,A\right]\cap \mathbb{P}}\log n$$
17		simpr	$$⊢\left(A\in ℝ\wedge n\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to n\in \left(\left[0,A\right]\cap \mathbb{P}\right)$$
18	17	elin2d	$$⊢\left(A\in ℝ\wedge n\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to n\in \mathbb{P}$$
19		vmaprm	$$⊢n\in \mathbb{P}\to \Lambda \left(n\right)=\log n$$
20	18 19	syl	$$⊢\left(A\in ℝ\wedge n\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to \Lambda \left(n\right)=\log n$$
21	20	sumeq2dv	$$⊢A\in ℝ\to \sum _{n\in \left[0,A\right]\cap \mathbb{P}}\Lambda \left(n\right)=\sum _{n\in \left[0,A\right]\cap \mathbb{P}}\log n$$
22	16 21	eqtr4d	$$⊢A\in ℝ\to \theta \left(A\right)=\sum _{n\in \left[0,A\right]\cap \mathbb{P}}\Lambda \left(n\right)$$
23		chpval	$$⊢A\in ℝ\to \psi \left(A\right)=\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)$$
24	15 22 23	3brtr4d	$$⊢A\in ℝ\to \theta \left(A\right)\le \psi \left(A\right)$$