Metamath Proof Explorer

Theorem pczcl

Description: Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pczcl 
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) e. NN0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < ) = sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < )
2 1 pczpre 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) = sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < ) )
3 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
4 eqid 
 |-  { x e. NN0 | ( P ^ x ) || N } = { x e. NN0 | ( P ^ x ) || N }
5 4 1 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < ) e. NN0 /\ ( P ^ sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < ) ) || N ) )
6 3 5 sylan 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < ) e. NN0 /\ ( P ^ sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < ) ) || N ) )
7 6 simpld 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> sup ( { x e. NN0 | ( P ^ x ) || N } , RR , < ) e. NN0 )
8 2 7 eqeltrd 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) e. NN0 )