Metamath Proof Explorer


Theorem fzsplit

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 K M N M N = M K K + 1 N

Proof

Step Hyp Ref Expression
1 elfzuz K M N K M
2 peano2uz K M K + 1 M
3 1 2 syl K M N K + 1 M
4 elfzuz3 K M N N K
5 fzsplit2 K + 1 M N K M N = M K K + 1 N
6 3 4 5 syl2anc K M N M N = M K K + 1 N