This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℕ_{0} \to ((1 \dots N) = \emptyset \leftrightarrow N = 0)$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
3		fzn	$⊢ (1 \in ℤ \land N \in ℤ) \to (N < 1 \leftrightarrow (1 \dots N) = \emptyset)$
4	1 2 3	sylancr	$⊢ N \in ℕ_{0} \to (N < 1 \leftrightarrow (1 \dots N) = \emptyset)$
5		nn0lt10b	$⊢ N \in ℕ_{0} \to (N < 1 \leftrightarrow N = 0)$
6	4 5	bitr3d	$⊢ N \in ℕ_{0} \to ((1 \dots N) = \emptyset \leftrightarrow N = 0)$