uzdisj

Description: The first N elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014)

		Ref	Expression
	Assertion	uzdisj	$⊢ (M \dots N - 1) \cap ℤ_{\geq N} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elinel2	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to k \in ℤ_{\geq N}$
2		eluzle	$⊢ k \in ℤ_{\geq N} \to N \leq k$
3	1 2	syl	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to N \leq k$
4		eluzel2	$⊢ k \in ℤ_{\geq N} \to N \in ℤ$
5	1 4	syl	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to N \in ℤ$
6		eluzelz	$⊢ k \in ℤ_{\geq N} \to k \in ℤ$
7	1 6	syl	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to k \in ℤ$
8		zlem1lt	$⊢ (N \in ℤ \land k \in ℤ) \to (N \leq k \leftrightarrow N - 1 < k)$
9	5 7 8	syl2anc	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to (N \leq k \leftrightarrow N - 1 < k)$
10	3 9	mpbid	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to N - 1 < k$
11	7	zred	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to k \in ℝ$
12		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
13	5 12	syl	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to N - 1 \in ℤ$
14	13	zred	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to N - 1 \in ℝ$
15		elinel1	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to k \in (M \dots N - 1)$
16		elfzle2	$⊢ k \in (M \dots N - 1) \to k \leq N - 1$
17	15 16	syl	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to k \leq N - 1$
18	11 14 17	lensymd	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to \neg N - 1 < k$
19	10 18	pm2.21dd	$⊢ k \in ((M \dots N - 1) \cap ℤ_{\geq N}) \to k \in \emptyset$
20	19	ssriv	$⊢ (M \dots N - 1) \cap ℤ_{\geq N} \subseteq \emptyset$
21		ss0	$⊢ (M \dots N - 1) \cap ℤ_{\geq N} \subseteq \emptyset \to (M \dots N - 1) \cap ℤ_{\geq N} = \emptyset$
22	20 21	ax-mp	$⊢ (M \dots N - 1) \cap ℤ_{\geq N} = \emptyset$

Metamath Proof Explorer

Theorem uzdisj

Proof