Metamath Proof Explorer

Theorem pczdvds

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

Ref Expression
Assertion pczdvds ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P P pCnt N ∥ 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 oveq2d ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P P pCnt N = P sup n ∈ ℕ 0 | P n ∥ N ℝ <
4 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
5 eqid ⊢ n ∈ ℕ 0 | P n ∥ N = n ∈ ℕ 0 | P n ∥ N
6 5 1 pcprecl ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → sup n ∈ ℕ 0 | P n ∥ N ℝ < ∈ ℕ 0 ∧ P sup n ∈ ℕ 0 | P n ∥ N ℝ < ∥ N
7 6 simprd ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → P sup n ∈ ℕ 0 | P n ∥ N ℝ < ∥ N
8 4 7 sylan ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P sup n ∈ ℕ 0 | P n ∥ N ℝ < ∥ N
9 3 8 eqbrtrd ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P P pCnt N ∥ N