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 = x = 1 1 Λ x
3 1 2 ax-mp ψ 1 = x = 1 1 Λ x
4 elfz1eq x 1 1 x = 1
5 4 fveq2d x 1 1 Λ x = Λ 1
6 vma1 Λ 1 = 0
7 5 6 eqtrdi x 1 1 Λ x = 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 x 1 1 Λ x = 0
13 12 sumeq2i x = 1 1 Λ x = x = 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 x = 1 1 0 = 0
17 15 16 ax-mp x = 1 1 0 = 0
18 3 13 17 3eqtri ψ 1 = 0