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