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

Metamath Proof Explorer

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