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

Metamath Proof Explorer

Theorem difico

Description: The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017)

		Ref	Expression
	Assertion	difico	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 [,) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		icodisj	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ )
2		undif4	⊢ ( ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ → ( ( 𝐴 [,) 𝐵 ) ∪ ( ( 𝐵 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) ) = ( ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) ∖ ( 𝐵 [,) 𝐶 ) ) )
3	1 2	syl	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( ( 𝐵 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) ) = ( ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) ∖ ( 𝐵 [,) 𝐶 ) ) )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( ( 𝐵 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) ) = ( ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) ∖ ( 𝐵 [,) 𝐶 ) ) )
5		difid	⊢ ( ( 𝐵 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) = ∅
6	5	uneq2i	⊢ ( ( 𝐴 [,) 𝐵 ) ∪ ( ( 𝐵 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) ) = ( ( 𝐴 [,) 𝐵 ) ∪ ∅ )
7		un0	⊢ ( ( 𝐴 [,) 𝐵 ) ∪ ∅ ) = ( 𝐴 [,) 𝐵 )
8	6 7	eqtri	⊢ ( ( 𝐴 [,) 𝐵 ) ∪ ( ( 𝐵 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) ) = ( 𝐴 [,) 𝐵 )
9	8	a1i	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( ( 𝐵 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) ) = ( 𝐴 [,) 𝐵 ) )
10		icoun	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 [,) 𝐶 ) )
11	10	difeq1d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) ∖ ( 𝐵 [,) 𝐶 ) ) = ( ( 𝐴 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) )
12	4 9 11	3eqtr3rd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 [,) 𝐵 ) )