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 M N ¬ K N + 1

Proof

Step Hyp Ref Expression
1 elfzle2 K M N K N
2 elfzel2 K M N N
3 eluzp1l N K N + 1 N < K
4 3 ex N K N + 1 N < K
5 2 4 syl K M N K N + 1 N < K
6 elfzelz K M N K
7 zre N N
8 zre K K
9 ltnle N K N < K ¬ K N
10 7 8 9 syl2an N K N < K ¬ K N
11 2 6 10 syl2anc K M N N < K ¬ K N
12 5 11 sylibd K M N K N + 1 ¬ K N
13 1 12 mt2d K M N ¬ K N + 1