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

Metamath Proof Explorer

Definition df-uz

Description: Define a function whose value at j is the semi-infinite set of contiguous integers starting at j , which we will also call the upper integers starting at j . Read " ZZ>=M " as "the set of integers greater than or equal to M ". See uzval for its value, uzssz for its relationship to ZZ , nnuz and nn0uz for its relationships to NN and NN0 , and eluz1 and eluz2 for its membership relations. (Contributed by NM, 5-Sep-2005)

		Ref	Expression
	Assertion	df-uz	\|- ZZ>= = ( j e. ZZ \|-> { k e. ZZ \| j <_ k } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuz	\|- ZZ>=
1		vj	\|- j
2		cz	\|- ZZ
3		vk	\|- k
4	1	cv	\|- j
5		cle	\|- <_
6	3	cv	\|- k
7	4 6 5	wbr	\|- j <_ k
8	7 3 2	crab	\|- { k e. ZZ \| j <_ k }
9	1 2 8	cmpt	\|- ( j e. ZZ \|-> { k e. ZZ \| j <_ k } )
10	0 9	wceq	\|- ZZ>= = ( j e. ZZ \|-> { k e. ZZ \| j <_ k } )