Step |
Hyp |
Ref |
Expression |
1 |
|
peano2uz |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
2 |
|
eluzfz2 |
⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) |
3 |
1 2
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) |
4 |
|
peano2fzr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) |
5 |
3 4
|
mpdan |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) |
6 |
|
fzsplit |
⊢ ( 𝑁 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( 𝑁 + 1 ) ) ) ) |
7 |
5 6
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( 𝑁 + 1 ) ) ) ) |
8 |
|
eluzelz |
⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ℤ ) |
9 |
|
fzsn |
⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( ( 𝑁 + 1 ) ... ( 𝑁 + 1 ) ) = { ( 𝑁 + 1 ) } ) |
10 |
1 8 9
|
3syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 1 ) ... ( 𝑁 + 1 ) ) = { ( 𝑁 + 1 ) } ) |
11 |
10
|
uneq2d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( 𝑁 + 1 ) ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ) |
12 |
7 11
|
eqtrd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ) |