Metamath Proof Explorer


Theorem fztp

Description: A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011) (Revised by Mario Carneiro, 7-Mar-2014)

Ref Expression
Assertion fztp M M M + 2 = M M + 1 M + 2

Proof

Step Hyp Ref Expression
1 uzid M M M
2 peano2uz M M M + 1 M
3 fzsuc M + 1 M M M + 1 + 1 = M M + 1 M + 1 + 1
4 1 2 3 3syl M M M + 1 + 1 = M M + 1 M + 1 + 1
5 zcn M M
6 ax-1cn 1
7 addass M 1 1 M + 1 + 1 = M + 1 + 1
8 6 6 7 mp3an23 M M + 1 + 1 = M + 1 + 1
9 5 8 syl M M + 1 + 1 = M + 1 + 1
10 df-2 2 = 1 + 1
11 10 oveq2i M + 2 = M + 1 + 1
12 9 11 eqtr4di M M + 1 + 1 = M + 2
13 12 oveq2d M M M + 1 + 1 = M M + 2
14 fzpr M M M + 1 = M M + 1
15 12 sneqd M M + 1 + 1 = M + 2
16 14 15 uneq12d M M M + 1 M + 1 + 1 = M M + 1 M + 2
17 df-tp M M + 1 M + 2 = M M + 1 M + 2
18 16 17 eqtr4di M M M + 1 M + 1 + 1 = M M + 1 M + 2
19 4 13 18 3eqtr3d M M M + 2 = M M + 1 M + 2