Metamath Proof Explorer

Theorem elfzo0subge1

Description: The difference of the upper bound of a half-open range of nonnegative integers and an element of this range is greater than or equal to 1. (Contributed by AV, 1-Sep-2025) (Proof shortened by SN, 18-Sep-2025)

Ref Expression
Assertion elfzo0subge1 ⊢ A ∈ 0 ..^ B → 1 ≤ B − A

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ A ∈ 0 ..^ B → A ∈ ℤ
2 1 zred ⊢ A ∈ 0 ..^ B → A ∈ ℝ
3 elfzoel2 ⊢ A ∈ 0 ..^ B → B ∈ ℤ
4 3 zred ⊢ A ∈ 0 ..^ B → B ∈ ℝ
5 1red ⊢ A ∈ 0 ..^ B → 1 ∈ ℝ
6 elfzolem1 ⊢ A ∈ 0 ..^ B → A ≤ B − 1
7 2 4 5 6 lesubd ⊢ A ∈ 0 ..^ B → 1 ≤ B − A