Step |
Hyp |
Ref |
Expression |
1 |
|
uzid |
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) |
2 |
|
peano2uz |
|- ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) ) |
3 |
|
fzsuc |
|- ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( M ... ( ( M + 1 ) + 1 ) ) = ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) ) |
4 |
1 2 3
|
3syl |
|- ( M e. ZZ -> ( M ... ( ( M + 1 ) + 1 ) ) = ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) ) |
5 |
|
zcn |
|- ( M e. ZZ -> M e. CC ) |
6 |
|
ax-1cn |
|- 1 e. CC |
7 |
|
addass |
|- ( ( M e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( M + 1 ) + 1 ) = ( M + ( 1 + 1 ) ) ) |
8 |
6 6 7
|
mp3an23 |
|- ( M e. CC -> ( ( M + 1 ) + 1 ) = ( M + ( 1 + 1 ) ) ) |
9 |
5 8
|
syl |
|- ( M e. ZZ -> ( ( 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 e. ZZ -> ( ( M + 1 ) + 1 ) = ( M + 2 ) ) |
13 |
12
|
oveq2d |
|- ( M e. ZZ -> ( M ... ( ( M + 1 ) + 1 ) ) = ( M ... ( M + 2 ) ) ) |
14 |
|
fzpr |
|- ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } ) |
15 |
12
|
sneqd |
|- ( M e. ZZ -> { ( ( M + 1 ) + 1 ) } = { ( M + 2 ) } ) |
16 |
14 15
|
uneq12d |
|- ( M e. ZZ -> ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) = ( { M , ( M + 1 ) } u. { ( M + 2 ) } ) ) |
17 |
|
df-tp |
|- { M , ( M + 1 ) , ( M + 2 ) } = ( { M , ( M + 1 ) } u. { ( M + 2 ) } ) |
18 |
16 17
|
eqtr4di |
|- ( M e. ZZ -> ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) = { M , ( M + 1 ) , ( M + 2 ) } ) |
19 |
4 13 18
|
3eqtr3d |
|- ( M e. ZZ -> ( M ... ( M + 2 ) ) = { M , ( M + 1 ) , ( M + 2 ) } ) |