Metamath Proof Explorer

Theorem nnsplit

Description: Express the set of positive integers as the disjoint (see nnuzdisj ) union of the first N values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Assertion nnsplit 
|- ( N e. NN -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1 a1i 
 |-  ( N e. NN -> NN = ( ZZ>= ` 1 ) )
3 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
4 3 1 eleqtrdi 
 |-  ( N e. NN -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
5 uzsplit 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
6 4 5 syl 
 |-  ( N e. NN -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
7 nncn 
 |-  ( N e. NN -> N e. CC )
8 1cnd 
 |-  ( N e. NN -> 1 e. CC )
9 7 8 pncand 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
10 9 oveq2d 
 |-  ( N e. NN -> ( 1 ... ( ( N + 1 ) - 1 ) ) = ( 1 ... N ) )
11 10 uneq1d 
 |-  ( N e. NN -> ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
12 2 6 11 3eqtrd 
 |-  ( N e. NN -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )