Step | Hyp | Ref
| Expression |
1 | | snunioo 12954 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) |
2 | 1 | 3expa 1119 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) |
3 | 2 | adantrr 717 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) |
4 | | lbico1 12877 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) |
5 | 4 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) |
6 | 5 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ (𝐴[,)𝐵)) |
7 | 6 | snssd 4697 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ (𝐴[,)𝐵)) |
8 | | iccid 12868 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) |
9 | 8 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,]𝐴) = {𝐴}) |
10 | 9 | ineq1d 4102 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ({𝐴} ∩ (𝐴(,)𝐵))) |
11 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈
ℝ*) |
12 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐵 ∈
ℝ*) |
13 | | df-icc 12830 |
. . . . . . . . . . 11
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
14 | | df-ioo 12827 |
. . . . . . . . . . 11
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
15 | | xrltnle 10788 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴 < 𝑤 ↔ ¬ 𝑤 ≤ 𝐴)) |
16 | 13, 14, 15 | ixxdisj 12838 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅) |
17 | 11, 11, 12, 16 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅) |
18 | 10, 17 | eqtr3d 2775 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∩ (𝐴(,)𝐵)) = ∅) |
19 | | uneqdifeq 4379 |
. . . . . . . 8
⊢ (({𝐴} ⊆ (𝐴[,)𝐵) ∧ ({𝐴} ∩ (𝐴(,)𝐵)) = ∅) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵))) |
20 | 7, 18, 19 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵))) |
21 | 3, 20 | mpbid 235 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)) |
22 | | mnfxr 10778 |
. . . . . . . . . 10
⊢ -∞
∈ ℝ* |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ ∈
ℝ*) |
24 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ < 𝐴) |
25 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 < 𝐵) |
26 | | xrre2 12648 |
. . . . . . . . 9
⊢
(((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (-∞ < 𝐴
∧ 𝐴 < 𝐵)) → 𝐴 ∈ ℝ) |
27 | 23, 11, 12, 24, 25, 26 | syl32anc 1379 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ ℝ) |
28 | | icombl 24318 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) ∈ dom
vol) |
29 | 27, 12, 28 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,)𝐵) ∈ dom vol) |
30 | 27 | snssd 4697 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ ℝ) |
31 | | ovolsn 24249 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(vol*‘{𝐴}) =
0) |
32 | 27, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (vol*‘{𝐴}) = 0) |
33 | | nulmbl 24289 |
. . . . . . . 8
⊢ (({𝐴} ⊆ ℝ ∧
(vol*‘{𝐴}) = 0)
→ {𝐴} ∈ dom
vol) |
34 | 30, 32, 33 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ∈ dom vol) |
35 | | difmbl 24297 |
. . . . . . 7
⊢ (((𝐴[,)𝐵) ∈ dom vol ∧ {𝐴} ∈ dom vol) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol) |
36 | 29, 34, 35 | syl2anc 587 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol) |
37 | 21, 36 | eqeltrrd 2834 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴(,)𝐵) ∈ dom vol) |
38 | 37 | expr 460 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 → (𝐴(,)𝐵) ∈ dom vol)) |
39 | | uncom 4043 |
. . . . . . . . 9
⊢ ((𝐵[,)+∞) ∪
(-∞(,)𝐵)) =
((-∞(,)𝐵) ∪
(𝐵[,)+∞)) |
40 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → -∞ ∈
ℝ*) |
41 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → 𝐵 ∈
ℝ*) |
42 | | pnfxr 10775 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → +∞ ∈
ℝ*) |
44 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 ∈
ℝ*) |
45 | | mnfle 12614 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
46 | 45 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → -∞ ≤ 𝐴) |
47 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
48 | 40, 44, 41, 46, 47 | xrlelttrd 12638 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → -∞ < 𝐵) |
49 | | pnfge 12610 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
50 | 41, 49 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → 𝐵 ≤ +∞) |
51 | | df-ico 12829 |
. . . . . . . . . . 11
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
52 | | xrlenlt 10786 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐵 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐵)) |
53 | | xrltletr 12635 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ +∞ ∈ ℝ*) → ((𝑤 < 𝐵 ∧ 𝐵 ≤ +∞) → 𝑤 < +∞)) |
54 | | xrltletr 12635 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((-∞ < 𝐵
∧ 𝐵 ≤ 𝑤) → -∞ < 𝑤)) |
55 | 14, 51, 52, 14, 53, 54 | ixxun 12839 |
. . . . . . . . . 10
⊢
(((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ < 𝐵 ∧ 𝐵 ≤ +∞)) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) =
(-∞(,)+∞)) |
56 | 40, 41, 43, 48, 50, 55 | syl32anc 1379 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) =
(-∞(,)+∞)) |
57 | 39, 56 | syl5eq 2785 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) =
(-∞(,)+∞)) |
58 | | ioomax 12898 |
. . . . . . . 8
⊢
(-∞(,)+∞) = ℝ |
59 | 57, 58 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ) |
60 | | ssun1 4062 |
. . . . . . . . 9
⊢ (𝐵[,)+∞) ⊆ ((𝐵[,)+∞) ∪
(-∞(,)𝐵)) |
61 | 60, 59 | sseqtrid 3929 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ⊆
ℝ) |
62 | | incom 4091 |
. . . . . . . . 9
⊢ ((𝐵[,)+∞) ∩
(-∞(,)𝐵)) =
((-∞(,)𝐵) ∩
(𝐵[,)+∞)) |
63 | 14, 51, 52 | ixxdisj 12838 |
. . . . . . . . . 10
⊢
((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞
∈ ℝ*) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅) |
64 | 40, 41, 43, 63 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅) |
65 | 62, 64 | syl5eq 2785 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ∅) |
66 | | uneqdifeq 4379 |
. . . . . . . 8
⊢ (((𝐵[,)+∞) ⊆ ℝ
∧ ((𝐵[,)+∞) ∩
(-∞(,)𝐵)) = ∅)
→ (((𝐵[,)+∞)
∪ (-∞(,)𝐵)) =
ℝ ↔ (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵))) |
67 | 61, 65, 66 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ ↔ (ℝ
∖ (𝐵[,)+∞)) =
(-∞(,)𝐵))) |
68 | 59, 67 | mpbid 235 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵)) |
69 | | rembl 24294 |
. . . . . . 7
⊢ ℝ
∈ dom vol |
70 | | xrleloe 12622 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞))) |
71 | 41, 42, 70 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞))) |
72 | 50, 71 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ ∨ 𝐵 = +∞)) |
73 | | xrre2 12648 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < +∞)) → 𝐵 ∈ ℝ) |
74 | 73 | expr 460 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ)) |
75 | 42, 74 | mp3anl3 1458 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ)) |
76 | 75 | orim1d 965 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵 < +∞ ∨ 𝐵 = +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))) |
77 | 72, 76 | mpd 15 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞)) |
78 | | icombl1 24317 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → (𝐵[,)+∞) ∈ dom
vol) |
79 | | oveq1 7179 |
. . . . . . . . . . 11
⊢ (𝐵 = +∞ → (𝐵[,)+∞) =
(+∞[,)+∞)) |
80 | | pnfge 12610 |
. . . . . . . . . . . . 13
⊢ (+∞
∈ ℝ* → +∞ ≤ +∞) |
81 | 42, 80 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ +∞
≤ +∞ |
82 | | ico0 12869 |
. . . . . . . . . . . . 13
⊢
((+∞ ∈ ℝ* ∧ +∞ ∈
ℝ*) → ((+∞[,)+∞) = ∅ ↔ +∞
≤ +∞)) |
83 | 42, 42, 82 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((+∞[,)+∞) = ∅ ↔ +∞ ≤
+∞) |
84 | 81, 83 | mpbir 234 |
. . . . . . . . . . 11
⊢
(+∞[,)+∞) = ∅ |
85 | 79, 84 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (𝐵 = +∞ → (𝐵[,)+∞) =
∅) |
86 | | 0mbl 24293 |
. . . . . . . . . 10
⊢ ∅
∈ dom vol |
87 | 85, 86 | eqeltrdi 2841 |
. . . . . . . . 9
⊢ (𝐵 = +∞ → (𝐵[,)+∞) ∈ dom
vol) |
88 | 78, 87 | jaoi 856 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∨ 𝐵 = +∞) → (𝐵[,)+∞) ∈ dom
vol) |
89 | 77, 88 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ∈ dom
vol) |
90 | | difmbl 24297 |
. . . . . . 7
⊢ ((ℝ
∈ dom vol ∧ (𝐵[,)+∞) ∈ dom vol) → (ℝ
∖ (𝐵[,)+∞))
∈ dom vol) |
91 | 69, 89, 90 | sylancr 590 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) ∈ dom
vol) |
92 | 68, 91 | eqeltrrd 2834 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (-∞(,)𝐵) ∈ dom vol) |
93 | | oveq1 7179 |
. . . . . 6
⊢ (-∞
= 𝐴 →
(-∞(,)𝐵) = (𝐴(,)𝐵)) |
94 | 93 | eleq1d 2817 |
. . . . 5
⊢ (-∞
= 𝐴 →
((-∞(,)𝐵) ∈ dom
vol ↔ (𝐴(,)𝐵) ∈ dom
vol)) |
95 | 92, 94 | syl5ibcom 248 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (-∞ = 𝐴 → (𝐴(,)𝐵) ∈ dom vol)) |
96 | | xrleloe 12622 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) →
(-∞ ≤ 𝐴 ↔
(-∞ < 𝐴 ∨
-∞ = 𝐴))) |
97 | 22, 44, 96 | sylancr 590 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (-∞ ≤ 𝐴 ↔ (-∞ < 𝐴 ∨ -∞ = 𝐴))) |
98 | 46, 97 | mpbid 235 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 ∨ -∞ = 𝐴)) |
99 | 38, 95, 98 | mpjaod 859 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol) |
100 | | ioo0 12848 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
101 | | xrlenlt 10786 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
102 | 101 | ancoms 462 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
103 | 100, 102 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ ¬ 𝐴 < 𝐵)) |
104 | 103 | biimpar 481 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) = ∅) |
105 | 104, 86 | eqeltrdi 2841 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol) |
106 | 99, 105 | pm2.61dan 813 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴(,)𝐵) ∈ dom vol) |
107 | | ndmioo 12850 |
. . 3
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) = ∅) |
108 | 107, 86 | eqeltrdi 2841 |
. 2
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) ∈ dom vol) |
109 | 106, 108 | pm2.61i 185 |
1
⊢ (𝐴(,)𝐵) ∈ dom vol |