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=ℤ