Metamath Proof Explorer

Theorem nn0split

Description: Express the set of nonnegative integers as the disjoint (see nn0disj ) union of the first N + 1 values and the rest. (Contributed by AV, 8-Nov-2019)

Ref Expression
Assertion nn0split 
|- ( N e. NN0 -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )

Proof

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 ) ) ) )