fznn

Description: Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011) (Revised by Mario Carneiro, 18-Jun-2015)

		Ref	Expression
	Assertion	fznn	$⊢ N \in ℤ \to (K \in (1 \dots N) \leftrightarrow (K \in ℕ \land K \leq N))$

Step	Hyp	Ref	Expression
1		elfzuzb	$⊢ K \in (1 \dots N) \leftrightarrow (K \in ℤ_{\geq 1} \land N \in ℤ_{\geq K})$
2		elnnuz	$⊢ K \in ℕ \leftrightarrow K \in ℤ_{\geq 1}$
3	2	anbi1i	$⊢ (K \in ℕ \land N \in ℤ_{\geq K}) \leftrightarrow (K \in ℤ_{\geq 1} \land N \in ℤ_{\geq K})$
4	1 3	bitr4i	$⊢ K \in (1 \dots N) \leftrightarrow (K \in ℕ \land N \in ℤ_{\geq K})$
5		nnz	$⊢ K \in ℕ \to K \in ℤ$
6		eluz	$⊢ (K \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq K} \leftrightarrow K \leq N)$
7	5 6	sylan	$⊢ (K \in ℕ \land N \in ℤ) \to (N \in ℤ_{\geq K} \leftrightarrow K \leq N)$
8	7	ancoms	$⊢ (N \in ℤ \land K \in ℕ) \to (N \in ℤ_{\geq K} \leftrightarrow K \leq N)$
9	8	pm5.32da	$⊢ N \in ℤ \to ((K \in ℕ \land N \in ℤ_{\geq K}) \leftrightarrow (K \in ℕ \land K \leq N))$
10	4 9	syl5bb	$⊢ N \in ℤ \to (K \in (1 \dots N) \leftrightarrow (K \in ℕ \land K \leq N))$

Metamath Proof Explorer