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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzp1 | |
|
2 | zcn | |
|
3 | ax-1cn | |
|
4 | npcan | |
|
5 | 2 3 4 | sylancl | |
6 | 5 | oveq2d | |
7 | uncom | |
|
8 | un0 | |
|
9 | 7 8 | eqtri | |
10 | zre | |
|
11 | 10 | ltm1d | |
12 | peano2zm | |
|
13 | fzn | |
|
14 | 12 13 | mpdan | |
15 | 11 14 | mpbid | |
16 | 5 | sneqd | |
17 | 15 16 | uneq12d | |
18 | fzsn | |
|
19 | 9 17 18 | 3eqtr4a | |
20 | 6 19 | eqtr4d | |
21 | oveq1 | |
|
22 | 21 | oveq2d | |
23 | oveq2 | |
|
24 | 21 | sneqd | |
25 | 23 24 | uneq12d | |
26 | 22 25 | eqeq12d | |
27 | 20 26 | syl5ibrcom | |
28 | 27 | imp | |
29 | 5 | fveq2d | |
30 | 29 | eleq2d | |
31 | 30 | biimpa | |
32 | fzsuc | |
|
33 | 31 32 | syl | |
34 | 28 33 | jaodan | |
35 | 1 34 | sylan2 | |