Description: Define an operation that produces a finite set of sequential integers. Read " M ... N " as "the set of integers from M to N inclusive". See fzval for its value and additional comments. (Contributed by NM, 6-Sep-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | df-fz | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cfz | |
|
1 | vm | |
|
2 | cz | |
|
3 | vn | |
|
4 | vk | |
|
5 | 1 | cv | |
6 | cle | |
|
7 | 4 | cv | |
8 | 5 7 6 | wbr | |
9 | 3 | cv | |
10 | 7 9 6 | wbr | |
11 | 8 10 | wa | |
12 | 11 4 2 | crab | |
13 | 1 3 2 2 12 | cmpo | |
14 | 0 13 | wceq | |