Metamath Proof Explorer


Theorem uzsplit

Description: Express an upper integer set as the disjoint (see uzdisj ) union of the first N values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion uzsplit N M M = M N 1 N

Proof

Step Hyp Ref Expression
1 eluzelre N M N
2 eluzelre k M k
3 lelttric N k N k k < N
4 1 2 3 syl2an N M k M N k k < N
5 eluzelz N M N
6 eluzelz k M k
7 eluz N k k N N k
8 5 6 7 syl2an N M k M k N N k
9 eluzle k M M k
10 6 9 jca k M k M k
11 10 adantl N M k M k M k
12 eluzel2 k M M
13 elfzm11 M N k M N 1 k M k k < N
14 df-3an k M k k < N k M k k < N
15 13 14 bitrdi M N k M N 1 k M k k < N
16 12 5 15 syl2anr N M k M k M N 1 k M k k < N
17 11 16 mpbirand N M k M k M N 1 k < N
18 8 17 orbi12d N M k M k N k M N 1 N k k < N
19 4 18 mpbird N M k M k N k M N 1
20 19 orcomd N M k M k M N 1 k N
21 20 ex N M k M k M N 1 k N
22 elfzuz k M N 1 k M
23 22 a1i N M k M N 1 k M
24 uztrn k N N M k M
25 24 expcom N M k N k M
26 23 25 jaod N M k M N 1 k N k M
27 21 26 impbid N M k M k M N 1 k N
28 elun k M N 1 N k M N 1 k N
29 27 28 bitr4di N M k M k M N 1 N
30 29 eqrdv N M M = M N 1 N