fzneuz

Description: No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005)

		Ref	Expression
	Assertion	fzneuz	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to \neg (M \dots N) = ℤ_{\geq K}$

Proof

Step	Hyp	Ref	Expression
1		peano2uz	$⊢ N \in ℤ_{\geq K} \to N + 1 \in ℤ_{\geq K}$
2		eluzelre	$⊢ N \in ℤ_{\geq M} \to N \in ℝ$
3		ltp1	$⊢ N \in ℝ \to N < N + 1$
4		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
5		ltnle	$⊢ (N \in ℝ \land N + 1 \in ℝ) \to (N < N + 1 \leftrightarrow \neg N + 1 \leq N)$
6	4 5	mpdan	$⊢ N \in ℝ \to (N < N + 1 \leftrightarrow \neg N + 1 \leq N)$
7	3 6	mpbid	$⊢ N \in ℝ \to \neg N + 1 \leq N$
8	2 7	syl	$⊢ N \in ℤ_{\geq M} \to \neg N + 1 \leq N$
9		elfzle2	$⊢ N + 1 \in (M \dots N) \to N + 1 \leq N$
10	8 9	nsyl	$⊢ N \in ℤ_{\geq M} \to \neg N + 1 \in (M \dots N)$
11	10	ad2antrr	$⊢ ((N \in ℤ_{\geq M} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to \neg N + 1 \in (M \dots N)$
12		nelneq2	$⊢ (N + 1 \in ℤ_{\geq K} \land \neg N + 1 \in (M \dots N)) \to \neg ℤ_{\geq K} = (M \dots N)$
13	1 11 12	syl2an2	$⊢ ((N \in ℤ_{\geq M} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to \neg ℤ_{\geq K} = (M \dots N)$
14		eqcom	$⊢ ℤ_{\geq K} = (M \dots N) \leftrightarrow (M \dots N) = ℤ_{\geq K}$
15	13 14	sylnib	$⊢ ((N \in ℤ_{\geq M} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to \neg (M \dots N) = ℤ_{\geq K}$
16		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
17	16	ad2antrr	$⊢ ((N \in ℤ_{\geq M} \land K \in ℤ) \land \neg N \in ℤ_{\geq K}) \to N \in (M \dots N)$
18		nelneq2	$⊢ (N \in (M \dots N) \land \neg N \in ℤ_{\geq K}) \to \neg (M \dots N) = ℤ_{\geq K}$
19	17 18	sylancom	$⊢ ((N \in ℤ_{\geq M} \land K \in ℤ) \land \neg N \in ℤ_{\geq K}) \to \neg (M \dots N) = ℤ_{\geq K}$
20	15 19	pm2.61dan	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to \neg (M \dots N) = ℤ_{\geq K}$

Metamath Proof Explorer

Theorem fzneuz

Proof