# 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}\in \left({M}\dots {N}\right)\to ¬{K}\in {ℤ}_{\ge \left({N}+1\right)}$

### Proof

Step Hyp Ref Expression
1 elfzle2 ${⊢}{K}\in \left({M}\dots {N}\right)\to {K}\le {N}$
2 elfzel2 ${⊢}{K}\in \left({M}\dots {N}\right)\to {N}\in ℤ$
3 eluzp1l ${⊢}\left({N}\in ℤ\wedge {K}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}<{K}$
4 3 ex ${⊢}{N}\in ℤ\to \left({K}\in {ℤ}_{\ge \left({N}+1\right)}\to {N}<{K}\right)$
5 2 4 syl ${⊢}{K}\in \left({M}\dots {N}\right)\to \left({K}\in {ℤ}_{\ge \left({N}+1\right)}\to {N}<{K}\right)$
6 elfzelz ${⊢}{K}\in \left({M}\dots {N}\right)\to {K}\in ℤ$
7 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
8 zre ${⊢}{K}\in ℤ\to {K}\in ℝ$
9 ltnle ${⊢}\left({N}\in ℝ\wedge {K}\in ℝ\right)\to \left({N}<{K}↔¬{K}\le {N}\right)$
10 7 8 9 syl2an ${⊢}\left({N}\in ℤ\wedge {K}\in ℤ\right)\to \left({N}<{K}↔¬{K}\le {N}\right)$
11 2 6 10 syl2anc ${⊢}{K}\in \left({M}\dots {N}\right)\to \left({N}<{K}↔¬{K}\le {N}\right)$
12 5 11 sylibd ${⊢}{K}\in \left({M}\dots {N}\right)\to \left({K}\in {ℤ}_{\ge \left({N}+1\right)}\to ¬{K}\le {N}\right)$
13 1 12 mt2d ${⊢}{K}\in \left({M}\dots {N}\right)\to ¬{K}\in {ℤ}_{\ge \left({N}+1\right)}$