Theorem fzneuz

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

	Ref	Expression
Assertion	fzneuz	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ¬ ( 𝑀 ... 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝐾 ) )
2		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ )
3		ltp1	⊢ ( 𝑁 ∈ ℝ → 𝑁 < ( 𝑁 + 1 ) )
4		peano2re	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
5		ltnle	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ) → ( 𝑁 < ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) ≤ 𝑁 ) )
6	4 5	mpdan	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 < ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) ≤ 𝑁 ) )
7	3 6	mpbid	⊢ ( 𝑁 ∈ ℝ → ¬ ( 𝑁 + 1 ) ≤ 𝑁 )
8	2 7	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ¬ ( 𝑁 + 1 ) ≤ 𝑁 )
9		elfzle2	⊢ ( ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝑁 + 1 ) ≤ 𝑁 )
10	8 9	nsyl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ¬ ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
11	10	ad2antrr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ¬ ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
12		nelneq2	⊢ ( ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ¬ ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ¬ ( ℤ≥ ‘ 𝐾 ) = ( 𝑀 ... 𝑁 ) )
13	1 11 12	syl2an2	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ¬ ( ℤ≥ ‘ 𝐾 ) = ( 𝑀 ... 𝑁 ) )
14		eqcom	⊢ ( ( ℤ≥ ‘ 𝐾 ) = ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ... 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )
15	13 14	sylnib	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ¬ ( 𝑀 ... 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )
16		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
17	16	ad2antrr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
18		nelneq2	⊢ ( ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ¬ ( 𝑀 ... 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )
19	17 18	sylancom	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ¬ ( 𝑀 ... 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )
20	15 19	pm2.61dan	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ¬ ( 𝑀 ... 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )