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 id ⊢ M ∈ ℤ → M ∈ ℤ
2 zre ⊢ M ∈ ℤ → M ∈ ℝ
3 2 leidd ⊢ M ∈ ℤ → M ≤ M
4 eluz1 ⊢ M ∈ ℤ → M ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ M ≤ M
5 1 3 4 mpbir2and ⊢ M ∈ ℤ → M ∈ ℤ ≥ M