Metamath Proof Explorer

Definition df-fzo

Description: Define a function generating sets of integers using ahalf-open range. Read ( M ..^ N ) as the integers from M up to, but not including, N ; contrast with ( M ... N ) df-fz , which includes N . Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit with fzsplit , for instance. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion df-fzo 
|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfzo 
 |-  ..^
1 vm 
 |-  m
2 cz 
 |-  ZZ
3 vn 
 |-  n
4 1 cv 
 |-  m
5 cfz 
 |-  ...
6 3 cv 
 |-  n
7 cmin 
 |-  -
8 c1 
 |-  1
9 6 8 7 co 
 |-  ( n - 1 )
10 4 9 5 co 
 |-  ( m ... ( n - 1 ) )
11 1 3 2 2 10 cmpo 
 |-  ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
12 0 11 wceq 
 |-  ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )