Metamath Proof Explorer

Theorem cht1

Description: The Chebyshev function at 1 . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion cht1 
|- ( theta ` 1 ) = 0

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 chtval 
 |-  ( 1 e. RR -> ( theta ` 1 ) = sum_ p e. ( ( 0 [,] 1 ) i^i Prime ) ( log ` p ) )
3 1 2 ax-mp 
 |-  ( theta ` 1 ) = sum_ p e. ( ( 0 [,] 1 ) i^i Prime ) ( log ` p )
4 ppisval 
 |-  ( 1 e. RR -> ( ( 0 [,] 1 ) i^i Prime ) = ( ( 2 ... ( |_ ` 1 ) ) i^i Prime ) )
5 1 4 ax-mp 
 |-  ( ( 0 [,] 1 ) i^i Prime ) = ( ( 2 ... ( |_ ` 1 ) ) i^i Prime )
6 1z 
 |-  1 e. ZZ
7 flid 
 |-  ( 1 e. ZZ -> ( |_ ` 1 ) = 1 )
8 6 7 ax-mp 
 |-  ( |_ ` 1 ) = 1
9 8 oveq2i 
 |-  ( 2 ... ( |_ ` 1 ) ) = ( 2 ... 1 )
10 1lt2 
 |-  1 < 2
11 2z 
 |-  2 e. ZZ
12 fzn 
 |-  ( ( 2 e. ZZ /\ 1 e. ZZ ) -> ( 1 < 2 <-> ( 2 ... 1 ) = (/) ) )
13 11 6 12 mp2an 
 |-  ( 1 < 2 <-> ( 2 ... 1 ) = (/) )
14 10 13 mpbi 
 |-  ( 2 ... 1 ) = (/)
15 9 14 eqtri 
 |-  ( 2 ... ( |_ ` 1 ) ) = (/)
16 15 ineq1i 
 |-  ( ( 2 ... ( |_ ` 1 ) ) i^i Prime ) = ( (/) i^i Prime )
17 0in 
 |-  ( (/) i^i Prime ) = (/)
18 5 16 17 3eqtri 
 |-  ( ( 0 [,] 1 ) i^i Prime ) = (/)
19 18 sumeq1i 
 |-  sum_ p e. ( ( 0 [,] 1 ) i^i Prime ) ( log ` p ) = sum_ p e. (/) ( log ` p )
20 sum0 
 |-  sum_ p e. (/) ( log ` p ) = 0
21 3 19 20 3eqtri 
 |-  ( theta ` 1 ) = 0