Metamath Proof Explorer

Theorem 1nuz2

Description: 1 is not in ( ZZ>=2 ) . (Contributed by Paul Chapman, 21-Nov-2012)

Ref Expression
Assertion 1nuz2 
|- -. 1 e. ( ZZ>= ` 2 )

Proof

Step Hyp Ref Expression
1 neirr 
 |-  -. 1 =/= 1
2 eluz2b3 
 |-  ( 1 e. ( ZZ>= ` 2 ) <-> ( 1 e. NN /\ 1 =/= 1 ) )
3 2 simprbi 
 |-  ( 1 e. ( ZZ>= ` 2 ) -> 1 =/= 1 )
4 1 3 mto 
 |-  -. 1 e. ( ZZ>= ` 2 )