Metamath Proof Explorer

Theorem difioo

Description: The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017)

Ref Expression
Assertion difioo ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B→AC∖AB=BC

Proof

Step Hyp Ref Expression
1 incom ⊢AB∩BC=BC∩AB
2 joiniooico ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→AB∩BC=∅∧AB∪BC=AC
3 2 anassrs ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→AB∩BC=∅∧AB∪BC=AC
4 3 simpld ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→AB∩BC=∅
5 1 4 eqtr3id ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→BC∩AB=∅
6 3 simprd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→AB∪BC=AC
7 uncom ⊢BC∪AB=AB∪BC
8 7 a1i ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→BC∪AB=AB∪BC
9 simpll1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→A∈ℝ*
10 simpl3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B→C∈ℝ*
11 10 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→C∈ℝ*
12 9 xrleidd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→A≤A
13 simpr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→B≤C
14 ioossioo ⊢A∈ℝ*∧C∈ℝ*∧A≤A∧B≤C→AB⊆AC
15 9 11 12 13 14 syl22anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→AB⊆AC
16 ssequn2 ⊢AB⊆AC↔AC∪AB=AC
17 15 16 sylib ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→AC∪AB=AC
18 6 8 17 3eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→BC∪AB=AC∪AB
19 difeq ⊢AC∖AB=BC↔BC∩AB=∅∧BC∪AB=AC∪AB
20 5 18 19 sylanbrc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B≤C→AC∖AB=BC
21 simpll1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→A∈ℝ*
22 simpl2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B→B∈ℝ*
23 22 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→B∈ℝ*
24 21 xrleidd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→A≤A
25 10 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→C∈ℝ*
26 simpr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→C<B
27 25 23 26 xrltled ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→C≤B
28 ioossioo ⊢A∈ℝ*∧B∈ℝ*∧A≤A∧C≤B→AC⊆AB
29 21 23 24 27 28 syl22anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→AC⊆AB
30 ssdif0 ⊢AC⊆AB↔AC∖AB=∅
31 29 30 sylib ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→AC∖AB=∅
32 ico0 ⊢B∈ℝ*∧C∈ℝ*→BC=∅↔C≤B
33 32 biimpar ⊢B∈ℝ*∧C∈ℝ*∧C≤B→BC=∅
34 23 25 27 33 syl21anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→BC=∅
35 31 34 eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧C<B→AC∖AB=BC
36 xrlelttric ⊢B∈ℝ*∧C∈ℝ*→B≤C∨C<B
37 22 10 36 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B→B≤C∨C<B
38 20 35 37 mpjaodan ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B→AC∖AB=BC