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 ⊢ M ∈ ℤ → N ∈ ℤ ≥ M ↔ N ∈ ℤ ∧ M ≤ N

Proof

Step Hyp Ref Expression
1 uzval ⊢ M ∈ ℤ → ℤ ≥ M = k ∈ ℤ | M ≤ k
2 1 eleq2d ⊢ M ∈ ℤ → N ∈ ℤ ≥ M ↔ N ∈ k ∈ ℤ | M ≤ k
3 breq2 ⊢ k = N → M ≤ k ↔ M ≤ N
4 3 elrab ⊢ N ∈ k ∈ ℤ | M ≤ k ↔ N ∈ ℤ ∧ M ≤ N
5 2 4 bitrdi ⊢ M ∈ ℤ → N ∈ ℤ ≥ M ↔ N ∈ ℤ ∧ M ≤ N