Theorem fzosplit

Description: Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015)

	Ref	Expression
Assertion	fzosplit	|- ( D e. ( B ... C ) -> ( B ..^ C ) = ( ( B ..^ D ) u. ( D ..^ C ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( D e. ( B ... C ) /\ x e. ( B ..^ C ) ) -> x e. ( B ..^ C ) )
2		elfzelz	|- ( D e. ( B ... C ) -> D e. ZZ )
3	2	adantr	|- ( ( D e. ( B ... C ) /\ x e. ( B ..^ C ) ) -> D e. ZZ )
4		fzospliti	|- ( ( x e. ( B ..^ C ) /\ D e. ZZ ) -> ( x e. ( B ..^ D ) \/ x e. ( D ..^ C ) ) )
5	1 3 4	syl2anc	|- ( ( D e. ( B ... C ) /\ x e. ( B ..^ C ) ) -> ( x e. ( B ..^ D ) \/ x e. ( D ..^ C ) ) )
6		elun	|- ( x e. ( ( B ..^ D ) u. ( D ..^ C ) ) <-> ( x e. ( B ..^ D ) \/ x e. ( D ..^ C ) ) )
7	5 6	sylibr	|- ( ( D e. ( B ... C ) /\ x e. ( B ..^ C ) ) -> x e. ( ( B ..^ D ) u. ( D ..^ C ) ) )
8	7	ex	|- ( D e. ( B ... C ) -> ( x e. ( B ..^ C ) -> x e. ( ( B ..^ D ) u. ( D ..^ C ) ) ) )
9	8	ssrdv	|- ( D e. ( B ... C ) -> ( B ..^ C ) C_ ( ( B ..^ D ) u. ( D ..^ C ) ) )
10		elfzuz3	|- ( D e. ( B ... C ) -> C e. ( ZZ>= ` D ) )
11		fzoss2	|- ( C e. ( ZZ>= ` D ) -> ( B ..^ D ) C_ ( B ..^ C ) )
12	10 11	syl	|- ( D e. ( B ... C ) -> ( B ..^ D ) C_ ( B ..^ C ) )
13		elfzuz	|- ( D e. ( B ... C ) -> D e. ( ZZ>= ` B ) )
14		fzoss1	|- ( D e. ( ZZ>= ` B ) -> ( D ..^ C ) C_ ( B ..^ C ) )
15	13 14	syl	|- ( D e. ( B ... C ) -> ( D ..^ C ) C_ ( B ..^ C ) )
16	12 15	unssd	|- ( D e. ( B ... C ) -> ( ( B ..^ D ) u. ( D ..^ C ) ) C_ ( B ..^ C ) )
17	9 16	eqssd	|- ( D e. ( B ... C ) -> ( B ..^ C ) = ( ( B ..^ D ) u. ( D ..^ C ) ) )