Metamath Proof Explorer


Theorem fz1eqin

Description: Express a one-based finite range as the intersection of lower integers with NN . (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion fz1eqin N 0 1 N = N + 1

Proof

Step Hyp Ref Expression
1 1z 1
2 nn0z N 0 N
3 elfz1 1 N a 1 N a 1 a a N
4 1 2 3 sylancr N 0 a 1 N a 1 a a N
5 3anass a 1 a a N a 1 a a N
6 ancom 1 a a N a N 1 a
7 6 anbi2i a 1 a a N a a N 1 a
8 anandi a a N 1 a a a N a 1 a
9 5 7 8 3bitri a 1 a a N a a N a 1 a
10 4 9 bitrdi N 0 a 1 N a a N a 1 a
11 elin a N + 1 a N + 1 a
12 ellz1 N a N + 1 a a N
13 2 12 syl N 0 a N + 1 a a N
14 elnnz1 a a 1 a
15 14 a1i N 0 a a 1 a
16 13 15 anbi12d N 0 a N + 1 a a a N a 1 a
17 11 16 syl5bb N 0 a N + 1 a a N a 1 a
18 10 17 bitr4d N 0 a 1 N a N + 1
19 18 eqrdv N 0 1 N = N + 1