This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )