Metamath Proof Explorer

Theorem elfz2

Description: Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show M e. ZZ and N e. ZZ . (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	elfz2	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N))$

Proof

Step	Hyp	Ref	Expression
1		anass	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N)))$
2		df-3an	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land K \in ℤ)$
3	2	anbi1i	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land (M \leq K \land K \leq N))$
4		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N))$
5		3anass	$⊢ (K \in ℤ \land M \leq K \land K \leq N) \leftrightarrow (K \in ℤ \land (M \leq K \land K \leq N))$
6		ibar	$⊢ (M \in ℤ \land N \in ℤ) \to ((K \in ℤ \land (M \leq K \land K \leq N)) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N))))$
7	5 6	bitrid	$⊢ (M \in ℤ \land N \in ℤ) \to ((K \in ℤ \land M \leq K \land K \leq N) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N))))$
8	4 7	bitrd	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N))))$
9		fzf	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$
10	9	fdmi	$⊢ dom \dots = ℤ \times ℤ$
11	10	ndmov	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (M \dots N) = \emptyset$
12	11	eleq2d	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow K \in \emptyset)$
13		noel	$⊢ \neg K \in \emptyset$
14	13	pm2.21i	$⊢ K \in \emptyset \to (M \in ℤ \land N \in ℤ)$
15		simpl	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N))) \to (M \in ℤ \land N \in ℤ)$
16	14 15	pm5.21ni	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (K \in \emptyset \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N))))$
17	12 16	bitrd	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N))))$
18	8 17	pm2.61i	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N)))$
19	1 3 18	3bitr4ri	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N))$