Metamath Proof Explorer


Theorem fzodif1

Description: Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023)

Ref Expression
Assertion fzodif1 K M N M ..^ N M ..^ K = K ..^ N

Proof

Step Hyp Ref Expression
1 fzosplit K M N M ..^ N = M ..^ K K ..^ N
2 1 difeq1d K M N M ..^ N M ..^ K = M ..^ K K ..^ N M ..^ K
3 difundir M ..^ K K ..^ N M ..^ K = M ..^ K M ..^ K K ..^ N M ..^ K
4 difid M ..^ K M ..^ K =
5 incom K ..^ N M ..^ K = M ..^ K K ..^ N
6 fzodisj M ..^ K K ..^ N =
7 5 6 eqtri K ..^ N M ..^ K =
8 disj3 K ..^ N M ..^ K = K ..^ N = K ..^ N M ..^ K
9 7 8 mpbi K ..^ N = K ..^ N M ..^ K
10 9 eqcomi K ..^ N M ..^ K = K ..^ N
11 4 10 uneq12i M ..^ K M ..^ K K ..^ N M ..^ K = K ..^ N
12 0un K ..^ N = K ..^ N
13 3 11 12 3eqtri M ..^ K K ..^ N M ..^ K = K ..^ N
14 2 13 eqtrdi K M N M ..^ N M ..^ K = K ..^ N