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