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

Metamath Proof Explorer

Theorem prmuz2

Description: A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Assertion prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2

Proof

Step Hyp Ref Expression
1 isprm4 ⊢ P ∈ ℙ ↔ P ∈ ℤ ≥ 2 ∧ ∀ x ∈ ℤ ≥ 2 x ∥ P → x = P
2 1 simplbi ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2