MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fz Unicode version

Definition df-fz 11430
Description: Define an operation that produces a finite set of sequential integers. Read " " as "the set of integers from to inclusive." See fzval 11431 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
df-fz
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-fz
StepHypRef Expression
1 cfz 11429 . 2
2 vm . . 3
3 vn . . 3
4 cz 10638 . . 3
52cv 1368 . . . . . 6
6 vk . . . . . . 7
76cv 1368 . . . . . 6
8 cle 9411 . . . . . 6
95, 7, 8wbr 4287 . . . . 5
103cv 1368 . . . . . 6
117, 10, 8wbr 4287 . . . . 5
129, 11wa 369 . . . 4
1312, 6, 4crab 2714 . . 3
142, 3, 4, 4, 13cmpt2 6088 . 2
151, 14wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  fzval  11431  fzf  11433
  Copyright terms: Public domain W3C validator