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 syl6eq ⊢ K ∈ M … N → M ..^ N ∖ M ..^ K = K ..^ N