This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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