Metamath Proof Explorer

Theorem fzsplit2

Description: Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Assertion fzsplit2 
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( x e. ( M ... N ) -> x e. ZZ )
2 1 zred 
 |-  ( x e. ( M ... N ) -> x e. RR )
3 eluzel2 
 |-  ( N e. ( ZZ>= ` K ) -> K e. ZZ )
4 3 adantl 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> K e. ZZ )
5 4 zred 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> K e. RR )
6 lelttric 
 |-  ( ( x e. RR /\ K e. RR ) -> ( x <_ K \/ K < x ) )
7 2 5 6 syl2anr 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x <_ K \/ K < x ) )
8 elfzuz 
 |-  ( x e. ( M ... N ) -> x e. ( ZZ>= ` M ) )
9 elfz5 
 |-  ( ( x e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( x e. ( M ... K ) <-> x <_ K ) )
10 8 4 9 syl2anr 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( M ... K ) <-> x <_ K ) )
11 simpl 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
12 eluzelz 
 |-  ( ( K + 1 ) e. ( ZZ>= ` M ) -> ( K + 1 ) e. ZZ )
13 11 12 syl 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( K + 1 ) e. ZZ )
14 eluz 
 |-  ( ( ( K + 1 ) e. ZZ /\ x e. ZZ ) -> ( x e. ( ZZ>= ` ( K + 1 ) ) <-> ( K + 1 ) <_ x ) )
15 13 1 14 syl2an 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( ZZ>= ` ( K + 1 ) ) <-> ( K + 1 ) <_ x ) )
16 elfzuz3 
 |-  ( x e. ( M ... N ) -> N e. ( ZZ>= ` x ) )
17 16 adantl 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> N e. ( ZZ>= ` x ) )
18 elfzuzb 
 |-  ( x e. ( ( K + 1 ) ... N ) <-> ( x e. ( ZZ>= ` ( K + 1 ) ) /\ N e. ( ZZ>= ` x ) ) )
19 18 rbaib 
 |-  ( N e. ( ZZ>= ` x ) -> ( x e. ( ( K + 1 ) ... N ) <-> x e. ( ZZ>= ` ( K + 1 ) ) ) )
20 17 19 syl 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( ( K + 1 ) ... N ) <-> x e. ( ZZ>= ` ( K + 1 ) ) ) )
21 zltp1le 
 |-  ( ( K e. ZZ /\ x e. ZZ ) -> ( K < x <-> ( K + 1 ) <_ x ) )
22 4 1 21 syl2an 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( K < x <-> ( K + 1 ) <_ x ) )
23 15 20 22 3bitr4d 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( ( K + 1 ) ... N ) <-> K < x ) )
24 10 23 orbi12d 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) <-> ( x <_ K \/ K < x ) ) )
25 7 24 mpbird 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) )
26 elfzuz 
 |-  ( x e. ( M ... K ) -> x e. ( ZZ>= ` M ) )
27 26 adantl 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... K ) ) -> x e. ( ZZ>= ` M ) )
28 simpr 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> N e. ( ZZ>= ` K ) )
29 elfzuz3 
 |-  ( x e. ( M ... K ) -> K e. ( ZZ>= ` x ) )
30 uztrn 
 |-  ( ( N e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` x ) ) -> N e. ( ZZ>= ` x ) )
31 28 29 30 syl2an 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... K ) ) -> N e. ( ZZ>= ` x ) )
32 elfzuzb 
 |-  ( x e. ( M ... N ) <-> ( x e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` x ) ) )
33 27 31 32 sylanbrc 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... K ) ) -> x e. ( M ... N ) )
34 elfzuz 
 |-  ( x e. ( ( K + 1 ) ... N ) -> x e. ( ZZ>= ` ( K + 1 ) ) )
35 uztrn 
 |-  ( ( x e. ( ZZ>= ` ( K + 1 ) ) /\ ( K + 1 ) e. ( ZZ>= ` M ) ) -> x e. ( ZZ>= ` M ) )
36 34 11 35 syl2anr 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( ( K + 1 ) ... N ) ) -> x e. ( ZZ>= ` M ) )
37 elfzuz3 
 |-  ( x e. ( ( K + 1 ) ... N ) -> N e. ( ZZ>= ` x ) )
38 37 adantl 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( ( K + 1 ) ... N ) ) -> N e. ( ZZ>= ` x ) )
39 36 38 32 sylanbrc 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( ( K + 1 ) ... N ) ) -> x e. ( M ... N ) )
40 33 39 jaodan 
 |-  ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) ) -> x e. ( M ... N ) )
41 25 40 impbida 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( x e. ( M ... N ) <-> ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) ) )
42 elun 
 |-  ( x e. ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) <-> ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) )
43 41 42 bitr4di 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( x e. ( M ... N ) <-> x e. ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) ) )
44 43 eqrdv 
 |-  ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) )