Metamath Proof Explorer

Theorem chp1

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

Ref Expression
Assertion chp1 
|- ( psi ` 1 ) = 0

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 chpval 
 |-  ( 1 e. RR -> ( psi ` 1 ) = sum_ x e. ( 1 ... ( |_ ` 1 ) ) ( Lam ` x ) )
3 1 2 ax-mp 
 |-  ( psi ` 1 ) = sum_ x e. ( 1 ... ( |_ ` 1 ) ) ( Lam ` x )
4 elfz1eq 
 |-  ( x e. ( 1 ... 1 ) -> x = 1 )
5 4 fveq2d 
 |-  ( x e. ( 1 ... 1 ) -> ( Lam ` x ) = ( Lam ` 1 ) )
6 vma1 
 |-  ( Lam ` 1 ) = 0
7 5 6 eqtrdi 
 |-  ( x e. ( 1 ... 1 ) -> ( Lam ` x ) = 0 )
8 1z 
 |-  1 e. ZZ
9 flid 
 |-  ( 1 e. ZZ -> ( |_ ` 1 ) = 1 )
10 8 9 ax-mp 
 |-  ( |_ ` 1 ) = 1
11 10 oveq2i 
 |-  ( 1 ... ( |_ ` 1 ) ) = ( 1 ... 1 )
12 7 11 eleq2s 
 |-  ( x e. ( 1 ... ( |_ ` 1 ) ) -> ( Lam ` x ) = 0 )
13 12 sumeq2i 
 |-  sum_ x e. ( 1 ... ( |_ ` 1 ) ) ( Lam ` x ) = sum_ x e. ( 1 ... ( |_ ` 1 ) ) 0
14 fzfi 
 |-  ( 1 ... ( |_ ` 1 ) ) e. Fin
15 14 olci 
 |-  ( ( 1 ... ( |_ ` 1 ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` 1 ) ) e. Fin )
16 sumz 
 |-  ( ( ( 1 ... ( |_ ` 1 ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` 1 ) ) e. Fin ) -> sum_ x e. ( 1 ... ( |_ ` 1 ) ) 0 = 0 )
17 15 16 ax-mp 
 |-  sum_ x e. ( 1 ... ( |_ ` 1 ) ) 0 = 0
18 3 13 17 3eqtri 
 |-  ( psi ` 1 ) = 0