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

Metamath Proof Explorer

Theorem fzo0sn0fzo1

Description: A half-open range of nonnegative integers is the union of the singleton set containing 0 and a half-open range of positive integers. (Contributed by Alexander van der Vekens, 18-May-2018)

Ref Expression
Assertion fzo0sn0fzo1 
|- ( N e. NN -> ( 0 ..^ N ) = ( { 0 } u. ( 1 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 1 a1i 
 |-  ( N e. NN -> 1 e. NN0 )
3 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
4 nnge1 
 |-  ( N e. NN -> 1 <_ N )
5 elfz2nn0 
 |-  ( 1 e. ( 0 ... N ) <-> ( 1 e. NN0 /\ N e. NN0 /\ 1 <_ N ) )
6 2 3 4 5 syl3anbrc 
 |-  ( N e. NN -> 1 e. ( 0 ... N ) )
7 fzosplit 
 |-  ( 1 e. ( 0 ... N ) -> ( 0 ..^ N ) = ( ( 0 ..^ 1 ) u. ( 1 ..^ N ) ) )
8 6 7 syl 
 |-  ( N e. NN -> ( 0 ..^ N ) = ( ( 0 ..^ 1 ) u. ( 1 ..^ N ) ) )
9 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
10 9 a1i 
 |-  ( N e. NN -> ( 0 ..^ 1 ) = { 0 } )
11 10 uneq1d 
 |-  ( N e. NN -> ( ( 0 ..^ 1 ) u. ( 1 ..^ N ) ) = ( { 0 } u. ( 1 ..^ N ) ) )
12 8 11 eqtrd 
 |-  ( N e. NN -> ( 0 ..^ N ) = ( { 0 } u. ( 1 ..^ N ) ) )