Metamath Proof Explorer

Theorem fzouzsplit

Description: Split an upper integer set into a half-open integer range and another upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 eluzelre 
 |-  ( B e. ( ZZ>= ` A ) -> B e. RR )
2 eluzelre 
 |-  ( x e. ( ZZ>= ` A ) -> x e. RR )
3 lelttric 
 |-  ( ( B e. RR /\ x e. RR ) -> ( B <_ x \/ x < B ) )
4 1 2 3 syl2an 
 |-  ( ( B e. ( ZZ>= ` A ) /\ x e. ( ZZ>= ` A ) ) -> ( B <_ x \/ x < B ) )
5 4 orcomd 
 |-  ( ( B e. ( ZZ>= ` A ) /\ x e. ( ZZ>= ` A ) ) -> ( x < B \/ B <_ x ) )
6 id 
 |-  ( x e. ( ZZ>= ` A ) -> x e. ( ZZ>= ` A ) )
7 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
8 elfzo2 
 |-  ( x e. ( A ..^ B ) <-> ( x e. ( ZZ>= ` A ) /\ B e. ZZ /\ x < B ) )
9 df-3an 
 |-  ( ( x e. ( ZZ>= ` A ) /\ B e. ZZ /\ x < B ) <-> ( ( x e. ( ZZ>= ` A ) /\ B e. ZZ ) /\ x < B ) )
10 8 9 bitri 
 |-  ( x e. ( A ..^ B ) <-> ( ( x e. ( ZZ>= ` A ) /\ B e. ZZ ) /\ x < B ) )
11 10 baib 
 |-  ( ( x e. ( ZZ>= ` A ) /\ B e. ZZ ) -> ( x e. ( A ..^ B ) <-> x < B ) )
12 6 7 11 syl2anr 
 |-  ( ( B e. ( ZZ>= ` A ) /\ x e. ( ZZ>= ` A ) ) -> ( x e. ( A ..^ B ) <-> x < B ) )
13 eluzelz 
 |-  ( x e. ( ZZ>= ` A ) -> x e. ZZ )
14 eluz 
 |-  ( ( B e. ZZ /\ x e. ZZ ) -> ( x e. ( ZZ>= ` B ) <-> B <_ x ) )
15 7 13 14 syl2an 
 |-  ( ( B e. ( ZZ>= ` A ) /\ x e. ( ZZ>= ` A ) ) -> ( x e. ( ZZ>= ` B ) <-> B <_ x ) )
16 12 15 orbi12d 
 |-  ( ( B e. ( ZZ>= ` A ) /\ x e. ( ZZ>= ` A ) ) -> ( ( x e. ( A ..^ B ) \/ x e. ( ZZ>= ` B ) ) <-> ( x < B \/ B <_ x ) ) )
17 5 16 mpbird 
 |-  ( ( B e. ( ZZ>= ` A ) /\ x e. ( ZZ>= ` A ) ) -> ( x e. ( A ..^ B ) \/ x e. ( ZZ>= ` B ) ) )
18 17 ex 
 |-  ( B e. ( ZZ>= ` A ) -> ( x e. ( ZZ>= ` A ) -> ( x e. ( A ..^ B ) \/ x e. ( ZZ>= ` B ) ) ) )
19 elun 
 |-  ( x e. ( ( A ..^ B ) u. ( ZZ>= ` B ) ) <-> ( x e. ( A ..^ B ) \/ x e. ( ZZ>= ` B ) ) )
20 18 19 syl6ibr 
 |-  ( B e. ( ZZ>= ` A ) -> ( x e. ( ZZ>= ` A ) -> x e. ( ( A ..^ B ) u. ( ZZ>= ` B ) ) ) )
21 20 ssrdv 
 |-  ( B e. ( ZZ>= ` A ) -> ( ZZ>= ` A ) C_ ( ( A ..^ B ) u. ( ZZ>= ` B ) ) )
22 elfzouz 
 |-  ( x e. ( A ..^ B ) -> x e. ( ZZ>= ` A ) )
23 22 ssriv 
 |-  ( A ..^ B ) C_ ( ZZ>= ` A )
24 23 a1i 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ B ) C_ ( ZZ>= ` A ) )
25 uzss 
 |-  ( B e. ( ZZ>= ` A ) -> ( ZZ>= ` B ) C_ ( ZZ>= ` A ) )
26 24 25 unssd 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A ..^ B ) u. ( ZZ>= ` B ) ) C_ ( ZZ>= ` A ) )
27 21 26 eqssd 
 |-  ( B e. ( ZZ>= ` A ) -> ( ZZ>= ` A ) = ( ( A ..^ B ) u. ( ZZ>= ` B ) ) )