Metamath Proof Explorer

Theorem pc1

Description: Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pc1 
|- ( P e. Prime -> ( P pCnt 1 ) = 0 )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 ax-1ne0 
 |-  1 =/= 0
3 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < )
4 3 pczpre 
 |-  ( ( P e. Prime /\ ( 1 e. ZZ /\ 1 =/= 0 ) ) -> ( P pCnt 1 ) = sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) )
5 1 2 4 mpanr12 
 |-  ( P e. Prime -> ( P pCnt 1 ) = sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) )
6 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
7 eqid 
 |-  1 = 1
8 eqid 
 |-  { n e. NN0 | ( P ^ n ) || 1 } = { n e. NN0 | ( P ^ n ) || 1 }
9 8 3 pcpre1 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ 1 = 1 ) -> sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) = 0 )
10 6 7 9 sylancl 
 |-  ( P e. Prime -> sup ( { n e. NN0 | ( P ^ n ) || 1 } , RR , < ) = 0 )
11 5 10 eqtrd 
 |-  ( P e. Prime -> ( P pCnt 1 ) = 0 )