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	$$⊢\left(P\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to \neg P\parallel \left(\frac{N}{P^{P\mathrm{pCnt}N}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
2		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
3	1 2	jca	$$⊢N\in \mathbb{N}\to \left(N\in \mathbb{Z}\wedge N\ne 0\right)$$
4		pczndvds2	$$⊢\left(P\in \mathbb{P}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \neg P\parallel \left(\frac{N}{P^{P\mathrm{pCnt}N}}\right)$$
5	3 4	sylan2	$$⊢\left(P\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to \neg P\parallel \left(\frac{N}{P^{P\mathrm{pCnt}N}}\right)$$