Theorem fzonn0p1

Description: A nonnegative integer is an element of the half-open range of nonnegative integers with the element increased by one as an upper bound. (Contributed by Alexander van der Vekens, 5-Aug-2018)

	Ref	Expression
Assertion	fzonn0p1	$$⊢N\in {\mathbb{N}}_0\to N\in \left(0..^N+1\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
2		nn0p1nn	$$⊢N\in {\mathbb{N}}_0\to N+1\in \mathbb{N}$$
3		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
4	3	ltp1d	$$⊢N\in {\mathbb{N}}_0\to N<N+1$$
5		elfzo0	$$⊢N\in \left(0..^N+1\right)\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N+1\in \mathbb{N}\wedge N<N+1\right)$$
6	1 2 4 5	syl3anbrc	$$⊢N\in {\mathbb{N}}_0\to N\in \left(0..^N+1\right)$$