Metamath Proof Explorer

Theorem elfzole1

Description: A member in a half-open integer interval is greater than or equal to the lower bound. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion elfzole1 ⊢ K ∈ M ..^ N → M ≤ K

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ K ∈ M ..^ N → K ∈ ℤ
2 elfzoel1 ⊢ K ∈ M ..^ N → M ∈ ℤ
3 elfzoel2 ⊢ K ∈ M ..^ N → N ∈ ℤ
4 elfzo ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M ..^ N ↔ M ≤ K ∧ K < N
5 1 2 3 4 syl3anc ⊢ K ∈ M ..^ N → K ∈ M ..^ N ↔ M ≤ K ∧ K < N
6 5 ibi ⊢ K ∈ M ..^ N → M ≤ K ∧ K < N
7 6 simpld ⊢ K ∈ M ..^ N → M ≤ K