Step |
Hyp |
Ref |
Expression |
1 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
2 |
1
|
a1i |
|- ( N e. NN0 -> NN0 = ( ZZ>= ` 0 ) ) |
3 |
|
peano2nn0 |
|- ( N e. NN0 -> ( N + 1 ) e. NN0 ) |
4 |
3 1
|
eleqtrdi |
|- ( N e. NN0 -> ( N + 1 ) e. ( ZZ>= ` 0 ) ) |
5 |
|
uzsplit |
|- ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) ) |
6 |
4 5
|
syl |
|- ( N e. NN0 -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) ) |
7 |
|
nn0cn |
|- ( N e. NN0 -> N e. CC ) |
8 |
|
pncan1 |
|- ( N e. CC -> ( ( N + 1 ) - 1 ) = N ) |
9 |
7 8
|
syl |
|- ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N ) |
10 |
9
|
oveq2d |
|- ( N e. NN0 -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) ) |
11 |
10
|
uneq1d |
|- ( N e. NN0 -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) ) |
12 |
2 6 11
|
3eqtrd |
|- ( N e. NN0 -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) ) |