Metamath Proof Explorer

Theorem eluz2gt1

Description: An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020)

Ref Expression
Assertion eluz2gt1 
|- ( N e. ( ZZ>= ` 2 ) -> 1 < N )

Proof

Step Hyp Ref Expression
1 eluz2b1 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) )
2 1 simprbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )