Metamath Proof Explorer

Theorem pczndvds

Description: Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion pczndvds 
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < )
2 1 pczpre 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) )
3 2 oveq1d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P pCnt N ) + 1 ) = ( sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) + 1 ) )
4 3 oveq2d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( ( P pCnt N ) + 1 ) ) = ( P ^ ( sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) + 1 ) ) )
5 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
6 eqid 
 |-  { n e. NN0 | ( P ^ n ) || N } = { n e. NN0 | ( P ^ n ) || N }
7 6 1 pcprendvds 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) + 1 ) ) || N )
8 5 7 sylan 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) + 1 ) ) || N )
9 4 8 eqnbrtrd 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )