Theorem 0elfz

Description: 0 is an element of a finite set of sequential nonnegative integers with a nonnegative integer as upper bound. (Contributed by AV, 6-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2	1	a1i	$$⊢N\in {\mathbb{N}}_0\to 0\in {\mathbb{N}}_0$$
3		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
4		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
5		elfz2nn0	$$⊢0\in \left(0\dots N\right)\leftrightarrow \left(0\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\wedge 0\le N\right)$$
6	2 3 4 5	syl3anbrc	$$⊢N\in {\mathbb{N}}_0\to 0\in \left(0\dots N\right)$$