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	$$⊢A\in \left(0..^B\right)\to A\le B$$

Proof

Step	Hyp	Ref	Expression
1		elfzo0	$$⊢A\in \left(0..^B\right)\leftrightarrow \left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\wedge A<B\right)$$
2		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
3		nnre	$$⊢B\in \mathbb{N}\to B\in ℝ$$
4		ltle	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\to A\le B\right)$$
5	2 3 4	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(A<B\to A\le B\right)$$
6	5	3impia	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\wedge A<B\right)\to A\le B$$
7	1 6	sylbi	$$⊢A\in \left(0..^B\right)\to A\le B$$