Step | Hyp | Ref
| Expression |
1 | | iccdificc.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
2 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐵 ∈
ℝ*) |
3 | | iccdificc.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
4 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐶 ∈
ℝ*) |
5 | | iccssxr 12256 |
. . . . . . 7
⊢ (𝐴[,]𝐶) ⊆
ℝ* |
6 | | eldifi 3732 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐶)) |
7 | 5, 6 | sseldi 3601 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ*) |
8 | 7 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ ℝ*) |
9 | | iccdificc.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
10 | 9 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐴 ∈
ℝ*) |
11 | 2 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐵 ∈
ℝ*) |
12 | 8 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*) |
13 | 9 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐴 ∈
ℝ*) |
14 | 6 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐴[,]𝐶)) |
15 | | iccgelb 12230 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐶)) → 𝐴 ≤ 𝑥) |
16 | 13, 4, 14, 15 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐴 ≤ 𝑥) |
17 | 16 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐴 ≤ 𝑥) |
18 | | simpr 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → ¬ 𝐵 < 𝑥) |
19 | 8, 2 | xrlenltd 10104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → (𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥)) |
20 | 19 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → (𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥)) |
21 | 18, 20 | mpbird 247 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ≤ 𝐵) |
22 | 10, 11, 12, 17, 21 | eliccxrd 39753 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ∈ (𝐴[,]𝐵)) |
23 | | eldifn 3733 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
24 | 23 | ad2antlr 763 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
25 | 22, 24 | condan 835 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐵 < 𝑥) |
26 | | iccleub 12229 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐶)) → 𝑥 ≤ 𝐶) |
27 | 13, 4, 14, 26 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ≤ 𝐶) |
28 | 2, 4, 8, 25, 27 | eliocd 39730 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐵(,]𝐶)) |
29 | 28 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))𝑥 ∈ (𝐵(,]𝐶)) |
30 | | dfss3 3592 |
. . 3
⊢ (((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) ⊆ (𝐵(,]𝐶) ↔ ∀𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))𝑥 ∈ (𝐵(,]𝐶)) |
31 | 29, 30 | sylibr 224 |
. 2
⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) ⊆ (𝐵(,]𝐶)) |
32 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ∈
ℝ*) |
33 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐶 ∈
ℝ*) |
34 | | iocssxr 12257 |
. . . . . . . 8
⊢ (𝐵(,]𝐶) ⊆
ℝ* |
35 | | id 22 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
36 | 34, 35 | sseldi 3601 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ ℝ*) |
37 | 36 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ℝ*) |
38 | 1 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 ∈
ℝ*) |
39 | | iccdificc.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
40 | 39 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ≤ 𝐵) |
41 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐵(,]𝐶)) |
42 | | iocgtlb 39724 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
43 | 38, 33, 41, 42 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
44 | 32, 38, 37, 40, 43 | xrlelttrd 11991 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 < 𝑥) |
45 | 32, 37, 44 | xrltled 39486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ≤ 𝑥) |
46 | | iocleub 39725 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
47 | 38, 33, 41, 46 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
48 | 32, 33, 37, 45, 47 | eliccxrd 39753 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐴[,]𝐶)) |
49 | 32, 38, 37, 43 | xrgtnelicc 39765 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
50 | 48, 49 | eldifd 3585 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) |
51 | 50 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) |
52 | | dfss3 3592 |
. . 3
⊢ ((𝐵(,]𝐶) ⊆ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) ↔ ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) |
53 | 51, 52 | sylibr 224 |
. 2
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) |
54 | 31, 53 | eqssd 3620 |
1
⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) = (𝐵(,]𝐶)) |