Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0n0n1ge2 Structured version   Unicode version

Theorem nn0n0n1ge2 10282
 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.)
Assertion
Ref Expression
nn0n0n1ge2

Proof of Theorem nn0n0n1ge2
StepHypRef Expression
1 nn0cn 10233 . . . . . 6
2 ax-1cn 9050 . . . . . . 7
32a1i 11 . . . . . 6
41, 3, 3subsub4d 9444 . . . . 5
5 1p1e2 10096 . . . . . 6
65oveq2i 6094 . . . . 5
74, 6syl6req 2487 . . . 4
9 3simpa 955 . . . . . . 7
10 elnnne0 10237 . . . . . . 7
119, 10sylibr 205 . . . . . 6
12 nnm1nn0 10263 . . . . . 6
1311, 12syl 16 . . . . 5
141, 3subeq0ad 9423 . . . . . . . . 9
1514biimpd 200 . . . . . . . 8
1615necon3d 2641 . . . . . . 7
1716imp 420 . . . . . 6
18173adant2 977 . . . . 5
19 elnnne0 10237 . . . . 5
2013, 18, 19sylanbrc 647 . . . 4
21 nnm1nn0 10263 . . . 4
2220, 21syl 16 . . 3
238, 22eqeltrd 2512 . 2
24 2nn0 10240 . . . . 5
2524jctl 527 . . . 4