Metamath Proof Explorer


Theorem eluz2nn

Description: An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018)

Ref Expression
Assertion eluz2nn A 2 A

Proof

Step Hyp Ref Expression
1 1z 1
2 1le2 1 2
3 eluzuzle 1 1 2 A 2 A 1
4 1 2 3 mp2an A 2 A 1
5 nnuz = 1
6 4 5 eleqtrrdi A 2 A