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 ) ) )