This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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