Theorem chp1

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

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

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		chpval	⊢ ( 1 ∈ ℝ → ( ψ ‘ 1 ) = Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 1 ) ) ( Λ ‘ 𝑥 ) )
3	1 2	ax-mp	⊢ ( ψ ‘ 1 ) = Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 1 ) ) ( Λ ‘ 𝑥 )
4		elfz1eq	⊢ ( 𝑥 ∈ ( 1 ... 1 ) → 𝑥 = 1 )
5	4	fveq2d	⊢ ( 𝑥 ∈ ( 1 ... 1 ) → ( Λ ‘ 𝑥 ) = ( Λ ‘ 1 ) )
6		vma1	⊢ ( Λ ‘ 1 ) = 0
7	5 6	eqtrdi	⊢ ( 𝑥 ∈ ( 1 ... 1 ) → ( Λ ‘ 𝑥 ) = 0 )
8		1z	⊢ 1 ∈ ℤ
9		flid	⊢ ( 1 ∈ ℤ → ( ⌊ ‘ 1 ) = 1 )
10	8 9	ax-mp	⊢ ( ⌊ ‘ 1 ) = 1
11	10	oveq2i	⊢ ( 1 ... ( ⌊ ‘ 1 ) ) = ( 1 ... 1 )
12	7 11	eleq2s	⊢ ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ 1 ) ) → ( Λ ‘ 𝑥 ) = 0 )
13	12	sumeq2i	⊢ Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 1 ) ) ( Λ ‘ 𝑥 ) = Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 1 ) ) 0
14		fzfi	⊢ ( 1 ... ( ⌊ ‘ 1 ) ) ∈ Fin
15	14	olci	⊢ ( ( 1 ... ( ⌊ ‘ 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ 1 ) ) ∈ Fin )
16		sumz	⊢ ( ( ( 1 ... ( ⌊ ‘ 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ 1 ) ) ∈ Fin ) → Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 1 ) ) 0 = 0 )
17	15 16	ax-mp	⊢ Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 1 ) ) 0 = 0
18	3 13 17	3eqtri	⊢ ( ψ ‘ 1 ) = 0