Metamath Proof Explorer

Theorem lzunuz

Description: The union of a lower set of integers and an upper set of integers which abut or overlap is all of the integers. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion lzunuz 
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) = ZZ )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( a e. ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) <-> ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) \/ a e. ( ZZ>= ` B ) ) )
2 ellz1 
 |-  ( A e. ZZ -> ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) <-> ( a e. ZZ /\ a <_ A ) ) )
3 2 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) <-> ( a e. ZZ /\ a <_ A ) ) )
4 eluz1 
 |-  ( B e. ZZ -> ( a e. ( ZZ>= ` B ) <-> ( a e. ZZ /\ B <_ a ) ) )
5 4 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ( ZZ>= ` B ) <-> ( a e. ZZ /\ B <_ a ) ) )
6 3 5 orbi12d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) \/ a e. ( ZZ>= ` B ) ) <-> ( ( a e. ZZ /\ a <_ A ) \/ ( a e. ZZ /\ B <_ a ) ) ) )
7 zre 
 |-  ( a e. ZZ -> a e. RR )
8 7 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> a e. RR )
9 simpl1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> A e. ZZ )
10 9 zred 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> A e. RR )
11 lelttric 
 |-  ( ( a e. RR /\ A e. RR ) -> ( a <_ A \/ A < a ) )
12 8 10 11 syl2anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( a <_ A \/ A < a ) )
13 simpll2 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B e. ZZ )
14 13 zred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B e. RR )
15 simpll1 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> A e. ZZ )
16 15 peano2zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> ( A + 1 ) e. ZZ )
17 16 zred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> ( A + 1 ) e. RR )
18 7 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> a e. RR )
19 simpll3 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B <_ ( A + 1 ) )
20 zltp1le 
 |-  ( ( A e. ZZ /\ a e. ZZ ) -> ( A < a <-> ( A + 1 ) <_ a ) )
21 20 3ad2antl1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( A < a <-> ( A + 1 ) <_ a ) )
22 21 biimpa 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> ( A + 1 ) <_ a )
23 14 17 18 19 22 letrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B <_ a )
24 23 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( A < a -> B <_ a ) )
25 24 orim2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( ( a <_ A \/ A < a ) -> ( a <_ A \/ B <_ a ) ) )
26 12 25 mpd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( a <_ A \/ B <_ a ) )
27 26 ex 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ZZ -> ( a <_ A \/ B <_ a ) ) )
28 27 pm4.71d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ZZ <-> ( a e. ZZ /\ ( a <_ A \/ B <_ a ) ) ) )
29 andi 
 |-  ( ( a e. ZZ /\ ( a <_ A \/ B <_ a ) ) <-> ( ( a e. ZZ /\ a <_ A ) \/ ( a e. ZZ /\ B <_ a ) ) )
30 28 29 bitr2di 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ( a e. ZZ /\ a <_ A ) \/ ( a e. ZZ /\ B <_ a ) ) <-> a e. ZZ ) )
31 6 30 bitrd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) \/ a e. ( ZZ>= ` B ) ) <-> a e. ZZ ) )
32 1 31 bitrid 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) <-> a e. ZZ ) )
33 32 eqrdv 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) = ZZ )