Description: Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 13-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | fzsplit |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuz | ||
2 | peano2uz | ||
3 | 1 2 | syl | |
4 | elfzuz3 | ||
5 | fzsplit2 | ||
6 | 3 4 5 | syl2anc |