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 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ ( 𝐴𝐵𝐵𝐶 ) ) → ( ( 𝐴 [,) 𝐶 ) ∖ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 [,) 𝐵 ) )