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