Description: An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018) (Proof shortened by OpenAI, 25-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | elfz0add | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0z | |
|
2 | uzid | |
|
3 | 1 2 | syl | |
4 | uzaddcl | |
|
5 | 3 4 | sylan | |
6 | fzss2 | |
|
7 | 5 6 | syl | |
8 | 7 | sseld | |