Metamath Proof Explorer


Theorem fz0sn0fz1

Description: A finite set of sequential nonnegative integers is the union of the singleton containing 0 and a finite set of sequential positive integers. (Contributed by AV, 20-Mar-2021)

Ref Expression
Assertion fz0sn0fz1
|- ( N e. NN0 -> ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) )

Proof

Step Hyp Ref Expression
1 0elfz
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
2 fzsplit
 |-  ( 0 e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... 0 ) u. ( ( 0 + 1 ) ... N ) ) )
3 0p1e1
 |-  ( 0 + 1 ) = 1
4 3 oveq1i
 |-  ( ( 0 + 1 ) ... N ) = ( 1 ... N )
5 4 uneq2i
 |-  ( ( 0 ... 0 ) u. ( ( 0 + 1 ) ... N ) ) = ( ( 0 ... 0 ) u. ( 1 ... N ) )
6 2 5 eqtrdi
 |-  ( 0 e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... 0 ) u. ( 1 ... N ) ) )
7 1 6 syl
 |-  ( N e. NN0 -> ( 0 ... N ) = ( ( 0 ... 0 ) u. ( 1 ... N ) ) )
8 0z
 |-  0 e. ZZ
9 fzsn
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
10 8 9 mp1i
 |-  ( N e. NN0 -> ( 0 ... 0 ) = { 0 } )
11 10 uneq1d
 |-  ( N e. NN0 -> ( ( 0 ... 0 ) u. ( 1 ... N ) ) = ( { 0 } u. ( 1 ... N ) ) )
12 7 11 eqtrd
 |-  ( N e. NN0 -> ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) )