Step |
Hyp |
Ref |
Expression |
1 |
|
fzolb |
⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ) |
2 |
|
fzofzp1 |
⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) |
3 |
1 2
|
sylbir |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑀 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) |
4 |
|
fzosplit |
⊢ ( ( 𝑀 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ..^ 𝑁 ) = ( ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) |
5 |
3 4
|
syl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑀 ..^ 𝑁 ) = ( ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) |
6 |
|
fzosn |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ..^ ( 𝑀 + 1 ) ) = { 𝑀 } ) |
7 |
6
|
3ad2ant1 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑀 ..^ ( 𝑀 + 1 ) ) = { 𝑀 } ) |
8 |
7
|
uneq1d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) |
9 |
5 8
|
eqtrd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑀 ..^ 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) |