Metamath Proof Explorer


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 ( ( 𝑁 ∈ ( ℤ𝑀 ) ∧ 𝐾 ∈ ℤ ) → ¬ ( 𝑀 ... 𝑁 ) = ( ℤ𝐾 ) )