Metamath Proof Explorer

Theorem elfz2nn0

Description: Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0uz	$⊢ K \in ℕ_{0} \leftrightarrow K \in ℤ_{\geq 0}$
2	1	anbi1i	$⊢ (K \in ℕ_{0} \land N \in ℤ_{\geq K}) \leftrightarrow (K \in ℤ_{\geq 0} \land N \in ℤ_{\geq K})$
3		eluznn0	$⊢ (K \in ℕ_{0} \land N \in ℤ_{\geq K}) \to N \in ℕ_{0}$
4		eluzle	$⊢ N \in ℤ_{\geq K} \to K \leq N$
5	4	adantl	$⊢ (K \in ℕ_{0} \land N \in ℤ_{\geq K}) \to K \leq N$
6	3 5	jca	$⊢ (K \in ℕ_{0} \land N \in ℤ_{\geq K}) \to (N \in ℕ_{0} \land K \leq N)$
7		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
8		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
9		eluz	$⊢ (K \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq K} \leftrightarrow K \leq N)$
10	7 8 9	syl2an	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to (N \in ℤ_{\geq K} \leftrightarrow K \leq N)$
11	10	biimprd	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to (K \leq N \to N \in ℤ_{\geq K})$
12	11	impr	$⊢ (K \in ℕ_{0} \land (N \in ℕ_{0} \land K \leq N)) \to N \in ℤ_{\geq K}$
13	6 12	impbida	$⊢ K \in ℕ_{0} \to (N \in ℤ_{\geq K} \leftrightarrow (N \in ℕ_{0} \land K \leq N))$
14	13	pm5.32i	$⊢ (K \in ℕ_{0} \land N \in ℤ_{\geq K}) \leftrightarrow (K \in ℕ_{0} \land (N \in ℕ_{0} \land K \leq N))$
15	2 14	bitr3i	$⊢ (K \in ℤ_{\geq 0} \land N \in ℤ_{\geq K}) \leftrightarrow (K \in ℕ_{0} \land (N \in ℕ_{0} \land K \leq N))$
16		elfzuzb	$⊢ K \in (0 \dots N) \leftrightarrow (K \in ℤ_{\geq 0} \land N \in ℤ_{\geq K})$
17		3anass	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N) \leftrightarrow (K \in ℕ_{0} \land (N \in ℕ_{0} \land K \leq N))$
18	15 16 17	3bitr4i	$⊢ K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)$