Theorem fzisfzounsn

Description: A finite interval of integers as union of a half-open integer range and a singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018)

	Ref	Expression
Assertion	fzisfzounsn	|- ( B e. ( ZZ>= ` A ) -> ( A ... B ) = ( ( A ..^ B ) u. { B } ) )

Proof

Step	Hyp	Ref	Expression
1		eluzelz	|- ( B e. ( ZZ>= ` A ) -> B e. ZZ )
2		fzval3	|- ( B e. ZZ -> ( A ... B ) = ( A ..^ ( B + 1 ) ) )
3	1 2	syl	|- ( B e. ( ZZ>= ` A ) -> ( A ... B ) = ( A ..^ ( B + 1 ) ) )
4		fzosplitsn	|- ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. { B } ) )
5	3 4	eqtrd	|- ( B e. ( ZZ>= ` A ) -> ( A ... B ) = ( ( A ..^ B ) u. { B } ) )