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