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 e. ( ZZ>= ` M ) -> ( ZZ>= ` M ) = ( ( M ... ( N - 1 ) ) u. ( ZZ>= ` N ) ) )

Proof

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