This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0n0n1ge2

Description: A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017)

Ref Expression
Assertion nn0n0n1ge2 
|- ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> 2 <_ N )

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
2 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
3 1 2 2 subsub4d 
 |-  ( N e. NN0 -> ( ( N - 1 ) - 1 ) = ( N - ( 1 + 1 ) ) )
4 1p1e2 
 |-  ( 1 + 1 ) = 2
5 4 oveq2i 
 |-  ( N - ( 1 + 1 ) ) = ( N - 2 )
6 3 5 eqtr2di 
 |-  ( N e. NN0 -> ( N - 2 ) = ( ( N - 1 ) - 1 ) )
7 6 3ad2ant1 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( N - 2 ) = ( ( N - 1 ) - 1 ) )
8 3simpa 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( N e. NN0 /\ N =/= 0 ) )
9 elnnne0 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
10 8 9 sylibr 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> N e. NN )
11 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
12 10 11 syl 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( N - 1 ) e. NN0 )
13 1 2 subeq0ad 
 |-  ( N e. NN0 -> ( ( N - 1 ) = 0 <-> N = 1 ) )
14 13 biimpd 
 |-  ( N e. NN0 -> ( ( N - 1 ) = 0 -> N = 1 ) )
15 14 necon3d 
 |-  ( N e. NN0 -> ( N =/= 1 -> ( N - 1 ) =/= 0 ) )
16 15 imp 
 |-  ( ( N e. NN0 /\ N =/= 1 ) -> ( N - 1 ) =/= 0 )
17 16 3adant2 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( N - 1 ) =/= 0 )
18 elnnne0 
 |-  ( ( N - 1 ) e. NN <-> ( ( N - 1 ) e. NN0 /\ ( N - 1 ) =/= 0 ) )
19 12 17 18 sylanbrc 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( N - 1 ) e. NN )
20 nnm1nn0 
 |-  ( ( N - 1 ) e. NN -> ( ( N - 1 ) - 1 ) e. NN0 )
21 19 20 syl 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( ( N - 1 ) - 1 ) e. NN0 )
22 7 21 eqeltrd 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( N - 2 ) e. NN0 )
23 2nn0 
 |-  2 e. NN0
24 23 jctl 
 |-  ( N e. NN0 -> ( 2 e. NN0 /\ N e. NN0 ) )
25 24 3ad2ant1 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( 2 e. NN0 /\ N e. NN0 ) )
26 nn0sub 
 |-  ( ( 2 e. NN0 /\ N e. NN0 ) -> ( 2 <_ N <-> ( N - 2 ) e. NN0 ) )
27 25 26 syl 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> ( 2 <_ N <-> ( N - 2 ) e. NN0 ) )
28 22 27 mpbird 
 |-  ( ( N e. NN0 /\ N =/= 0 /\ N =/= 1 ) -> 2 <_ N )