cht1

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

		Ref	Expression
	Assertion	cht1	$⊢ θ (1) = 0$

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

Metamath Proof Explorer