nn0disj

Description: The first N + 1 elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019)

		Ref	Expression
	Assertion	nn0disj	$⊢ (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elinel2	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to k \in ℤ_{\geq (N + 1)}$
2		eluzle	$⊢ k \in ℤ_{\geq (N + 1)} \to N + 1 \leq k$
3	1 2	syl	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N + 1 \leq k$
4		eluzel2	$⊢ k \in ℤ_{\geq (N + 1)} \to N + 1 \in ℤ$
5	1 4	syl	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N + 1 \in ℤ$
6		eluzelz	$⊢ k \in ℤ_{\geq (N + 1)} \to k \in ℤ$
7	1 6	syl	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to k \in ℤ$
8		zlem1lt	$⊢ (N + 1 \in ℤ \land k \in ℤ) \to (N + 1 \leq k \leftrightarrow N + 1 - 1 < k)$
9	5 7 8	syl2anc	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to (N + 1 \leq k \leftrightarrow N + 1 - 1 < k)$
10	3 9	mpbid	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N + 1 - 1 < k$
11		elinel1	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to k \in (0 \dots N)$
12		elfzle2	$⊢ k \in (0 \dots N) \to k \leq N$
13	11 12	syl	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to k \leq N$
14	7	zred	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to k \in ℝ$
15		elin	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \leftrightarrow (k \in (0 \dots N) \land k \in ℤ_{\geq (N + 1)})$
16		elfzel2	$⊢ k \in (0 \dots N) \to N \in ℤ$
17	16	adantr	$⊢ (k \in (0 \dots N) \land k \in ℤ_{\geq (N + 1)}) \to N \in ℤ$
18	15 17	sylbi	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N \in ℤ$
19	18	zred	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N \in ℝ$
20	14 19	lenltd	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to (k \leq N \leftrightarrow \neg N < k)$
21	18	zcnd	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N \in ℂ$
22		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
23	21 22	syl	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N + 1 - 1 = N$
24	23	eqcomd	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to N = N + 1 - 1$
25	24	breq1d	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to (N < k \leftrightarrow N + 1 - 1 < k)$
26	25	notbid	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to (\neg N < k \leftrightarrow \neg N + 1 - 1 < k)$
27	20 26	bitrd	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to (k \leq N \leftrightarrow \neg N + 1 - 1 < k)$
28	13 27	mpbid	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to \neg N + 1 - 1 < k$
29	10 28	pm2.21dd	$⊢ k \in ((0 \dots N) \cap ℤ_{\geq (N + 1)}) \to k \in \emptyset$
30	29	ssriv	$⊢ (0 \dots N) \cap ℤ_{\geq (N + 1)} \subseteq \emptyset$
31		ss0	$⊢ (0 \dots N) \cap ℤ_{\geq (N + 1)} \subseteq \emptyset \to (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset$
32	30 31	ax-mp	$⊢ (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset$

Metamath Proof Explorer

Theorem nn0disj

Proof