Description: 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | 1eluzge0 | |- 1 e. ( ZZ>= ` 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0z | |- 0 e. ZZ |
|
2 | 1z | |- 1 e. ZZ |
|
3 | 0le1 | |- 0 <_ 1 |
|
4 | eluz2 | |- ( 1 e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ 1 e. ZZ /\ 0 <_ 1 ) ) |
|
5 | 1 2 3 4 | mpbir3an | |- 1 e. ( ZZ>= ` 0 ) |