Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nn0n0n1ge2 Unicode version

Theorem nn0n0n1ge2 8311
 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 8191 . . . . . 6
2 1cnd 7043 . . . . . 6
31, 2, 2subsub4d 7353 . . . . 5
4 1p1e2 8033 . . . . . 6
54oveq2i 5523 . . . . 5
63, 5syl6req 2089 . . . 4
8 3simpa 901 . . . . . . 7
9 elnnne0 8195 . . . . . . 7
108, 9sylibr 137 . . . . . 6
11 nnm1nn0 8223 . . . . . 6
1210, 11syl 14 . . . . 5
131, 2subeq0ad 7332 . . . . . . . . 9
1413biimpd 132 . . . . . . . 8
1514necon3d 2249 . . . . . . 7
1615imp 115 . . . . . 6
17163adant2 923 . . . . 5
18 elnnne0 8195 . . . . 5
1912, 17, 18sylanbrc 394 . . . 4
20 nnm1nn0 8223 . . . 4
2119, 20syl 14 . . 3
227, 21eqeltrd 2114 . 2
23 2nn0 8198 . . . . 5
2423jctl 297 . . . 4