Theorem fzosplitsni

Description: Membership in a half-open range extended by a singleton. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Assertion	fzosplitsni	|- ( B e. ( ZZ>= ` A ) -> ( C e. ( A ..^ ( B + 1 ) ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzosplitsn	|- ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. { B } ) )
2	1	eleq2d	|- ( B e. ( ZZ>= ` A ) -> ( C e. ( A ..^ ( B + 1 ) ) <-> C e. ( ( A ..^ B ) u. { B } ) ) )
3		elun	|- ( C e. ( ( A ..^ B ) u. { B } ) <-> ( C e. ( A ..^ B ) \/ C e. { B } ) )
4		elsn2g	|- ( B e. ( ZZ>= ` A ) -> ( C e. { B } <-> C = B ) )
5	4	orbi2d	|- ( B e. ( ZZ>= ` A ) -> ( ( C e. ( A ..^ B ) \/ C e. { B } ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )
6	3 5	syl5bb	|- ( B e. ( ZZ>= ` A ) -> ( C e. ( ( A ..^ B ) u. { B } ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )
7	2 6	bitrd	|- ( B e. ( ZZ>= ` A ) -> ( C e. ( A ..^ ( B + 1 ) ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )