This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pczcl

Description: Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pczcl ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P pCnt N ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ sup x ∈ ℕ 0 | P x ∥ N ℝ < = sup x ∈ ℕ 0 | P x ∥ N ℝ <
2 1 pczpre ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P pCnt N = sup x ∈ ℕ 0 | P x ∥ N ℝ <
3 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
4 eqid ⊢ x ∈ ℕ 0 | P x ∥ N = x ∈ ℕ 0 | P x ∥ N
5 4 1 pcprecl ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → sup x ∈ ℕ 0 | P x ∥ N ℝ < ∈ ℕ 0 ∧ P sup x ∈ ℕ 0 | P x ∥ N ℝ < ∥ N
6 3 5 sylan ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → sup x ∈ ℕ 0 | P x ∥ N ℝ < ∈ ℕ 0 ∧ P sup x ∈ ℕ 0 | P x ∥ N ℝ < ∥ N
7 6 simpld ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → sup x ∈ ℕ 0 | P x ∥ N ℝ < ∈ ℕ 0
8 2 7 eqeltrd ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → P pCnt N ∈ ℕ 0