This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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