MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ioombl Structured version   Visualization version   GIF version

Theorem ioombl 24319
Description: An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
Assertion
Ref Expression
ioombl (𝐴(,)𝐵) ∈ dom vol

Proof of Theorem ioombl
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snunioo 12954 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
213expa 1119 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
32adantrr 717 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
4 lbico1 12877 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
543expa 1119 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
65adantrr 717 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ (𝐴[,)𝐵))
76snssd 4697 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ (𝐴[,)𝐵))
8 iccid 12868 . . . . . . . . . . 11 (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴})
98ad2antrr 726 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,]𝐴) = {𝐴})
109ineq1d 4102 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ({𝐴} ∩ (𝐴(,)𝐵)))
11 simpll 767 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ ℝ*)
12 simplr 769 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐵 ∈ ℝ*)
13 df-icc 12830 . . . . . . . . . . 11 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
14 df-ioo 12827 . . . . . . . . . . 11 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
15 xrltnle 10788 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐴 < 𝑤 ↔ ¬ 𝑤𝐴))
1613, 14, 15ixxdisj 12838 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅)
1711, 11, 12, 16syl3anc 1372 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅)
1810, 17eqtr3d 2775 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∩ (𝐴(,)𝐵)) = ∅)
19 uneqdifeq 4379 . . . . . . . 8 (({𝐴} ⊆ (𝐴[,)𝐵) ∧ ({𝐴} ∩ (𝐴(,)𝐵)) = ∅) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)))
207, 18, 19syl2anc 587 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)))
213, 20mpbid 235 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵))
22 mnfxr 10778 . . . . . . . . . 10 -∞ ∈ ℝ*
2322a1i 11 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ ∈ ℝ*)
24 simprr 773 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ < 𝐴)
25 simprl 771 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 < 𝐵)
26 xrre2 12648 . . . . . . . . 9 (((-∞ ∈ ℝ*𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (-∞ < 𝐴𝐴 < 𝐵)) → 𝐴 ∈ ℝ)
2723, 11, 12, 24, 25, 26syl32anc 1379 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ ℝ)
28 icombl 24318 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol)
2927, 12, 28syl2anc 587 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,)𝐵) ∈ dom vol)
3027snssd 4697 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ ℝ)
31 ovolsn 24249 . . . . . . . . 9 (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0)
3227, 31syl 17 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (vol*‘{𝐴}) = 0)
33 nulmbl 24289 . . . . . . . 8 (({𝐴} ⊆ ℝ ∧ (vol*‘{𝐴}) = 0) → {𝐴} ∈ dom vol)
3430, 32, 33syl2anc 587 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ∈ dom vol)
35 difmbl 24297 . . . . . . 7 (((𝐴[,)𝐵) ∈ dom vol ∧ {𝐴} ∈ dom vol) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol)
3629, 34, 35syl2anc 587 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol)
3721, 36eqeltrrd 2834 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴(,)𝐵) ∈ dom vol)
3837expr 460 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 → (𝐴(,)𝐵) ∈ dom vol))
39 uncom 4043 . . . . . . . . 9 ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ((-∞(,)𝐵) ∪ (𝐵[,)+∞))
4022a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → -∞ ∈ ℝ*)
41 simplr 769 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ*)
42 pnfxr 10775 . . . . . . . . . . 11 +∞ ∈ ℝ*
4342a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → +∞ ∈ ℝ*)
44 simpll 767 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ*)
45 mnfle 12614 . . . . . . . . . . . 12 (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
4645ad2antrr 726 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → -∞ ≤ 𝐴)
47 simpr 488 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
4840, 44, 41, 46, 47xrlelttrd 12638 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → -∞ < 𝐵)
49 pnfge 12610 . . . . . . . . . . 11 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
5041, 49syl 17 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐵 ≤ +∞)
51 df-ico 12829 . . . . . . . . . . 11 [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
52 xrlenlt 10786 . . . . . . . . . . 11 ((𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐵𝑤 ↔ ¬ 𝑤 < 𝐵))
53 xrltletr 12635 . . . . . . . . . . 11 ((𝑤 ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑤 < 𝐵𝐵 ≤ +∞) → 𝑤 < +∞))
54 xrltletr 12635 . . . . . . . . . . 11 ((-∞ ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → ((-∞ < 𝐵𝐵𝑤) → -∞ < 𝑤))
5514, 51, 52, 14, 53, 54ixxun 12839 . . . . . . . . . 10 (((-∞ ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ < 𝐵𝐵 ≤ +∞)) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) = (-∞(,)+∞))
5640, 41, 43, 48, 50, 55syl32anc 1379 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) = (-∞(,)+∞))
5739, 56syl5eq 2785 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = (-∞(,)+∞))
58 ioomax 12898 . . . . . . . 8 (-∞(,)+∞) = ℝ
5957, 58eqtrdi 2789 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ)
60 ssun1 4062 . . . . . . . . 9 (𝐵[,)+∞) ⊆ ((𝐵[,)+∞) ∪ (-∞(,)𝐵))
6160, 59sseqtrid 3929 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ⊆ ℝ)
62 incom 4091 . . . . . . . . 9 ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ((-∞(,)𝐵) ∩ (𝐵[,)+∞))
6314, 51, 52ixxdisj 12838 . . . . . . . . . 10 ((-∞ ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
6440, 41, 43, 63syl3anc 1372 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
6562, 64syl5eq 2785 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ∅)
66 uneqdifeq 4379 . . . . . . . 8 (((𝐵[,)+∞) ⊆ ℝ ∧ ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ∅) → (((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ ↔ (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵)))
6761, 65, 66syl2anc 587 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ ↔ (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵)))
6859, 67mpbid 235 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵))
69 rembl 24294 . . . . . . 7 ℝ ∈ dom vol
70 xrleloe 12622 . . . . . . . . . . 11 ((𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
7141, 42, 70sylancl 589 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
7250, 71mpbid 235 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ ∨ 𝐵 = +∞))
73 xrre2 12648 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝐴 < 𝐵𝐵 < +∞)) → 𝐵 ∈ ℝ)
7473expr 460 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
7542, 74mp3anl3 1458 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
7675orim1d 965 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵 < +∞ ∨ 𝐵 = +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞)))
7772, 76mpd 15 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
78 icombl1 24317 . . . . . . . . 9 (𝐵 ∈ ℝ → (𝐵[,)+∞) ∈ dom vol)
79 oveq1 7179 . . . . . . . . . . 11 (𝐵 = +∞ → (𝐵[,)+∞) = (+∞[,)+∞))
80 pnfge 12610 . . . . . . . . . . . . 13 (+∞ ∈ ℝ* → +∞ ≤ +∞)
8142, 80ax-mp 5 . . . . . . . . . . . 12 +∞ ≤ +∞
82 ico0 12869 . . . . . . . . . . . . 13 ((+∞ ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞))
8342, 42, 82mp2an 692 . . . . . . . . . . . 12 ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞)
8481, 83mpbir 234 . . . . . . . . . . 11 (+∞[,)+∞) = ∅
8579, 84eqtrdi 2789 . . . . . . . . . 10 (𝐵 = +∞ → (𝐵[,)+∞) = ∅)
86 0mbl 24293 . . . . . . . . . 10 ∅ ∈ dom vol
8785, 86eqeltrdi 2841 . . . . . . . . 9 (𝐵 = +∞ → (𝐵[,)+∞) ∈ dom vol)
8878, 87jaoi 856 . . . . . . . 8 ((𝐵 ∈ ℝ ∨ 𝐵 = +∞) → (𝐵[,)+∞) ∈ dom vol)
8977, 88syl 17 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ∈ dom vol)
90 difmbl 24297 . . . . . . 7 ((ℝ ∈ dom vol ∧ (𝐵[,)+∞) ∈ dom vol) → (ℝ ∖ (𝐵[,)+∞)) ∈ dom vol)
9169, 89, 90sylancr 590 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) ∈ dom vol)
9268, 91eqeltrrd 2834 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞(,)𝐵) ∈ dom vol)
93 oveq1 7179 . . . . . 6 (-∞ = 𝐴 → (-∞(,)𝐵) = (𝐴(,)𝐵))
9493eleq1d 2817 . . . . 5 (-∞ = 𝐴 → ((-∞(,)𝐵) ∈ dom vol ↔ (𝐴(,)𝐵) ∈ dom vol))
9592, 94syl5ibcom 248 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ = 𝐴 → (𝐴(,)𝐵) ∈ dom vol))
96 xrleloe 12622 . . . . . 6 ((-∞ ∈ ℝ*𝐴 ∈ ℝ*) → (-∞ ≤ 𝐴 ↔ (-∞ < 𝐴 ∨ -∞ = 𝐴)))
9722, 44, 96sylancr 590 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ ≤ 𝐴 ↔ (-∞ < 𝐴 ∨ -∞ = 𝐴)))
9846, 97mpbid 235 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 ∨ -∞ = 𝐴))
9938, 95, 98mpjaod 859 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol)
100 ioo0 12848 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵𝐴))
101 xrlenlt 10786 . . . . . . 7 ((𝐵 ∈ ℝ*𝐴 ∈ ℝ*) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
102101ancoms 462 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
103100, 102bitrd 282 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ ¬ 𝐴 < 𝐵))
104103biimpar 481 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) = ∅)
105104, 86eqeltrdi 2841 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol)
10699, 105pm2.61dan 813 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) ∈ dom vol)
107 ndmioo 12850 . . 3 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅)
108107, 86eqeltrdi 2841 . 2 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) ∈ dom vol)
109106, 108pm2.61i 185 1 (𝐴(,)𝐵) ∈ dom vol
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  w3a 1088   = wceq 1542  wcel 2114  cdif 3840  cun 3841  cin 3842  wss 3843  c0 4211  {csn 4516   class class class wbr 5030  dom cdm 5525  cfv 6339  (class class class)co 7172  cr 10616  0cc0 10617  +∞cpnf 10752  -∞cmnf 10753  *cxr 10754   < clt 10755  cle 10756  (,)cioo 12823  [,)cico 12825  [,]cicc 12826  vol*covol 24216  volcvol 24217
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7481  ax-inf2 9179  ax-cnex 10673  ax-resscn 10674  ax-1cn 10675  ax-icn 10676  ax-addcl 10677  ax-addrcl 10678  ax-mulcl 10679  ax-mulrcl 10680  ax-mulcom 10681  ax-addass 10682  ax-mulass 10683  ax-distr 10684  ax-i2m1 10685  ax-1ne0 10686  ax-1rid 10687  ax-rnegex 10688  ax-rrecex 10689  ax-cnre 10690  ax-pre-lttri 10691  ax-pre-lttrn 10692  ax-pre-ltadd 10693  ax-pre-mulgt0 10694  ax-pre-sup 10695
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7129  df-ov 7175  df-oprab 7176  df-mpo 7177  df-of 7427  df-om 7602  df-1st 7716  df-2nd 7717  df-wrecs 7978  df-recs 8039  df-rdg 8077  df-1o 8133  df-2o 8134  df-er 8322  df-map 8441  df-pm 8442  df-en 8558  df-dom 8559  df-sdom 8560  df-fin 8561  df-sup 8981  df-inf 8982  df-oi 9049  df-dju 9405  df-card 9443  df-pnf 10757  df-mnf 10758  df-xr 10759  df-ltxr 10760  df-le 10761  df-sub 10952  df-neg 10953  df-div 11378  df-nn 11719  df-2 11781  df-3 11782  df-n0 11979  df-z 12065  df-uz 12327  df-q 12433  df-rp 12475  df-xadd 12593  df-ioo 12827  df-ico 12829  df-icc 12830  df-fz 12984  df-fzo 13127  df-fl 13255  df-seq 13463  df-exp 13524  df-hash 13785  df-cj 14550  df-re 14551  df-im 14552  df-sqrt 14686  df-abs 14687  df-clim 14937  df-rlim 14938  df-sum 15138  df-xmet 20212  df-met 20213  df-ovol 24218  df-vol 24219
This theorem is referenced by:  iccmbl  24320  ovolioo  24322  volioo  24323  ioovolcl  24324  uniioovol  24333  uniioombllem4  24340  uniioombllem5  24341  opnmblALT  24357  mbfid  24389  ditgcl  24612  ditgswap  24613  ditgsplitlem  24614  ftc1lem1  24789  ftc1lem2  24790  ftc1a  24791  ftc1lem4  24793  ftc2  24798  ftc2ditglem  24799  itgsubstlem  24802  itgpowd  24804  ftc2re  32150  fdvposlt  32151  fdvposle  32153  itgexpif  32158  circlemeth  32192  itg2gt0cn  35477  ftc1cnnclem  35493  ftc1anclem7  35501  ftc1anclem8  35502  ftc1anc  35503  ftc2nc  35504  areacirc  35515  lcmineqlem10  39688  lcmineqlem12  39690  iocmbl  40638  cnioobibld  40639  lhe4.4ex1a  41507  itgsin0pilem1  43055  iblioosinexp  43058  itgsinexplem1  43059  itgsinexp  43060  itgcoscmulx  43074  volioc  43077  itgsincmulx  43079  iblcncfioo  43083  itgiccshift  43085  itgperiod  43086  itgsbtaddcnst  43087  volico  43088  volioof  43092  wallispilem2  43171  dirkeritg  43207  fourierdlem16  43228  fourierdlem21  43233  fourierdlem22  43234  fourierdlem39  43251  fourierdlem73  43284  fourierdlem83  43294  fourierdlem103  43314  fourierdlem104  43315  fourierdlem111  43322  fourierdlem112  43323  sqwvfoura  43333  sqwvfourb  43334  etransclem18  43357  etransclem23  43362  ovolval4lem1  43751  ovolval5lem1  43754
  Copyright terms: Public domain W3C validator