Metamath Proof Explorer

Theorem pczndvds

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

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

Proof

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