Metamath Proof Explorer


Theorem fzsplit3

Description: Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017)

Ref Expression
Assertion fzsplit3 KMNMN=MK1KN

Proof

Step Hyp Ref Expression
1 elfzelz xMNx
2 1 zred xMNx
3 elfzelz KMNK
4 3 zred KMNK
5 1red KMN1
6 4 5 resubcld KMNK1
7 lelttric xK1xK1K1<x
8 2 6 7 syl2anr KMNxMNxK1K1<x
9 elfzuz xMNxM
10 1zzd KMN1
11 3 10 zsubcld KMNK1
12 elfz5 xMK1xMK1xK1
13 9 11 12 syl2anr KMNxMNxMK1xK1
14 elfzuz3 xMNNx
15 14 adantl KMNxMNNx
16 elfzuzb xKNxKNx
17 16 rbaib NxxKNxK
18 15 17 syl KMNxMNxKNxK
19 eluz KxxKKx
20 3 1 19 syl2an KMNxMNxKKx
21 zlem1lt KxKxK1<x
22 3 1 21 syl2an KMNxMNKxK1<x
23 18 20 22 3bitrd KMNxMNxKNK1<x
24 13 23 orbi12d KMNxMNxMK1xKNxK1K1<x
25 8 24 mpbird KMNxMNxMK1xKN
26 elfzuz xMK1xM
27 26 adantl KMNxMK1xM
28 elfzuz3 KMNNK
29 28 adantr KMNxMK1NK
30 elfzuz3 xMK1K1x
31 30 adantl KMNxMK1K1x
32 peano2uz K1xK-1+1x
33 31 32 syl KMNxMK1K-1+1x
34 4 recnd KMNK
35 5 recnd KMN1
36 34 35 npcand KMNK-1+1=K
37 36 eleq1d KMNK-1+1xKx
38 37 adantr KMNxMK1K-1+1xKx
39 33 38 mpbid KMNxMK1Kx
40 uztrn NKKxNx
41 29 39 40 syl2anc KMNxMK1Nx
42 elfzuzb xMNxMNx
43 27 41 42 sylanbrc KMNxMK1xMN
44 elfzuz xKNxK
45 elfzuz KMNKM
46 uztrn xKKMxM
47 44 45 46 syl2anr KMNxKNxM
48 elfzuz3 xKNNx
49 48 adantl KMNxKNNx
50 47 49 42 sylanbrc KMNxKNxMN
51 43 50 jaodan KMNxMK1xKNxMN
52 25 51 impbida KMNxMNxMK1xKN
53 elun xMK1KNxMK1xKN
54 52 53 bitr4di KMNxMNxMK1KN
55 54 eqrdv KMNMN=MK1KN