Metamath Proof Explorer

Theorem eluzle

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005)

Ref Expression
Assertion eluzle ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
2 1 simp3bi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )