Metamath Proof Explorer


Theorem ige2m1fz1

Description: Membership of an integer greater than 1 decreased by 1 in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018)

Ref Expression
Assertion ige2m1fz1 N2N11N

Proof

Step Hyp Ref Expression
1 1e2m1 1=21
2 1 a1i N21=21
3 2 oveq2d N2N1=N21
4 2nn 2
5 uzsubsubfz1 2N2N211N
6 4 5 mpan N2N211N
7 3 6 eqeltrd N2N11N