chp1

Description: The second Chebyshev function at 1 . (Contributed by Mario Carneiro, 9-Apr-2016)

		Ref	Expression
	Assertion	chp1	$⊢ ψ (1) = 0$

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		chpval	$⊢ 1 \in ℝ \to ψ (1) = \sum_{x = 1}^{⌊1⌋} Λ (x)$
3	1 2	ax-mp	$⊢ ψ (1) = \sum_{x = 1}^{⌊1⌋} Λ (x)$
4		elfz1eq	$⊢ x \in (1 \dots 1) \to x = 1$
5	4	fveq2d	$⊢ x \in (1 \dots 1) \to Λ (x) = Λ (1)$
6		vma1	$⊢ Λ (1) = 0$
7	5 6	eqtrdi	$⊢ x \in (1 \dots 1) \to Λ (x) = 0$
8		1z	$⊢ 1 \in ℤ$
9		flid	$⊢ 1 \in ℤ \to ⌊1⌋ = 1$
10	8 9	ax-mp	$⊢ ⌊1⌋ = 1$
11	10	oveq2i	$⊢ (1 \dots ⌊1⌋) = (1 \dots 1)$
12	7 11	eleq2s	$⊢ x \in (1 \dots ⌊1⌋) \to Λ (x) = 0$
13	12	sumeq2i	$⊢ \sum_{x = 1}^{⌊1⌋} Λ (x) = \sum_{x = 1}^{⌊1⌋} 0$
14		fzfi	$⊢ (1 \dots ⌊1⌋) \in Fin$
15	14	olci	$⊢ ((1 \dots ⌊1⌋) \subseteq ℤ_{\geq 1} \lor (1 \dots ⌊1⌋) \in Fin)$
16		sumz	$⊢ ((1 \dots ⌊1⌋) \subseteq ℤ_{\geq 1} \lor (1 \dots ⌊1⌋) \in Fin) \to \sum_{x = 1}^{⌊1⌋} 0 = 0$
17	15 16	ax-mp	$⊢ \sum_{x = 1}^{⌊1⌋} 0 = 0$
18	3 13 17	3eqtri	$⊢ ψ (1) = 0$

Metamath Proof Explorer