Database
ELEMENTARY NUMBER THEORY
Elementary prime number theory
Elementary properties
prmssuz2
Next ⟩
prmgt1
Metamath Proof Explorer
Ascii
Unicode
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