Metamath Proof Explorer


Theorem iccdificc

Description: The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses iccdificc.a φ A *
iccdificc.b φ B *
iccdificc.c φ C *
iccdificc.4 φ A B
Assertion iccdificc φ A C A B = B C

Proof

Step Hyp Ref Expression
1 iccdificc.a φ A *
2 iccdificc.b φ B *
3 iccdificc.c φ C *
4 iccdificc.4 φ A B
5 2 adantr φ x A C A B B *
6 3 adantr φ x A C A B C *
7 iccssxr A C *
8 eldifi x A C A B x A C
9 7 8 sseldi x A C A B x *
10 9 adantl φ x A C A B x *
11 1 ad2antrr φ x A C A B ¬ B < x A *
12 5 adantr φ x A C A B ¬ B < x B *
13 10 adantr φ x A C A B ¬ B < x x *
14 1 adantr φ x A C A B A *
15 8 adantl φ x A C A B x A C
16 iccgelb A * C * x A C A x
17 14 6 15 16 syl3anc φ x A C A B A x
18 17 adantr φ x A C A B ¬ B < x A x
19 simpr φ x A C A B ¬ B < x ¬ B < x
20 10 5 xrlenltd φ x A C A B x B ¬ B < x
21 20 adantr φ x A C A B ¬ B < x x B ¬ B < x
22 19 21 mpbird φ x A C A B ¬ B < x x B
23 11 12 13 18 22 eliccxrd φ x A C A B ¬ B < x x A B
24 eldifn x A C A B ¬ x A B
25 24 ad2antlr φ x A C A B ¬ B < x ¬ x A B
26 23 25 condan φ x A C A B B < x
27 iccleub A * C * x A C x C
28 14 6 15 27 syl3anc φ x A C A B x C
29 5 6 10 26 28 eliocd φ x A C A B x B C
30 29 ralrimiva φ x A C A B x B C
31 dfss3 A C A B B C x A C A B x B C
32 30 31 sylibr φ A C A B B C
33 1 adantr φ x B C A *
34 3 adantr φ x B C C *
35 iocssxr B C *
36 id x B C x B C
37 35 36 sseldi x B C x *
38 37 adantl φ x B C x *
39 2 adantr φ x B C B *
40 4 adantr φ x B C A B
41 simpr φ x B C x B C
42 iocgtlb B * C * x B C B < x
43 39 34 41 42 syl3anc φ x B C B < x
44 33 39 38 40 43 xrlelttrd φ x B C A < x
45 33 38 44 xrltled φ x B C A x
46 iocleub B * C * x B C x C
47 39 34 41 46 syl3anc φ x B C x C
48 33 34 38 45 47 eliccxrd φ x B C x A C
49 33 39 38 43 xrgtnelicc φ x B C ¬ x A B
50 48 49 eldifd φ x B C x A C A B
51 32 50 eqelssd φ A C A B = B C