Metamath Proof Explorer

Theorem uzid

Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005)

Ref Expression
Assertion uzid ⊢ M ∈ ℤ → M ∈ ℤ ≥ M

Proof

Step Hyp Ref Expression
1 zre ⊢ M ∈ ℤ → M ∈ ℝ
2 1 leidd ⊢ M ∈ ℤ → M ≤ M
3 2 ancli ⊢ M ∈ ℤ → M ∈ ℤ ∧ M ≤ M
4 eluz1 ⊢ M ∈ ℤ → M ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ M ≤ M
5 3 4 mpbird ⊢ M ∈ ℤ → M ∈ ℤ ≥ M