Step | Hyp | Ref
| Expression |
1 | | iccdificc.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐵 ∈
ℝ*) |
3 | | iccdificc.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
4 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐶 ∈
ℝ*) |
5 | | iccssxr 13018 |
. . . . . . 7
⊢ (𝐴[,]𝐶) ⊆
ℝ* |
6 | | eldifi 4041 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐶)) |
7 | 5, 6 | sseldi 3899 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ*) |
8 | 7 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ ℝ*) |
9 | | iccdificc.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
10 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐴 ∈
ℝ*) |
11 | 2 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐵 ∈
ℝ*) |
12 | 8 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*) |
13 | 9 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐴 ∈
ℝ*) |
14 | 6 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐴[,]𝐶)) |
15 | | iccgelb 12991 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐶)) → 𝐴 ≤ 𝑥) |
16 | 13, 4, 14, 15 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐴 ≤ 𝑥) |
17 | 16 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐴 ≤ 𝑥) |
18 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → ¬ 𝐵 < 𝑥) |
19 | 8, 2 | xrlenltd 10899 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → (𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥)) |
20 | 19 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → (𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥)) |
21 | 18, 20 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ≤ 𝐵) |
22 | 10, 11, 12, 17, 21 | eliccxrd 42740 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ∈ (𝐴[,]𝐵)) |
23 | | eldifn 4042 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
24 | 23 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
25 | 22, 24 | condan 818 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐵 < 𝑥) |
26 | | iccleub 12990 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐶)) → 𝑥 ≤ 𝐶) |
27 | 13, 4, 14, 26 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ≤ 𝐶) |
28 | 2, 4, 8, 25, 27 | eliocd 42720 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐵(,]𝐶)) |
29 | 28 | ralrimiva 3105 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))𝑥 ∈ (𝐵(,]𝐶)) |
30 | | dfss3 3888 |
. . 3
⊢ (((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) ⊆ (𝐵(,]𝐶) ↔ ∀𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))𝑥 ∈ (𝐵(,]𝐶)) |
31 | 29, 30 | sylibr 237 |
. 2
⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) ⊆ (𝐵(,]𝐶)) |
32 | 9 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ∈
ℝ*) |
33 | 3 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐶 ∈
ℝ*) |
34 | | iocssxr 13019 |
. . . . . 6
⊢ (𝐵(,]𝐶) ⊆
ℝ* |
35 | | id 22 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
36 | 34, 35 | sseldi 3899 |
. . . . 5
⊢ (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ ℝ*) |
37 | 36 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ℝ*) |
38 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 ∈
ℝ*) |
39 | | iccdificc.4 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
40 | 39 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ≤ 𝐵) |
41 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐵(,]𝐶)) |
42 | | iocgtlb 42715 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
43 | 38, 33, 41, 42 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
44 | 32, 38, 37, 40, 43 | xrlelttrd 12750 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 < 𝑥) |
45 | 32, 37, 44 | xrltled 12740 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ≤ 𝑥) |
46 | | iocleub 42716 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
47 | 38, 33, 41, 46 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
48 | 32, 33, 37, 45, 47 | eliccxrd 42740 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐴[,]𝐶)) |
49 | 32, 38, 37, 43 | xrgtnelicc 42751 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
50 | 48, 49 | eldifd 3877 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) |
51 | 31, 50 | eqelssd 3922 |
1
⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) = (𝐵(,]𝐶)) |