Description: Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | fzsplit3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzelz | |
|
2 | 1 | zred | |
3 | elfzelz | |
|
4 | 3 | zred | |
5 | 1red | |
|
6 | 4 5 | resubcld | |
7 | lelttric | |
|
8 | 2 6 7 | syl2anr | |
9 | elfzuz | |
|
10 | 1zzd | |
|
11 | 3 10 | zsubcld | |
12 | elfz5 | |
|
13 | 9 11 12 | syl2anr | |
14 | elfzuz3 | |
|
15 | 14 | adantl | |
16 | elfzuzb | |
|
17 | 16 | rbaib | |
18 | 15 17 | syl | |
19 | eluz | |
|
20 | 3 1 19 | syl2an | |
21 | zlem1lt | |
|
22 | 3 1 21 | syl2an | |
23 | 18 20 22 | 3bitrd | |
24 | 13 23 | orbi12d | |
25 | 8 24 | mpbird | |
26 | elfzuz | |
|
27 | 26 | adantl | |
28 | elfzuz3 | |
|
29 | 28 | adantr | |
30 | elfzuz3 | |
|
31 | 30 | adantl | |
32 | peano2uz | |
|
33 | 31 32 | syl | |
34 | 4 | recnd | |
35 | 5 | recnd | |
36 | 34 35 | npcand | |
37 | 36 | eleq1d | |
38 | 37 | adantr | |
39 | 33 38 | mpbid | |
40 | uztrn | |
|
41 | 29 39 40 | syl2anc | |
42 | elfzuzb | |
|
43 | 27 41 42 | sylanbrc | |
44 | elfzuz | |
|
45 | elfzuz | |
|
46 | uztrn | |
|
47 | 44 45 46 | syl2anr | |
48 | elfzuz3 | |
|
49 | 48 | adantl | |
50 | 47 49 42 | sylanbrc | |
51 | 43 50 | jaodan | |
52 | 25 51 | impbida | |
53 | elun | |
|
54 | 52 53 | bitr4di | |
55 | 54 | eqrdv | |