Theorem pcdvds

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

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

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		pczdvds	|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( P pCnt N ) ) || N )
5	3 4	sylan2	|- ( ( P e. Prime /\ N e. NN ) -> ( P ^ ( P pCnt N ) ) || N )