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
|- ( ph -> A e. RR* )
iccdificc.b
|- ( ph -> B e. RR* )
iccdificc.c
|- ( ph -> C e. RR* )
iccdificc.4
|- ( ph -> A <_ B )
Assertion iccdificc
|- ( ph -> ( ( A [,] C ) \ ( A [,] B ) ) = ( B (,] C ) )

Proof

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