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

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 ⊢ ( 𝑎 ∈ ℙ → 𝑎 ∈ ( ℤ≥ ‘ 2 ) )
2 1 ssriv ⊢ ℙ ⊆ ( ℤ≥ ‘ 2 )