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