Theorem uznfz

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

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

Proof

Step	Hyp	Ref	Expression
1		eluzle	|- ( K e. ( ZZ>= ` N ) -> N <_ K )
2		eluzel2	|- ( K e. ( ZZ>= ` N ) -> N e. ZZ )
3		elfzel1	|- ( K e. ( M ... ( N - 1 ) ) -> M e. ZZ )
4		elfzm11	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) <-> ( K e. ZZ /\ M <_ K /\ K < N ) ) )
5		simp3	|- ( ( K e. ZZ /\ M <_ K /\ K < N ) -> K < N )
6	4 5	syl6bi	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... ( N - 1 ) ) -> K < N ) )
7	6	impancom	|- ( ( M e. ZZ /\ K e. ( M ... ( N - 1 ) ) ) -> ( N e. ZZ -> K < N ) )
8	3 7	mpancom	|- ( K e. ( M ... ( N - 1 ) ) -> ( N e. ZZ -> K < N ) )
9	2 8	syl5com	|- ( K e. ( ZZ>= ` N ) -> ( K e. ( M ... ( N - 1 ) ) -> K < N ) )
10		eluzelz	|- ( K e. ( ZZ>= ` N ) -> K e. ZZ )
11		zre	|- ( K e. ZZ -> K e. RR )
12		zre	|- ( N e. ZZ -> N e. RR )
13		ltnle	|- ( ( K e. RR /\ N e. RR ) -> ( K < N <-> -. N <_ K ) )
14	11 12 13	syl2an	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N <-> -. N <_ K ) )
15	10 2 14	syl2anc	|- ( K e. ( ZZ>= ` N ) -> ( K < N <-> -. N <_ K ) )
16	9 15	sylibd	|- ( K e. ( ZZ>= ` N ) -> ( K e. ( M ... ( N - 1 ) ) -> -. N <_ K ) )
17	1 16	mt2d	|- ( K e. ( ZZ>= ` N ) -> -. K e. ( M ... ( N - 1 ) ) )