Theorem pcndvds

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

	Ref	Expression
Assertion	pcndvds	|- ( ( P e. Prime /\ N e. NN ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || 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		pczndvds	|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )
5	3 4	sylan2	|- ( ( P e. Prime /\ N e. NN ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )