elfz2z

Description: Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018)

		Ref	Expression
	Assertion	elfz2z	$⊢ (K \in ℤ \land N \in ℤ) \to (K \in (0 \dots N) \leftrightarrow (0 \leq K \land K \leq N))$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)$
2		df-3an	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N) \leftrightarrow ((K \in ℕ_{0} \land N \in ℕ_{0}) \land K \leq N)$
3	1 2	bitri	$⊢ K \in (0 \dots N) \leftrightarrow ((K \in ℕ_{0} \land N \in ℕ_{0}) \land K \leq N)$
4		nn0ge0	$⊢ K \in ℕ_{0} \to 0 \leq K$
5	4	adantr	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to 0 \leq K$
6		simpll	$⊢ ((K \in ℤ \land N \in ℤ) \land K \leq N) \to K \in ℤ$
7	6	anim1i	$⊢ (((K \in ℤ \land N \in ℤ) \land K \leq N) \land 0 \leq K) \to (K \in ℤ \land 0 \leq K)$
8		elnn0z	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℤ \land 0 \leq K)$
9	7 8	sylibr	$⊢ (((K \in ℤ \land N \in ℤ) \land K \leq N) \land 0 \leq K) \to K \in ℕ_{0}$
10		0red	$⊢ (K \in ℤ \land N \in ℤ) \to 0 \in ℝ$
11		zre	$⊢ K \in ℤ \to K \in ℝ$
12	11	adantr	$⊢ (K \in ℤ \land N \in ℤ) \to K \in ℝ$
13		zre	$⊢ N \in ℤ \to N \in ℝ$
14	13	adantl	$⊢ (K \in ℤ \land N \in ℤ) \to N \in ℝ$
15		letr	$⊢ (0 \in ℝ \land K \in ℝ \land N \in ℝ) \to ((0 \leq K \land K \leq N) \to 0 \leq N)$
16	10 12 14 15	syl3anc	$⊢ (K \in ℤ \land N \in ℤ) \to ((0 \leq K \land K \leq N) \to 0 \leq N)$
17		elnn0z	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℤ \land 0 \leq N)$
18	17	simplbi2	$⊢ N \in ℤ \to (0 \leq N \to N \in ℕ_{0})$
19	18	adantl	$⊢ (K \in ℤ \land N \in ℤ) \to (0 \leq N \to N \in ℕ_{0})$
20	16 19	syld	$⊢ (K \in ℤ \land N \in ℤ) \to ((0 \leq K \land K \leq N) \to N \in ℕ_{0})$
21	20	expcomd	$⊢ (K \in ℤ \land N \in ℤ) \to (K \leq N \to (0 \leq K \to N \in ℕ_{0}))$
22	21	imp31	$⊢ (((K \in ℤ \land N \in ℤ) \land K \leq N) \land 0 \leq K) \to N \in ℕ_{0}$
23	9 22	jca	$⊢ (((K \in ℤ \land N \in ℤ) \land K \leq N) \land 0 \leq K) \to (K \in ℕ_{0} \land N \in ℕ_{0})$
24	23	ex	$⊢ ((K \in ℤ \land N \in ℤ) \land K \leq N) \to (0 \leq K \to (K \in ℕ_{0} \land N \in ℕ_{0}))$
25	5 24	impbid2	$⊢ ((K \in ℤ \land N \in ℤ) \land K \leq N) \to ((K \in ℕ_{0} \land N \in ℕ_{0}) \leftrightarrow 0 \leq K)$
26	25	ex	$⊢ (K \in ℤ \land N \in ℤ) \to (K \leq N \to ((K \in ℕ_{0} \land N \in ℕ_{0}) \leftrightarrow 0 \leq K))$
27	26	pm5.32rd	$⊢ (K \in ℤ \land N \in ℤ) \to (((K \in ℕ_{0} \land N \in ℕ_{0}) \land K \leq N) \leftrightarrow (0 \leq K \land K \leq N))$
28	3 27	syl5bb	$⊢ (K \in ℤ \land N \in ℤ) \to (K \in (0 \dots N) \leftrightarrow (0 \leq K \land K \leq N))$

Metamath Proof Explorer

Theorem elfz2z

Proof