This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ..^ = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfzo ⊢ ..^
1 vm ⊢ 𝑚
2 cz ⊢ ℤ
3 vn ⊢ 𝑛
4 1 cv ⊢ 𝑚
5 cfz ⊢ ...
6 3 cv ⊢ 𝑛
7 cmin ⊢ −
8 c1 ⊢ 1
9 6 8 7 co ⊢ ( 𝑛 − 1 )
10 4 9 5 co ⊢ ( 𝑚 ... ( 𝑛 − 1 ) )
11 1 3 2 2 10 cmpo ⊢ ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )
12 0 11 wceq ⊢ ..^ = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )