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 )