Metamath Proof Explorer

Theorem ppi1

Description: The prime-counting function ppi at 1 . (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion ppi1 
|- ( ppi ` 1 ) = 0

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 ppival2 
 |-  ( 1 e. ZZ -> ( ppi ` 1 ) = ( # ` ( ( 2 ... 1 ) i^i Prime ) ) )
3 1 2 ax-mp 
 |-  ( ppi ` 1 ) = ( # ` ( ( 2 ... 1 ) i^i Prime ) )
4 1lt2 
 |-  1 < 2
5 2z 
 |-  2 e. ZZ
6 fzn 
 |-  ( ( 2 e. ZZ /\ 1 e. ZZ ) -> ( 1 < 2 <-> ( 2 ... 1 ) = (/) ) )
7 5 1 6 mp2an 
 |-  ( 1 < 2 <-> ( 2 ... 1 ) = (/) )
8 4 7 mpbi 
 |-  ( 2 ... 1 ) = (/)
9 8 ineq1i 
 |-  ( ( 2 ... 1 ) i^i Prime ) = ( (/) i^i Prime )
10 0in 
 |-  ( (/) i^i Prime ) = (/)
11 9 10 eqtri 
 |-  ( ( 2 ... 1 ) i^i Prime ) = (/)
12 11 fveq2i 
 |-  ( # ` ( ( 2 ... 1 ) i^i Prime ) ) = ( # ` (/) )
13 hash0 
 |-  ( # ` (/) ) = 0
14 12 13 eqtri 
 |-  ( # ` ( ( 2 ... 1 ) i^i Prime ) ) = 0
15 3 14 eqtri 
 |-  ( ppi ` 1 ) = 0