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

Metamath Proof Explorer

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