This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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