Metamath Proof Explorer


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 ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ𝑀 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) ) )