Metamath Proof Explorer

Theorem elfzo0suble

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

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

Proof

Step Hyp Ref Expression
1 elfzoel2 ⊢ A ∈ 0 ..^ B → B ∈ ℤ
2 1 zred ⊢ A ∈ 0 ..^ B → B ∈ ℝ
3 elfzoelz ⊢ A ∈ 0 ..^ B → A ∈ ℤ
4 3 zred ⊢ A ∈ 0 ..^ B → A ∈ ℝ
5 1 zcnd ⊢ A ∈ 0 ..^ B → B ∈ ℂ
6 5 subidd ⊢ A ∈ 0 ..^ B → B − B = 0
7 elfzole1 ⊢ A ∈ 0 ..^ B → 0 ≤ A
8 6 7 eqbrtrd ⊢ A ∈ 0 ..^ B → B − B ≤ A
9 2 2 4 8 subled ⊢ A ∈ 0 ..^ B → B − A ≤ B