Metamath Proof Explorer

Theorem nnne1ge2

Description: A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion nnne1ge2 
|- ( ( N e. NN /\ N =/= 1 ) -> 2 <_ N )

Proof

Step Hyp Ref Expression
1 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
2 1 adantr 
 |-  ( ( N e. NN /\ N =/= 1 ) -> N e. NN0 )
3 nnne0 
 |-  ( N e. NN -> N =/= 0 )
4 3 adantr 
 |-  ( ( N e. NN /\ N =/= 1 ) -> N =/= 0 )
5 simpr 
 |-  ( ( N e. NN /\ N =/= 1 ) -> N =/= 1 )
6 nn0n0n1ge2 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> 2 <_ N )
7 2 4 5 6 syl3anc 
 |-  ( ( N e. NN /\ N =/= 1 ) -> 2 <_ N )