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	⊢ ℤ_≥ = ( 𝑗 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuz	⊢ ℤ_≥
1		vj	⊢ 𝑗
2		cz	⊢ ℤ
3		vk	⊢ 𝑘
4	1	cv	⊢ 𝑗
5		cle	⊢ ≤
6	3	cv	⊢ 𝑘
7	4 6 5	wbr	⊢ 𝑗 ≤ 𝑘
8	7 3 2	crab	⊢ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 }
9	1 2 8	cmpt	⊢ ( 𝑗 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } )
10	0 9	wceq	⊢ ℤ_≥ = ( 𝑗 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } )