Metamath Proof Explorer


Theorem fzne1

Description: Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)

Ref Expression
Assertion fzne1 KMNKMKM+1N

Proof

Step Hyp Ref Expression
1 df-ne KM¬K=M
2 elfzuz2 KMNNM
3 elfzp12 NMKMNK=MKM+1N
4 2 3 syl KMNKMNK=MKM+1N
5 4 ibi KMNK=MKM+1N
6 5 orcanai KMN¬K=MKM+1N
7 1 6 sylan2b KMNKMKM+1N