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