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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
iccdificc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
iccdificc.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
iccdificc.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion iccdificc ( 𝜑 → ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵 (,] 𝐶 ) )

Proof

Step Hyp Ref Expression
1 iccdificc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 iccdificc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 iccdificc.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4 iccdificc.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝐵 ∈ ℝ* )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝐶 ∈ ℝ* )
7 iccssxr ⊢ ( 𝐴 [,] 𝐶 ) ⊆ ℝ*
8 eldifi ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐶 ) )
9 7 8 sselid ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ* )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ℝ* )
11 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → 𝐴 ∈ ℝ* )
12 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → 𝐵 ∈ ℝ* )
13 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → 𝑥 ∈ ℝ* )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝐴 ∈ ℝ* )
15 8 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐶 ) )
16 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ) → 𝐴 ≤ 𝑥 )
17 14 6 15 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝐴 ≤ 𝑥 )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → 𝐴 ≤ 𝑥 )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → ¬ 𝐵 < 𝑥 )
20 10 5 xrlenltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥 ) )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → ( 𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥 ) )
22 19 21 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → 𝑥 ≤ 𝐵 )
23 11 12 13 18 22 eliccxrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
24 eldifn ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) → ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
25 24 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝐵 < 𝑥 ) → ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
26 23 25 condan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝐵 < 𝑥 )
27 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ) → 𝑥 ≤ 𝐶 )
28 14 6 15 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ≤ 𝐶 )
29 5 6 10 26 28 eliocd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
31 dfss3 ⊢ ( ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐵 (,] 𝐶 ) ↔ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
32 30 31 sylibr ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐵 (,] 𝐶 ) )
33 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐴 ∈ ℝ* )
34 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐶 ∈ ℝ* )
35 iocssxr ⊢ ( 𝐵 (,] 𝐶 ) ⊆ ℝ*
36 id ⊢ ( 𝑥 ∈ ( 𝐵 (,] 𝐶 ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
37 35 36 sselid ⊢ ( 𝑥 ∈ ( 𝐵 (,] 𝐶 ) → 𝑥 ∈ ℝ* )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ∈ ℝ* )
39 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐵 ∈ ℝ* )
40 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐴 ≤ 𝐵 )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
42 iocgtlb ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐵 < 𝑥 )
43 39 34 41 42 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐵 < 𝑥 )
44 33 39 38 40 43 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐴 < 𝑥 )
45 33 38 44 xrltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐴 ≤ 𝑥 )
46 iocleub ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ≤ 𝐶 )
47 39 34 41 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ≤ 𝐶 )
48 33 34 38 45 47 eliccxrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐶 ) )
49 33 39 38 43 xrgtnelicc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
50 48 49 eldifd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ∈ ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) )
51 32 50 eqelssd ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐶 ) ∖ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵 (,] 𝐶 ) )