fznn0

Description: Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005)

		Ref	Expression
	Assertion	fznn0	$⊢ N \in ℕ_{0} \to (K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land K \leq N))$

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
3		elfz1	$⊢ (0 \in ℤ \land N \in ℤ) \to (K \in (0 \dots N) \leftrightarrow (K \in ℤ \land 0 \leq K \land K \leq N))$
4	1 2 3	sylancr	$⊢ N \in ℕ_{0} \to (K \in (0 \dots N) \leftrightarrow (K \in ℤ \land 0 \leq K \land K \leq N))$
5		df-3an	$⊢ (K \in ℤ \land 0 \leq K \land K \leq N) \leftrightarrow ((K \in ℤ \land 0 \leq K) \land K \leq N)$
6		elnn0z	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℤ \land 0 \leq K)$
7	6	anbi1i	$⊢ (K \in ℕ_{0} \land K \leq N) \leftrightarrow ((K \in ℤ \land 0 \leq K) \land K \leq N)$
8	5 7	bitr4i	$⊢ (K \in ℤ \land 0 \leq K \land K \leq N) \leftrightarrow (K \in ℕ_{0} \land K \leq N)$
9	4 8	bitrdi	$⊢ N \in ℕ_{0} \to (K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land K \leq N))$

Metamath Proof Explorer