Metamath Proof Explorer


Theorem fzsuc2

Description: Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014)

Ref Expression
Assertion fzsuc2 MNM1MN+1=MNN+1

Proof

Step Hyp Ref Expression
1 uzp1 NM1N=M1NM-1+1
2 zcn MM
3 ax-1cn 1
4 npcan M1M-1+1=M
5 2 3 4 sylancl MM-1+1=M
6 5 oveq2d MMM-1+1=MM
7 uncom M=M
8 un0 M=M
9 7 8 eqtri M=M
10 zre MM
11 10 ltm1d MM1<M
12 peano2zm MM1
13 fzn MM1M1<MMM1=
14 12 13 mpdan MM1<MMM1=
15 11 14 mpbid MMM1=
16 5 sneqd MM-1+1=M
17 15 16 uneq12d MMM1M-1+1=M
18 fzsn MMM=M
19 9 17 18 3eqtr4a MMM1M-1+1=MM
20 6 19 eqtr4d MMM-1+1=MM1M-1+1
21 oveq1 N=M1N+1=M-1+1
22 21 oveq2d N=M1MN+1=MM-1+1
23 oveq2 N=M1MN=MM1
24 21 sneqd N=M1N+1=M-1+1
25 23 24 uneq12d N=M1MNN+1=MM1M-1+1
26 22 25 eqeq12d N=M1MN+1=MNN+1MM-1+1=MM1M-1+1
27 20 26 syl5ibrcom MN=M1MN+1=MNN+1
28 27 imp MN=M1MN+1=MNN+1
29 5 fveq2d MM-1+1=M
30 29 eleq2d MNM-1+1NM
31 30 biimpa MNM-1+1NM
32 fzsuc NMMN+1=MNN+1
33 31 32 syl MNM-1+1MN+1=MNN+1
34 28 33 jaodan MN=M1NM-1+1MN+1=MNN+1
35 1 34 sylan2 MNM1MN+1=MNN+1