Metamath Proof Explorer

Theorem elfzop1le2

Description: A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion elfzop1le2 ⊢ K ∈ M ..^ N → K + 1 ≤ N

Proof

Step Hyp Ref Expression
1 elfzolt2 ⊢ K ∈ M ..^ N → K < N
2 elfzoelz ⊢ K ∈ M ..^ N → K ∈ ℤ
3 elfzoel2 ⊢ K ∈ M ..^ N → N ∈ ℤ
4 zltp1le ⊢ K ∈ ℤ ∧ N ∈ ℤ → K < N ↔ K + 1 ≤ N
5 2 3 4 syl2anc ⊢ K ∈ M ..^ N → K < N ↔ K + 1 ≤ N
6 1 5 mpbid ⊢ K ∈ M ..^ N → K + 1 ≤ N