Theorem chp1

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

	Ref	Expression
Assertion	chp1	$$⊢\psi \left(1\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		chpval	$$⊢1\in ℝ\to \psi \left(1\right)=\sum _{x=1}^{⌊1⌋}\Lambda \left(x\right)$$
3	1 2	ax-mp	$$⊢\psi \left(1\right)=\sum _{x=1}^{⌊1⌋}\Lambda \left(x\right)$$
4		elfz1eq	$$⊢x\in \left(1\dots 1\right)\to x=1$$
5	4	fveq2d	$$⊢x\in \left(1\dots 1\right)\to \Lambda \left(x\right)=\Lambda \left(1\right)$$
6		vma1	$$⊢\Lambda \left(1\right)=0$$
7	5 6	syl6eq	$$⊢x\in \left(1\dots 1\right)\to \Lambda \left(x\right)=0$$
8		1z	$$⊢1\in \mathbb{Z}$$
9		flid	$$⊢1\in \mathbb{Z}\to ⌊1⌋=1$$
10	8 9	ax-mp	$$⊢⌊1⌋=1$$
11	10	oveq2i	$$⊢\left(1\dots ⌊1⌋\right)=\left(1\dots 1\right)$$
12	7 11	eleq2s	$$⊢x\in \left(1\dots ⌊1⌋\right)\to \Lambda \left(x\right)=0$$
13	12	sumeq2i	$$⊢\sum _{x=1}^{⌊1⌋}\Lambda \left(x\right)=\sum _{x=1}^{⌊1⌋}0$$
14		fzfi	$$⊢\left(1\dots ⌊1⌋\right)\in \mathrm{Fin}$$
15	14	olci	$$⊢\left(\left(1\dots ⌊1⌋\right)\subseteq {\mathbb{Z}}_{\ge 1}\vee \left(1\dots ⌊1⌋\right)\in \mathrm{Fin}\right)$$
16		sumz	$$⊢\left(\left(1\dots ⌊1⌋\right)\subseteq {\mathbb{Z}}_{\ge 1}\vee \left(1\dots ⌊1⌋\right)\in \mathrm{Fin}\right)\to \sum _{x=1}^{⌊1⌋}0=0$$
17	15 16	ax-mp	$$⊢\sum _{x=1}^{⌊1⌋}0=0$$
18	3 13 17	3eqtri	$$⊢\psi \left(1\right)=0$$