Metamath Proof Explorer


Theorem eluz4nn

Description: An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023)

Ref Expression
Assertion eluz4nn X 4 X

Proof

Step Hyp Ref Expression
1 eluz4eluz2 X 4 X 2
2 eluz2nn X 2 X
3 1 2 syl X 4 X