Theorem eluz1i

Description: Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005)

	Ref	Expression
Hypothesis	eluz.1	⊢ 𝑀 ∈ ℤ
Assertion	eluz1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eluz.1	⊢ 𝑀 ∈ ℤ
2		eluz1	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ) )
3	1 2	ax-mp	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )