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	⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 1 ≤ ( 𝐵 − 𝐴 ) )

Proof

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