Theorem eluz1

Description: Membership in the upper set of integers starting at M . (Contributed by NM, 5-Sep-2005)

	Ref	Expression
Assertion	eluz1	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uzval	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } )
2	1	eleq2d	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑁 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ) )
3		breq2	⊢ ( 𝑘 = 𝑁 → ( 𝑀 ≤ 𝑘 ↔ 𝑀 ≤ 𝑁 ) )
4	3	elrab	⊢ ( 𝑁 ∈ { 𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘 } ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
5	2 4	bitrdi	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ) )