elfzp12

Description: Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010)

		Ref	Expression
	Assertion	elfzp12	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow (K = M \lor K \in (M + 1 \dots N)))$

Step	Hyp	Ref	Expression
1		elex	$⊢ K \in (M \dots N) \to K \in V$
2	1	anim2i	$⊢ (N \in ℤ_{\geq M} \land K \in (M \dots N)) \to (N \in ℤ_{\geq M} \land K \in V)$
3		elfvex	$⊢ N \in ℤ_{\geq M} \to M \in V$
4		eleq1	$⊢ K = M \to (K \in V \leftrightarrow M \in V)$
5	3 4	syl5ibrcom	$⊢ N \in ℤ_{\geq M} \to (K = M \to K \in V)$
6	5	imdistani	$⊢ (N \in ℤ_{\geq M} \land K = M) \to (N \in ℤ_{\geq M} \land K \in V)$
7		elex	$⊢ K \in (M + 1 \dots N) \to K \in V$
8	7	anim2i	$⊢ (N \in ℤ_{\geq M} \land K \in (M + 1 \dots N)) \to (N \in ℤ_{\geq M} \land K \in V)$
9	6 8	jaodan	$⊢ (N \in ℤ_{\geq M} \land (K = M \lor K \in (M + 1 \dots N))) \to (N \in ℤ_{\geq M} \land K \in V)$
10		fzpred	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
11	10	eleq2d	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow K \in (\{M\} \cup (M + 1 \dots N)))$
12		elun	$⊢ K \in (\{M\} \cup (M + 1 \dots N)) \leftrightarrow (K \in \{M\} \lor K \in (M + 1 \dots N))$
13	11 12	bitrdi	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow (K \in \{M\} \lor K \in (M + 1 \dots N)))$
14		elsng	$⊢ K \in V \to (K \in \{M\} \leftrightarrow K = M)$
15	14	orbi1d	$⊢ K \in V \to ((K \in \{M\} \lor K \in (M + 1 \dots N)) \leftrightarrow (K = M \lor K \in (M + 1 \dots N)))$
16	13 15	sylan9bb	$⊢ (N \in ℤ_{\geq M} \land K \in V) \to (K \in (M \dots N) \leftrightarrow (K = M \lor K \in (M + 1 \dots N)))$
17	2 9 16	pm5.21nd	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow (K = M \lor K \in (M + 1 \dots N)))$

Metamath Proof Explorer