# 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)\cup {ℤ}_{\ge {B}}=ℤ$

### Proof

Step Hyp Ref Expression
1 elun ${⊢}{a}\in \left(\left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)\cup {ℤ}_{\ge {B}}\right)↔\left({a}\in \left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)\vee {a}\in {ℤ}_{\ge {B}}\right)$
2 ellz1 ${⊢}{A}\in ℤ\to \left({a}\in \left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)↔\left({a}\in ℤ\wedge {a}\le {A}\right)\right)$
3 2 3ad2ant1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left({a}\in \left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)↔\left({a}\in ℤ\wedge {a}\le {A}\right)\right)$
4 eluz1 ${⊢}{B}\in ℤ\to \left({a}\in {ℤ}_{\ge {B}}↔\left({a}\in ℤ\wedge {B}\le {a}\right)\right)$
5 4 3ad2ant2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left({a}\in {ℤ}_{\ge {B}}↔\left({a}\in ℤ\wedge {B}\le {a}\right)\right)$
6 3 5 orbi12d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left(\left({a}\in \left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)\vee {a}\in {ℤ}_{\ge {B}}\right)↔\left(\left({a}\in ℤ\wedge {a}\le {A}\right)\vee \left({a}\in ℤ\wedge {B}\le {a}\right)\right)\right)$
7 zre ${⊢}{a}\in ℤ\to {a}\in ℝ$
8 7 adantl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to {a}\in ℝ$
9 simpl1 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to {A}\in ℤ$
10 9 zred ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to {A}\in ℝ$
11 lelttric ${⊢}\left({a}\in ℝ\wedge {A}\in ℝ\right)\to \left({a}\le {A}\vee {A}<{a}\right)$
12 8 10 11 syl2anc ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to \left({a}\le {A}\vee {A}<{a}\right)$
13 simpll2 ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {B}\in ℤ$
14 13 zred ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {B}\in ℝ$
15 simpll1 ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {A}\in ℤ$
16 15 peano2zd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {A}+1\in ℤ$
17 16 zred ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {A}+1\in ℝ$
18 7 ad2antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {a}\in ℝ$
19 simpll3 ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {B}\le {A}+1$
20 zltp1le ${⊢}\left({A}\in ℤ\wedge {a}\in ℤ\right)\to \left({A}<{a}↔{A}+1\le {a}\right)$
21 20 3ad2antl1 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to \left({A}<{a}↔{A}+1\le {a}\right)$
22 21 biimpa ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {A}+1\le {a}$
23 14 17 18 19 22 letrd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\wedge {A}<{a}\right)\to {B}\le {a}$
24 23 ex ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to \left({A}<{a}\to {B}\le {a}\right)$
25 24 orim2d ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to \left(\left({a}\le {A}\vee {A}<{a}\right)\to \left({a}\le {A}\vee {B}\le {a}\right)\right)$
26 12 25 mpd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\wedge {a}\in ℤ\right)\to \left({a}\le {A}\vee {B}\le {a}\right)$
27 26 ex ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left({a}\in ℤ\to \left({a}\le {A}\vee {B}\le {a}\right)\right)$
28 27 pm4.71d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left({a}\in ℤ↔\left({a}\in ℤ\wedge \left({a}\le {A}\vee {B}\le {a}\right)\right)\right)$
29 andi ${⊢}\left({a}\in ℤ\wedge \left({a}\le {A}\vee {B}\le {a}\right)\right)↔\left(\left({a}\in ℤ\wedge {a}\le {A}\right)\vee \left({a}\in ℤ\wedge {B}\le {a}\right)\right)$
30 28 29 syl6rbb ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left(\left(\left({a}\in ℤ\wedge {a}\le {A}\right)\vee \left({a}\in ℤ\wedge {B}\le {a}\right)\right)↔{a}\in ℤ\right)$
31 6 30 bitrd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left(\left({a}\in \left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)\vee {a}\in {ℤ}_{\ge {B}}\right)↔{a}\in ℤ\right)$
32 1 31 syl5bb ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left({a}\in \left(\left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)\cup {ℤ}_{\ge {B}}\right)↔{a}\in ℤ\right)$
33 32 eqrdv ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\le {A}+1\right)\to \left(ℤ\setminus {ℤ}_{\ge \left({A}+1\right)}\right)\cup {ℤ}_{\ge {B}}=ℤ$