Theorem fz1n

Description: A 1-based finite set of sequential integers is empty iff it ends at index 0 . (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	fz1n	$$⊢N\in {\mathbb{N}}_0\to \left(\left(1\dots N\right)=\varnothing \leftrightarrow N=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
3		fzn	$$⊢\left(1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(N<1\leftrightarrow \left(1\dots N\right)=\varnothing \right)$$
4	1 2 3	sylancr	$$⊢N\in {\mathbb{N}}_0\to \left(N<1\leftrightarrow \left(1\dots N\right)=\varnothing \right)$$
5		nn0lt10b	$$⊢N\in {\mathbb{N}}_0\to \left(N<1\leftrightarrow N=0\right)$$
6	4 5	bitr3d	$$⊢N\in {\mathbb{N}}_0\to \left(\left(1\dots N\right)=\varnothing \leftrightarrow N=0\right)$$