Theorem pcndvds2

Description: The remainder after dividing out all factors of P is not divisible by P . (Contributed by Mario Carneiro, 23-Feb-2014)

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