Metamath Proof Explorer


Theorem ige2m1fz

Description: Membership in a 0-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 18-Jun-2018) (Proof shortened by Alexander van der Vekens, 15-Sep-2018)

Ref Expression
Assertion ige2m1fz N 0 2 N N 1 0 N

Proof

Step Hyp Ref Expression
1 1eluzge0 1 0
2 fzss1 1 0 1 N 0 N
3 1 2 ax-mp 1 N 0 N
4 2z 2
5 4 a1i N 0 2 N 2
6 nn0z N 0 N
7 6 adantr N 0 2 N N
8 simpr N 0 2 N 2 N
9 eluz2 N 2 2 N 2 N
10 5 7 8 9 syl3anbrc N 0 2 N N 2
11 ige2m1fz1 N 2 N 1 1 N
12 10 11 syl N 0 2 N N 1 1 N
13 3 12 sseldi N 0 2 N N 1 0 N