Step |
Hyp |
Ref |
Expression |
1 |
|
eluzelz |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ ) |
2 |
1
|
zcnd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℂ ) |
3 |
|
1zzd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 1 ∈ ℤ ) |
4 |
3
|
zcnd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 1 ∈ ℂ ) |
5 |
2 4
|
npcand |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 ) |
6 |
5
|
eleq1d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) |
7 |
6
|
ibir |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
8 |
|
eluzelre |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ ) |
9 |
8
|
lem1d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ≤ 𝑁 ) |
10 |
1 3
|
zsubcld |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ ) |
11 |
|
eluz1 |
⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑁 − 1 ) ≤ 𝑁 ) ) ) |
12 |
10 11
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑁 − 1 ) ≤ 𝑁 ) ) ) |
13 |
1 9 12
|
mpbir2and |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ) |
14 |
|
fzsplit2 |
⊢ ( ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) |
15 |
7 13 14
|
syl2anc |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) |
16 |
5
|
oveq1d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑁 ... 𝑁 ) ) |
17 |
|
fzsn |
⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } ) |
18 |
1 17
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ... 𝑁 ) = { 𝑁 } ) |
19 |
16 18
|
eqtrd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = { 𝑁 } ) |
20 |
19
|
uneq2d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ) |
21 |
15 20
|
eqtrd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ) |