Description: A 1-based finite set of sequential integers is empty iff it ends at index 0 . (Contributed by Paul Chapman, 22-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | fz1n | |- ( N e. NN0 -> ( ( 1 ... N ) = (/) <-> N = 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1z | |- 1 e. ZZ |
|
2 | nn0z | |- ( N e. NN0 -> N e. ZZ ) |
|
3 | fzn | |- ( ( 1 e. ZZ /\ N e. ZZ ) -> ( N < 1 <-> ( 1 ... N ) = (/) ) ) |
|
4 | 1 2 3 | sylancr | |- ( N e. NN0 -> ( N < 1 <-> ( 1 ... N ) = (/) ) ) |
5 | nn0lt10b | |- ( N e. NN0 -> ( N < 1 <-> N = 0 ) ) |
|
6 | 4 5 | bitr3d | |- ( N e. NN0 -> ( ( 1 ... N ) = (/) <-> N = 0 ) ) |