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 ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → ℤ ∖ ℤ ≥ A + 1 ∪ ℤ ≥ B = ℤ

Proof

Step Hyp Ref Expression
1 elun ⊢ a ∈ ℤ ∖ ℤ ≥ A + 1 ∪ ℤ ≥ B ↔ a ∈ ℤ ∖ ℤ ≥ A + 1 ∨ a ∈ ℤ ≥ B
2 ellz1 ⊢ A ∈ ℤ → a ∈ ℤ ∖ ℤ ≥ A + 1 ↔ a ∈ ℤ ∧ a ≤ A
3 2 3ad2ant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ ∖ ℤ ≥ A + 1 ↔ a ∈ ℤ ∧ a ≤ A
4 eluz1 ⊢ B ∈ ℤ → a ∈ ℤ ≥ B ↔ a ∈ ℤ ∧ B ≤ a
5 4 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ ≥ B ↔ a ∈ ℤ ∧ B ≤ a
6 3 5 orbi12d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ ∖ ℤ ≥ A + 1 ∨ a ∈ ℤ ≥ B ↔ a ∈ ℤ ∧ a ≤ A ∨ a ∈ ℤ ∧ B ≤ a
7 zre ⊢ a ∈ ℤ → a ∈ ℝ
8 7 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → a ∈ ℝ
9 simpl1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → A ∈ ℤ
10 9 zred ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → A ∈ ℝ
11 lelttric ⊢ a ∈ ℝ ∧ A ∈ ℝ → a ≤ A ∨ A < a
12 8 10 11 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → a ≤ A ∨ A < a
13 simpll2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → B ∈ ℤ
14 13 zred ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → B ∈ ℝ
15 simpll1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → A ∈ ℤ
16 15 peano2zd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → A + 1 ∈ ℤ
17 16 zred ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → A + 1 ∈ ℝ
18 7 ad2antlr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → a ∈ ℝ
19 simpll3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → B ≤ A + 1
20 zltp1le ⊢ A ∈ ℤ ∧ a ∈ ℤ → A < a ↔ A + 1 ≤ a
21 20 3ad2antl1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → A < a ↔ A + 1 ≤ a
22 21 biimpa ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → A + 1 ≤ a
23 14 17 18 19 22 letrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ ∧ A < a → B ≤ a
24 23 ex ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → A < a → B ≤ a
25 24 orim2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → a ≤ A ∨ A < a → a ≤ A ∨ B ≤ a
26 12 25 mpd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 ∧ a ∈ ℤ → a ≤ A ∨ B ≤ a
27 26 ex ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ → a ≤ A ∨ B ≤ a
28 27 pm4.71d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ ↔ a ∈ ℤ ∧ a ≤ A ∨ B ≤ a
29 andi ⊢ a ∈ ℤ ∧ a ≤ A ∨ B ≤ a ↔ a ∈ ℤ ∧ a ≤ A ∨ a ∈ ℤ ∧ B ≤ a
30 28 29 bitr2di ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ ∧ a ≤ A ∨ a ∈ ℤ ∧ B ≤ a ↔ a ∈ ℤ
31 6 30 bitrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ ∖ ℤ ≥ A + 1 ∨ a ∈ ℤ ≥ B ↔ a ∈ ℤ
32 1 31 bitrid ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → a ∈ ℤ ∖ ℤ ≥ A + 1 ∪ ℤ ≥ B ↔ a ∈ ℤ
33 32 eqrdv ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≤ A + 1 → ℤ ∖ ℤ ≥ A + 1 ∪ ℤ ≥ B = ℤ