Theorem elfzo0le

Description: A member in a half-open range of nonnegative integers is less than or equal to the upper bound of the range. (Contributed by Alexander van der Vekens, 23-Sep-2018)

	Ref	Expression
Assertion	elfzo0le	⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐴 ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elfzo0	⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ↔ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) )
2		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
3		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
4		ltle	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
5	2 3 4	syl2an	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
6	5	3impia	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
7	1 6	sylbi	⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐴 ≤ 𝐵 )