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 ) )

Metamath Proof Explorer

Theorem fzneuz

Proof