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	$⊢ ..^= (m \in ℤ, n \in ℤ ⟼ (m \dots n - 1))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfzo	$class ..^$
1		vm	$setvar m$
2		cz	$class ℤ$
3		vn	$setvar n$
4	1	cv	$setvar m$
5		cfz	$class \dots$
6	3	cv	$setvar n$
7		cmin	$class -$
8		c1	$class 1$
9	6 8 7	co	$class (n - 1)$
10	4 9 5	co	$class (m \dots n - 1)$
11	1 3 2 2 10	cmpo	$class (m \in ℤ, n \in ℤ ⟼ (m \dots n - 1))$
12	0 11	wceq	$wff ..^= (m \in ℤ, n \in ℤ ⟼ (m \dots n - 1))$