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	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) ) = ( 𝐾 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fzosplit	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ..^ 𝑁 ) = ( ( 𝑀 ..^ 𝐾 ) ∪ ( 𝐾 ..^ 𝑁 ) ) )
2	1	difeq1d	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) ) = ( ( ( 𝑀 ..^ 𝐾 ) ∪ ( 𝐾 ..^ 𝑁 ) ) ∖ ( 𝑀 ..^ 𝐾 ) ) )
3		difundir	⊢ ( ( ( 𝑀 ..^ 𝐾 ) ∪ ( 𝐾 ..^ 𝑁 ) ) ∖ ( 𝑀 ..^ 𝐾 ) ) = ( ( ( 𝑀 ..^ 𝐾 ) ∖ ( 𝑀 ..^ 𝐾 ) ) ∪ ( ( 𝐾 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) ) )
4		difid	⊢ ( ( 𝑀 ..^ 𝐾 ) ∖ ( 𝑀 ..^ 𝐾 ) ) = ∅
5		incom	⊢ ( ( 𝐾 ..^ 𝑁 ) ∩ ( 𝑀 ..^ 𝐾 ) ) = ( ( 𝑀 ..^ 𝐾 ) ∩ ( 𝐾 ..^ 𝑁 ) )
6		fzodisj	⊢ ( ( 𝑀 ..^ 𝐾 ) ∩ ( 𝐾 ..^ 𝑁 ) ) = ∅
7	5 6	eqtri	⊢ ( ( 𝐾 ..^ 𝑁 ) ∩ ( 𝑀 ..^ 𝐾 ) ) = ∅
8		disj3	⊢ ( ( ( 𝐾 ..^ 𝑁 ) ∩ ( 𝑀 ..^ 𝐾 ) ) = ∅ ↔ ( 𝐾 ..^ 𝑁 ) = ( ( 𝐾 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) ) )
9	7 8	mpbi	⊢ ( 𝐾 ..^ 𝑁 ) = ( ( 𝐾 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) )
10	9	eqcomi	⊢ ( ( 𝐾 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) ) = ( 𝐾 ..^ 𝑁 )
11	4 10	uneq12i	⊢ ( ( ( 𝑀 ..^ 𝐾 ) ∖ ( 𝑀 ..^ 𝐾 ) ) ∪ ( ( 𝐾 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) ) ) = ( ∅ ∪ ( 𝐾 ..^ 𝑁 ) )
12		0un	⊢ ( ∅ ∪ ( 𝐾 ..^ 𝑁 ) ) = ( 𝐾 ..^ 𝑁 )
13	3 11 12	3eqtri	⊢ ( ( ( 𝑀 ..^ 𝐾 ) ∪ ( 𝐾 ..^ 𝑁 ) ) ∖ ( 𝑀 ..^ 𝐾 ) ) = ( 𝐾 ..^ 𝑁 )
14	2 13	eqtrdi	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) ∖ ( 𝑀 ..^ 𝐾 ) ) = ( 𝐾 ..^ 𝑁 ) )