Metamath Proof Explorer


Theorem nn0lt2

Description: A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018)

Ref Expression
Assertion nn0lt2 N 0 N < 2 N = 0 N = 1

Proof

Step Hyp Ref Expression
1 olc N = 1 N = 0 N = 1
2 1 a1d N = 1 N 0 N < 2 N = 0 N = 1
3 nn0z N 0 N
4 2z 2
5 zltlem1 N 2 N < 2 N 2 1
6 3 4 5 sylancl N 0 N < 2 N 2 1
7 2m1e1 2 1 = 1
8 7 breq2i N 2 1 N 1
9 6 8 bitrdi N 0 N < 2 N 1
10 necom N 1 1 N
11 nn0re N 0 N
12 1re 1
13 ltlen N 1 N < 1 N 1 1 N
14 11 12 13 sylancl N 0 N < 1 N 1 1 N
15 nn0lt10b N 0 N < 1 N = 0
16 15 biimpa N 0 N < 1 N = 0
17 16 orcd N 0 N < 1 N = 0 N = 1
18 17 ex N 0 N < 1 N = 0 N = 1
19 14 18 sylbird N 0 N 1 1 N N = 0 N = 1
20 19 expd N 0 N 1 1 N N = 0 N = 1
21 10 20 syl7bi N 0 N 1 N 1 N = 0 N = 1
22 9 21 sylbid N 0 N < 2 N 1 N = 0 N = 1
23 22 imp N 0 N < 2 N 1 N = 0 N = 1
24 23 com12 N 1 N 0 N < 2 N = 0 N = 1
25 2 24 pm2.61ine N 0 N < 2 N = 0 N = 1