Theorem fz0dif1

Description: Split the first element of a finite set of sequential nonnegative integers. (Contributed by AV, 12-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0uz	|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
2		fzdif1	|- ( N e. ( ZZ>= ` 0 ) -> ( ( 0 ... N ) \ { 0 } ) = ( ( 0 + 1 ) ... N ) )
3	1 2	sylbi	|- ( N e. NN0 -> ( ( 0 ... N ) \ { 0 } ) = ( ( 0 + 1 ) ... N ) )
4		0p1e1	|- ( 0 + 1 ) = 1
5	4	oveq1i	|- ( ( 0 + 1 ) ... N ) = ( 1 ... N )
6	3 5	eqtrdi	|- ( N e. NN0 -> ( ( 0 ... N ) \ { 0 } ) = ( 1 ... N ) )