Theorem fznuz

Description: Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 30-Jun-2013) (Revised by Mario Carneiro, 24-Aug-2013)

	Ref	Expression
Assertion	fznuz	|- ( K e. ( M ... N ) -> -. K e. ( ZZ>= ` ( N + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzle2	|- ( K e. ( M ... N ) -> K <_ N )
2		elfzel2	|- ( K e. ( M ... N ) -> N e. ZZ )
3		eluzp1l	|- ( ( N e. ZZ /\ K e. ( ZZ>= ` ( N + 1 ) ) ) -> N < K )
4	3	ex	|- ( N e. ZZ -> ( K e. ( ZZ>= ` ( N + 1 ) ) -> N < K ) )
5	2 4	syl	|- ( K e. ( M ... N ) -> ( K e. ( ZZ>= ` ( N + 1 ) ) -> N < K ) )
6		elfzelz	|- ( K e. ( M ... N ) -> K e. ZZ )
7		zre	|- ( N e. ZZ -> N e. RR )
8		zre	|- ( K e. ZZ -> K e. RR )
9		ltnle	|- ( ( N e. RR /\ K e. RR ) -> ( N < K <-> -. K <_ N ) )
10	7 8 9	syl2an	|- ( ( N e. ZZ /\ K e. ZZ ) -> ( N < K <-> -. K <_ N ) )
11	2 6 10	syl2anc	|- ( K e. ( M ... N ) -> ( N < K <-> -. K <_ N ) )
12	5 11	sylibd	|- ( K e. ( M ... N ) -> ( K e. ( ZZ>= ` ( N + 1 ) ) -> -. K <_ N ) )
13	1 12	mt2d	|- ( K e. ( M ... N ) -> -. K e. ( ZZ>= ` ( N + 1 ) ) )