Metamath Proof Explorer


Theorem prmssuz2

Description: The primes are integers greater than 1. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion prmssuz2 ⊢ ℙ ⊆ ℤ ≥ 2

Proof

Step Hyp Ref Expression
1 prmuz2 ⊢ a ∈ ℙ → a ∈ ℤ ≥ 2
2 1 ssriv ⊢ ℙ ⊆ ℤ ≥ 2