Theorem cht1

Description: The Chebyshev function at 1 . (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	cht1	$$⊢\theta \left(1\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		chtval	$$⊢1\in ℝ\to \theta \left(1\right)=\sum _{p\in \left[0,1\right]\cap \mathbb{P}}\log p$$
3	1 2	ax-mp	$$⊢\theta \left(1\right)=\sum _{p\in \left[0,1\right]\cap \mathbb{P}}\log p$$
4		ppisval	$$⊢1\in ℝ\to \left[0,1\right]\cap \mathbb{P}=\left(2\dots ⌊1⌋\right)\cap \mathbb{P}$$
5	1 4	ax-mp	$$⊢\left[0,1\right]\cap \mathbb{P}=\left(2\dots ⌊1⌋\right)\cap \mathbb{P}$$
6		1z	$$⊢1\in \mathbb{Z}$$
7		flid	$$⊢1\in \mathbb{Z}\to ⌊1⌋=1$$
8	6 7	ax-mp	$$⊢⌊1⌋=1$$
9	8	oveq2i	$$⊢\left(2\dots ⌊1⌋\right)=\left(2\dots 1\right)$$
10		1lt2	$$⊢1<2$$
11		2z	$$⊢2\in \mathbb{Z}$$
12		fzn	$$⊢\left(2\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to \left(1<2\leftrightarrow \left(2\dots 1\right)=\varnothing \right)$$
13	11 6 12	mp2an	$$⊢1<2\leftrightarrow \left(2\dots 1\right)=\varnothing$$
14	10 13	mpbi	$$⊢\left(2\dots 1\right)=\varnothing$$
15	9 14	eqtri	$$⊢\left(2\dots ⌊1⌋\right)=\varnothing$$
16	15	ineq1i	$$⊢\left(2\dots ⌊1⌋\right)\cap \mathbb{P}=\varnothing \cap \mathbb{P}$$
17		0in	$$⊢\varnothing \cap \mathbb{P}=\varnothing$$
18	5 16 17	3eqtri	$$⊢\left[0,1\right]\cap \mathbb{P}=\varnothing$$
19	18	sumeq1i	$$⊢\sum _{p\in \left[0,1\right]\cap \mathbb{P}}\log p=\sum _{p\in \varnothing }\log p$$
20		sum0	$$⊢\sum _{p\in \varnothing }\log p=0$$
21	3 19 20	3eqtri	$$⊢\theta \left(1\right)=0$$