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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 ) )