Theorem nn0fz0

Description: A nonnegative integer is always part of the finite set of sequential nonnegative integers with this integer as upper bound. (Contributed by Scott Fenton, 21-Mar-2018)

	Ref	Expression
Assertion	nn0fz0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in \left(0\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
2		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
3	2	leidd	$$⊢N\in {\mathbb{N}}_0\to N\le N$$
4		fznn0	$$⊢N\in {\mathbb{N}}_0\to \left(N\in \left(0\dots N\right)\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\le N\right)\right)$$
5	1 3 4	mpbir2and	$$⊢N\in {\mathbb{N}}_0\to N\in \left(0\dots N\right)$$
6		elfz3nn0	$$⊢N\in \left(0\dots N\right)\to N\in {\mathbb{N}}_0$$
7	5 6	impbii	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in \left(0\dots N\right)$$