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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
3	1 2	jca	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) )
4		pczndvds2	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
5	3 4	sylan2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )