Theorem fzosplitsn

Description: Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		id	|- ( B e. ( ZZ>= ` A ) -> B e. ( ZZ>= ` A ) )
2		eluzelz	|- ( B e. ( ZZ>= ` A ) -> B e. ZZ )
3		uzid	|- ( B e. ZZ -> B e. ( ZZ>= ` B ) )
4		peano2uz	|- ( B e. ( ZZ>= ` B ) -> ( B + 1 ) e. ( ZZ>= ` B ) )
5	2 3 4	3syl	|- ( B e. ( ZZ>= ` A ) -> ( B + 1 ) e. ( ZZ>= ` B ) )
6		elfzuzb	|- ( B e. ( A ... ( B + 1 ) ) <-> ( B e. ( ZZ>= ` A ) /\ ( B + 1 ) e. ( ZZ>= ` B ) ) )
7	1 5 6	sylanbrc	|- ( B e. ( ZZ>= ` A ) -> B e. ( A ... ( B + 1 ) ) )
8		fzosplit	|- ( B e. ( A ... ( B + 1 ) ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. ( B ..^ ( B + 1 ) ) ) )
9	7 8	syl	|- ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. ( B ..^ ( B + 1 ) ) ) )
10		fzosn	|- ( B e. ZZ -> ( B ..^ ( B + 1 ) ) = { B } )
11	2 10	syl	|- ( B e. ( ZZ>= ` A ) -> ( B ..^ ( B + 1 ) ) = { B } )
12	11	uneq2d	|- ( B e. ( ZZ>= ` A ) -> ( ( A ..^ B ) u. ( B ..^ ( B + 1 ) ) ) = ( ( A ..^ B ) u. { B } ) )
13	9 12	eqtrd	|- ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. { B } ) )