uznfz

Description: Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013)

		Ref	Expression
	Assertion	uznfz	$⊢ K \in ℤ_{\geq N} \to \neg K \in (M \dots N - 1)$

Step	Hyp	Ref	Expression
1		eluzle	$⊢ K \in ℤ_{\geq N} \to N \leq K$
2		eluzel2	$⊢ K \in ℤ_{\geq N} \to N \in ℤ$
3		elfzel1	$⊢ K \in (M \dots N - 1) \to M \in ℤ$
4		elfzm11	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N - 1) \leftrightarrow (K \in ℤ \land M \leq K \land K < N))$
5		simp3	$⊢ (K \in ℤ \land M \leq K \land K < N) \to K < N$
6	4 5	biimtrdi	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N - 1) \to K < N)$
7	6	impancom	$⊢ (M \in ℤ \land K \in (M \dots N - 1)) \to (N \in ℤ \to K < N)$
8	3 7	mpancom	$⊢ K \in (M \dots N - 1) \to (N \in ℤ \to K < N)$
9	2 8	syl5com	$⊢ K \in ℤ_{\geq N} \to (K \in (M \dots N - 1) \to K < N)$
10		eluzelz	$⊢ K \in ℤ_{\geq N} \to K \in ℤ$
11		zre	$⊢ K \in ℤ \to K \in ℝ$
12		zre	$⊢ N \in ℤ \to N \in ℝ$
13		ltnle	$⊢ (K \in ℝ \land N \in ℝ) \to (K < N \leftrightarrow \neg N \leq K)$
14	11 12 13	syl2an	$⊢ (K \in ℤ \land N \in ℤ) \to (K < N \leftrightarrow \neg N \leq K)$
15	10 2 14	syl2anc	$⊢ K \in ℤ_{\geq N} \to (K < N \leftrightarrow \neg N \leq K)$
16	9 15	sylibd	$⊢ K \in ℤ_{\geq N} \to (K \in (M \dots N - 1) \to \neg N \leq K)$
17	1 16	mt2d	$⊢ K \in ℤ_{\geq N} \to \neg K \in (M \dots N - 1)$

Metamath Proof Explorer