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 
|- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> -. ( M ... N ) = ( ZZ>= ` K ) )

Proof

Step Hyp Ref Expression
1 peano2uz 
 |-  ( N e. ( ZZ>= ` K ) -> ( N + 1 ) e. ( ZZ>= ` K ) )
2 eluzelre 
 |-  ( N e. ( ZZ>= ` M ) -> N e. RR )
3 ltp1 
 |-  ( N e. RR -> N < ( N + 1 ) )
4 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
5 ltnle 
 |-  ( ( N e. RR /\ ( N + 1 ) e. RR ) -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
6 4 5 mpdan 
 |-  ( N e. RR -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
7 3 6 mpbid 
 |-  ( N e. RR -> -. ( N + 1 ) <_ N )
8 2 7 syl 
 |-  ( N e. ( ZZ>= ` M ) -> -. ( N + 1 ) <_ N )
9 elfzle2 
 |-  ( ( N + 1 ) e. ( M ... N ) -> ( N + 1 ) <_ N )
10 8 9 nsyl 
 |-  ( N e. ( ZZ>= ` M ) -> -. ( N + 1 ) e. ( M ... N ) )
11 10 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> -. ( N + 1 ) e. ( M ... N ) )
12 nelneq2 
 |-  ( ( ( N + 1 ) e. ( ZZ>= ` K ) /\ -. ( N + 1 ) e. ( M ... N ) ) -> -. ( ZZ>= ` K ) = ( M ... N ) )
13 1 11 12 syl2an2 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> -. ( ZZ>= ` K ) = ( M ... N ) )
14 eqcom 
 |-  ( ( ZZ>= ` K ) = ( M ... N ) <-> ( M ... N ) = ( ZZ>= ` K ) )
15 13 14 sylnib 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> -. ( M ... N ) = ( ZZ>= ` K ) )
16 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
17 16 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) /\ -. N e. ( ZZ>= ` K ) ) -> N e. ( M ... N ) )
18 nelneq2 
 |-  ( ( N e. ( M ... N ) /\ -. N e. ( ZZ>= ` K ) ) -> -. ( M ... N ) = ( ZZ>= ` K ) )
19 17 18 sylancom 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) /\ -. N e. ( ZZ>= ` K ) ) -> -. ( M ... N ) = ( ZZ>= ` K ) )
20 15 19 pm2.61dan 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> -. ( M ... N ) = ( ZZ>= ` K ) )