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 syl5bb A B B A + 1 a A + 1 B a
33 32 eqrdv A B B A + 1 A + 1 B =