Description: Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | fzne1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne | |
|
2 | elfzuz2 | |
|
3 | elfzp12 | |
|
4 | 2 3 | syl | |
5 | 4 | ibi | |
6 | 5 | orcanai | |
7 | 1 6 | sylan2b | |