Theorem pccl

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

	Ref	Expression
Assertion	pccl	|- ( ( P e. Prime /\ N e. NN ) -> ( P pCnt N ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		nnz	|- ( N e. NN -> N e. ZZ )
2		nnne0	|- ( N e. NN -> N =/= 0 )
3	1 2	jca	|- ( N e. NN -> ( N e. ZZ /\ N =/= 0 ) )
4		pczcl	|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) e. NN0 )
5	3 4	sylan2	|- ( ( P e. Prime /\ N e. NN ) -> ( P pCnt N ) e. NN0 )