Metamath Proof Explorer

Theorem fzospliti

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

Ref Expression
Assertion fzospliti 
|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A e. ( B ..^ D ) \/ A e. ( D ..^ C ) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( D e. ZZ -> D e. RR )
2 elfzoelz 
 |-  ( A e. ( B ..^ C ) -> A e. ZZ )
3 2 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. ZZ )
4 3 zred 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. RR )
5 lelttric 
 |-  ( ( D e. RR /\ A e. RR ) -> ( D <_ A \/ A < D ) )
6 1 4 5 syl2an2 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( D <_ A \/ A < D ) )
7 6 orcomd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A < D \/ D <_ A ) )
8 elfzole1 
 |-  ( A e. ( B ..^ C ) -> B <_ A )
9 8 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B <_ A )
10 9 a1d 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A < D -> B <_ A ) )
11 10 ancrd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A < D -> ( B <_ A /\ A < D ) ) )
12 elfzolt2 
 |-  ( A e. ( B ..^ C ) -> A < C )
13 12 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A < C )
14 13 a1d 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( D <_ A -> A < C ) )
15 14 ancld 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( D <_ A -> ( D <_ A /\ A < C ) ) )
16 11 15 orim12d 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( ( A < D \/ D <_ A ) -> ( ( B <_ A /\ A < D ) \/ ( D <_ A /\ A < C ) ) ) )
17 7 16 mpd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( ( B <_ A /\ A < D ) \/ ( D <_ A /\ A < C ) ) )
18 elfzoel1 
 |-  ( A e. ( B ..^ C ) -> B e. ZZ )
19 18 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B e. ZZ )
20 simpr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> D e. ZZ )
21 elfzo 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ D e. ZZ ) -> ( A e. ( B ..^ D ) <-> ( B <_ A /\ A < D ) ) )
22 3 19 20 21 syl3anc 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A e. ( B ..^ D ) <-> ( B <_ A /\ A < D ) ) )
23 elfzoel2 
 |-  ( A e. ( B ..^ C ) -> C e. ZZ )
24 23 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> C e. ZZ )
25 elfzo 
 |-  ( ( A e. ZZ /\ D e. ZZ /\ C e. ZZ ) -> ( A e. ( D ..^ C ) <-> ( D <_ A /\ A < C ) ) )
26 3 20 24 25 syl3anc 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A e. ( D ..^ C ) <-> ( D <_ A /\ A < C ) ) )
27 22 26 orbi12d 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( ( A e. ( B ..^ D ) \/ A e. ( D ..^ C ) ) <-> ( ( B <_ A /\ A < D ) \/ ( D <_ A /\ A < C ) ) ) )
28 17 27 mpbird 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A e. ( B ..^ D ) \/ A e. ( D ..^ C ) ) )