Metamath Proof Explorer

Theorem pczdvds

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

Ref Expression
Assertion pczdvds 
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( P pCnt N ) ) || 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 oveq2d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( P pCnt N ) ) = ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) )
4 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
5 eqid 
 |-  { n e. NN0 | ( P ^ n ) || N } = { n e. NN0 | ( P ^ n ) || N }
6 5 1 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) e. NN0 /\ ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) || N ) )
7 6 simprd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) || N )
8 4 7 sylan 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < ) ) || N )
9 3 8 eqbrtrd 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( P pCnt N ) ) || N )