Metamath Proof Explorer

Theorem pczndvds2

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

Ref Expression
Assertion pczndvds2 ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → ¬ P ∥ N P P pCnt N

Proof

Step Hyp Ref Expression
1 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
2 eqid ⊢ n ∈ ℕ 0 | P n ∥ N = n ∈ ℕ 0 | P n ∥ N
3 eqid ⊢ sup n ∈ ℕ 0 | P n ∥ N ℝ < = sup n ∈ ℕ 0 | P n ∥ N ℝ <
4 2 3 pcprendvds2 ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → ¬ P ∥ N P sup n ∈ ℕ 0 | P n ∥ N ℝ <
5 1 4 sylan ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → ¬ P ∥ N P sup n ∈ ℕ 0 | P n ∥ N ℝ <
6 3 pczpre ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P pCnt N = sup n ∈ ℕ 0 | P n ∥ N ℝ <
7 6 oveq2d ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P P pCnt N = P sup n ∈ ℕ 0 | P n ∥ N ℝ <
8 7 oveq2d ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → N P P pCnt N = N P sup n ∈ ℕ 0 | P n ∥ N ℝ <
9 8 breq2d ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P ∥ N P P pCnt N ↔ P ∥ N P sup n ∈ ℕ 0 | P n ∥ N ℝ <
10 5 9 mtbird ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → ¬ P ∥ N P P pCnt N