Step |
Hyp |
Ref |
Expression |
1 |
|
uzid |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
2 |
|
peano2uz |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
3 |
|
fzsuc |
⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( ( 𝑀 + 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) ) |
4 |
1 2 3
|
3syl |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( ( 𝑀 + 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) ) |
5 |
|
zcn |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ ) |
6 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
7 |
|
addass |
⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + ( 1 + 1 ) ) ) |
8 |
6 6 7
|
mp3an23 |
⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + ( 1 + 1 ) ) ) |
9 |
5 8
|
syl |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + ( 1 + 1 ) ) ) |
10 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
11 |
10
|
oveq2i |
⊢ ( 𝑀 + 2 ) = ( 𝑀 + ( 1 + 1 ) ) |
12 |
9 11
|
eqtr4di |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + 2 ) ) |
13 |
12
|
oveq2d |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( ( 𝑀 + 1 ) + 1 ) ) = ( 𝑀 ... ( 𝑀 + 2 ) ) ) |
14 |
|
fzpr |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } ) |
15 |
12
|
sneqd |
⊢ ( 𝑀 ∈ ℤ → { ( ( 𝑀 + 1 ) + 1 ) } = { ( 𝑀 + 2 ) } ) |
16 |
14 15
|
uneq12d |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) = ( { 𝑀 , ( 𝑀 + 1 ) } ∪ { ( 𝑀 + 2 ) } ) ) |
17 |
|
df-tp |
⊢ { 𝑀 , ( 𝑀 + 1 ) , ( 𝑀 + 2 ) } = ( { 𝑀 , ( 𝑀 + 1 ) } ∪ { ( 𝑀 + 2 ) } ) |
18 |
16 17
|
eqtr4di |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) = { 𝑀 , ( 𝑀 + 1 ) , ( 𝑀 + 2 ) } ) |
19 |
4 13 18
|
3eqtr3d |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 2 ) ) = { 𝑀 , ( 𝑀 + 1 ) , ( 𝑀 + 2 ) } ) |