Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | prmnn | ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isprm | ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ℕ ∧ { 𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃 } ≈ 2o ) ) | |
2 | 1 | simplbi | ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |