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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≤ ( 𝐴 + 1 ) ) → ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) ∪ ( ℤ≥ ‘ 𝐵 ) ) = ℤ )

Proof

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