Step |
Hyp |
Ref |
Expression |
1 |
|
fzosplitsn |
|- ( N e. ( ZZ>= ` M ) -> ( M ..^ ( N + 1 ) ) = ( ( M ..^ N ) u. { N } ) ) |
2 |
1
|
difeq1d |
|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ ( N + 1 ) ) \ { N } ) = ( ( ( M ..^ N ) u. { N } ) \ { N } ) ) |
3 |
|
difun2 |
|- ( ( ( M ..^ N ) u. { N } ) \ { N } ) = ( ( M ..^ N ) \ { N } ) |
4 |
2 3
|
eqtrdi |
|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ ( N + 1 ) ) \ { N } ) = ( ( M ..^ N ) \ { N } ) ) |
5 |
|
fzonel |
|- -. N e. ( M ..^ N ) |
6 |
|
disjsn |
|- ( ( ( M ..^ N ) i^i { N } ) = (/) <-> -. N e. ( M ..^ N ) ) |
7 |
5 6
|
mpbir |
|- ( ( M ..^ N ) i^i { N } ) = (/) |
8 |
|
disjdif2 |
|- ( ( ( M ..^ N ) i^i { N } ) = (/) -> ( ( M ..^ N ) \ { N } ) = ( M ..^ N ) ) |
9 |
7 8
|
mp1i |
|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ N ) \ { N } ) = ( M ..^ N ) ) |
10 |
4 9
|
eqtrd |
|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ ( N + 1 ) ) \ { N } ) = ( M ..^ N ) ) |