Theorem 1fzopredsuc

Description: Join 0 and a successor to the beginning and the end of an open integer interval starting at 1. (Contributed by AV, 14-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0uz	|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
2		fzopredsuc	|- ( N e. ( ZZ>= ` 0 ) -> ( 0 ... N ) = ( ( { 0 } u. ( ( 0 + 1 ) ..^ N ) ) u. { N } ) )
3		0p1e1	|- ( 0 + 1 ) = 1
4	3	oveq1i	|- ( ( 0 + 1 ) ..^ N ) = ( 1 ..^ N )
5	4	uneq2i	|- ( { 0 } u. ( ( 0 + 1 ) ..^ N ) ) = ( { 0 } u. ( 1 ..^ N ) )
6	5	uneq1i	|- ( ( { 0 } u. ( ( 0 + 1 ) ..^ N ) ) u. { N } ) = ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } )
7	2 6	eqtrdi	|- ( N e. ( ZZ>= ` 0 ) -> ( 0 ... N ) = ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) )
8	1 7	sylbi	|- ( N e. NN0 -> ( 0 ... N ) = ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) )