Metamath Proof Explorer

Theorem fznuz

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

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

Proof

Step	Hyp	Ref	Expression
1		elfzle2	$⊢ K \in (M \dots N) \to K \leq N$
2		elfzel2	$⊢ K \in (M \dots N) \to N \in ℤ$
3		eluzp1l	$⊢ (N \in ℤ \land K \in ℤ_{\geq (N + 1)}) \to N < K$
4	3	ex	$⊢ N \in ℤ \to (K \in ℤ_{\geq (N + 1)} \to N < K)$
5	2 4	syl	$⊢ K \in (M \dots N) \to (K \in ℤ_{\geq (N + 1)} \to N < K)$
6		elfzelz	$⊢ K \in (M \dots N) \to K \in ℤ$
7		zre	$⊢ N \in ℤ \to N \in ℝ$
8		zre	$⊢ K \in ℤ \to K \in ℝ$
9		ltnle	$⊢ (N \in ℝ \land K \in ℝ) \to (N < K \leftrightarrow \neg K \leq N)$
10	7 8 9	syl2an	$⊢ (N \in ℤ \land K \in ℤ) \to (N < K \leftrightarrow \neg K \leq N)$
11	2 6 10	syl2anc	$⊢ K \in (M \dots N) \to (N < K \leftrightarrow \neg K \leq N)$
12	5 11	sylibd	$⊢ K \in (M \dots N) \to (K \in ℤ_{\geq (N + 1)} \to \neg K \leq N)$
13	1 12	mt2d	$⊢ K \in (M \dots N) \to \neg K \in ℤ_{\geq (N + 1)}$