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

Theorem ioombl 23731
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 12591 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
213expa 1151 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
32adantrr 708 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
4 lbico1 12516 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
543expa 1151 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
65adantrr 708 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ (𝐴[,)𝐵))
76snssd 4558 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ (𝐴[,)𝐵))
8 iccid 12508 . . . . . . . . . . 11 (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴})
98ad2antrr 717 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,]𝐴) = {𝐴})
109ineq1d 4040 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ({𝐴} ∩ (𝐴(,)𝐵)))
11 simpll 783 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ ℝ*)
12 simplr 785 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐵 ∈ ℝ*)
13 df-icc 12470 . . . . . . . . . . 11 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
14 df-ioo 12467 . . . . . . . . . . 11 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
15 xrltnle 10424 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐴 < 𝑤 ↔ ¬ 𝑤𝐴))
1613, 14, 15ixxdisj 12478 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅)
1711, 11, 12, 16syl3anc 1494 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅)
1810, 17eqtr3d 2863 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∩ (𝐴(,)𝐵)) = ∅)
19 uneqdifeq 4280 . . . . . . . 8 (({𝐴} ⊆ (𝐴[,)𝐵) ∧ ({𝐴} ∩ (𝐴(,)𝐵)) = ∅) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)))
207, 18, 19syl2anc 579 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)))
213, 20mpbid 224 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵))
22 mnfxr 10414 . . . . . . . . . 10 -∞ ∈ ℝ*
2322a1i 11 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ ∈ ℝ*)
24 simprr 789 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ < 𝐴)
25 simprl 787 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 < 𝐵)
26 xrre2 12289 . . . . . . . . 9 (((-∞ ∈ ℝ*𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (-∞ < 𝐴𝐴 < 𝐵)) → 𝐴 ∈ ℝ)
2723, 11, 12, 24, 25, 26syl32anc 1501 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ ℝ)
28 icombl 23730 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol)
2927, 12, 28syl2anc 579 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,)𝐵) ∈ dom vol)
3027snssd 4558 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ ℝ)
31 ovolsn 23661 . . . . . . . . 9 (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0)
3227, 31syl 17 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (vol*‘{𝐴}) = 0)
33 nulmbl 23701 . . . . . . . 8 (({𝐴} ⊆ ℝ ∧ (vol*‘{𝐴}) = 0) → {𝐴} ∈ dom vol)
3430, 32, 33syl2anc 579 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ∈ dom vol)
35 difmbl 23709 . . . . . . 7 (((𝐴[,)𝐵) ∈ dom vol ∧ {𝐴} ∈ dom vol) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol)
3629, 34, 35syl2anc 579 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol)
3721, 36eqeltrrd 2907 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴(,)𝐵) ∈ dom vol)
3837expr 450 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 → (𝐴(,)𝐵) ∈ dom vol))
39 uncom 3984 . . . . . . . . 9 ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ((-∞(,)𝐵) ∪ (𝐵[,)+∞))
4022a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → -∞ ∈ ℝ*)
41 simplr 785 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ*)
42 pnfxr 10410 . . . . . . . . . . 11 +∞ ∈ ℝ*
4342a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → +∞ ∈ ℝ*)
44 simpll 783 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ*)
45 mnfle 12255 . . . . . . . . . . . 12 (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
4645ad2antrr 717 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → -∞ ≤ 𝐴)
47 simpr 479 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
4840, 44, 41, 46, 47xrlelttrd 12279 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → -∞ < 𝐵)
49 pnfge 12250 . . . . . . . . . . 11 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
5041, 49syl 17 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → 𝐵 ≤ +∞)
51 df-ico 12469 . . . . . . . . . . 11 [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
52 xrlenlt 10422 . . . . . . . . . . 11 ((𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐵𝑤 ↔ ¬ 𝑤 < 𝐵))
53 xrltletr 12276 . . . . . . . . . . 11 ((𝑤 ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑤 < 𝐵𝐵 ≤ +∞) → 𝑤 < +∞))
54 xrltletr 12276 . . . . . . . . . . 11 ((-∞ ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → ((-∞ < 𝐵𝐵𝑤) → -∞ < 𝑤))
5514, 51, 52, 14, 53, 54ixxun 12479 . . . . . . . . . 10 (((-∞ ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ < 𝐵𝐵 ≤ +∞)) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) = (-∞(,)+∞))
5640, 41, 43, 48, 50, 55syl32anc 1501 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) = (-∞(,)+∞))
5739, 56syl5eq 2873 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = (-∞(,)+∞))
58 ioomax 12536 . . . . . . . 8 (-∞(,)+∞) = ℝ
5957, 58syl6eq 2877 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ)
60 ssun1 4003 . . . . . . . . 9 (𝐵[,)+∞) ⊆ ((𝐵[,)+∞) ∪ (-∞(,)𝐵))
6160, 59syl5sseq 3878 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ⊆ ℝ)
62 incom 4032 . . . . . . . . 9 ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ((-∞(,)𝐵) ∩ (𝐵[,)+∞))
6314, 51, 52ixxdisj 12478 . . . . . . . . . 10 ((-∞ ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
6440, 41, 43, 63syl3anc 1494 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
6562, 64syl5eq 2873 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ∅)
66 uneqdifeq 4280 . . . . . . . 8 (((𝐵[,)+∞) ⊆ ℝ ∧ ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ∅) → (((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ ↔ (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵)))
6761, 65, 66syl2anc 579 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ ↔ (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵)))
6859, 67mpbid 224 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵))
69 rembl 23706 . . . . . . 7 ℝ ∈ dom vol
70 xrleloe 12263 . . . . . . . . . . 11 ((𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
7141, 42, 70sylancl 580 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
7250, 71mpbid 224 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ ∨ 𝐵 = +∞))
73 xrre2 12289 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝐴 < 𝐵𝐵 < +∞)) → 𝐵 ∈ ℝ)
7473expr 450 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
7542, 74mp3anl3 1585 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
7675orim1d 993 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐵 < +∞ ∨ 𝐵 = +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞)))
7772, 76mpd 15 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
78 icombl1 23729 . . . . . . . . 9 (𝐵 ∈ ℝ → (𝐵[,)+∞) ∈ dom vol)
79 oveq1 6912 . . . . . . . . . . 11 (𝐵 = +∞ → (𝐵[,)+∞) = (+∞[,)+∞))
80 pnfge 12250 . . . . . . . . . . . . 13 (+∞ ∈ ℝ* → +∞ ≤ +∞)
8142, 80ax-mp 5 . . . . . . . . . . . 12 +∞ ≤ +∞
82 ico0 12509 . . . . . . . . . . . . 13 ((+∞ ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞))
8342, 42, 82mp2an 683 . . . . . . . . . . . 12 ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞)
8481, 83mpbir 223 . . . . . . . . . . 11 (+∞[,)+∞) = ∅
8579, 84syl6eq 2877 . . . . . . . . . 10 (𝐵 = +∞ → (𝐵[,)+∞) = ∅)
86 0mbl 23705 . . . . . . . . . 10 ∅ ∈ dom vol
8785, 86syl6eqel 2914 . . . . . . . . 9 (𝐵 = +∞ → (𝐵[,)+∞) ∈ dom vol)
8878, 87jaoi 888 . . . . . . . 8 ((𝐵 ∈ ℝ ∨ 𝐵 = +∞) → (𝐵[,)+∞) ∈ dom vol)
8977, 88syl 17 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ∈ dom vol)
90 difmbl 23709 . . . . . . 7 ((ℝ ∈ dom vol ∧ (𝐵[,)+∞) ∈ dom vol) → (ℝ ∖ (𝐵[,)+∞)) ∈ dom vol)
9169, 89, 90sylancr 581 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) ∈ dom vol)
9268, 91eqeltrrd 2907 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞(,)𝐵) ∈ dom vol)
93 oveq1 6912 . . . . . 6 (-∞ = 𝐴 → (-∞(,)𝐵) = (𝐴(,)𝐵))
9493eleq1d 2891 . . . . 5 (-∞ = 𝐴 → ((-∞(,)𝐵) ∈ dom vol ↔ (𝐴(,)𝐵) ∈ dom vol))
9592, 94syl5ibcom 237 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ = 𝐴 → (𝐴(,)𝐵) ∈ dom vol))
96 xrleloe 12263 . . . . . 6 ((-∞ ∈ ℝ*𝐴 ∈ ℝ*) → (-∞ ≤ 𝐴 ↔ (-∞ < 𝐴 ∨ -∞ = 𝐴)))
9722, 44, 96sylancr 581 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ ≤ 𝐴 ↔ (-∞ < 𝐴 ∨ -∞ = 𝐴)))
9846, 97mpbid 224 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 ∨ -∞ = 𝐴))
9938, 95, 98mpjaod 891 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol)
100 ioo0 12488 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵𝐴))
101 xrlenlt 10422 . . . . . . 7 ((𝐵 ∈ ℝ*𝐴 ∈ ℝ*) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
102101ancoms 452 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
103100, 102bitrd 271 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ ¬ 𝐴 < 𝐵))
104103biimpar 471 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) = ∅)
105104, 86syl6eqel 2914 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol)
10699, 105pm2.61dan 847 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) ∈ dom vol)
107 ndmioo 12490 . . 3 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅)
108107, 86syl6eqel 2914 . 2 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) ∈ dom vol)
109106, 108pm2.61i 177 1 (𝐴(,)𝐵) ∈ dom vol
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 878  w3a 1111   = wceq 1656  wcel 2164  cdif 3795  cun 3796  cin 3797  wss 3798  c0 4144  {csn 4397   class class class wbr 4873  dom cdm 5342  cfv 6123  (class class class)co 6905  cr 10251  0cc0 10252  +∞cpnf 10388  -∞cmnf 10389  *cxr 10390   < clt 10391  cle 10392  (,)cioo 12463  [,)cico 12465  [,]cicc 12466  vol*covol 23628  volcvol 23629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-fal 1670  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-of 7157  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-er 8009  df-map 8124  df-pm 8125  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-sup 8617  df-inf 8618  df-oi 8684  df-card 9078  df-cda 9305  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-n0 11619  df-z 11705  df-uz 11969  df-q 12072  df-rp 12113  df-xadd 12233  df-ioo 12467  df-ico 12469  df-icc 12470  df-fz 12620  df-fzo 12761  df-fl 12888  df-seq 13096  df-exp 13155  df-hash 13411  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-clim 14596  df-rlim 14597  df-sum 14794  df-xmet 20099  df-met 20100  df-ovol 23630  df-vol 23631
This theorem is referenced by:  iccmbl  23732  ovolioo  23734  volioo  23735  ioovolcl  23736  uniioovol  23745  uniioombllem4  23752  uniioombllem5  23753  opnmblALT  23769  mbfid  23801  ditgcl  24021  ditgswap  24022  ditgsplitlem  24023  ftc1lem1  24197  ftc1lem2  24198  ftc1a  24199  ftc1lem4  24201  ftc2  24206  ftc2ditglem  24207  itgsubstlem  24210  ftc2re  31214  fdvposlt  31215  fdvposle  31217  itgexpif  31222  circlemeth  31256  itg2gt0cn  34001  ftc1cnnclem  34019  ftc1anclem7  34027  ftc1anclem8  34028  ftc1anc  34029  ftc2nc  34030  areacirc  34041  iocmbl  38633  cnioobibld  38634  itgpowd  38635  lhe4.4ex1a  39361  itgsin0pilem1  40953  iblioosinexp  40956  itgsinexplem1  40957  itgsinexp  40958  itgcoscmulx  40972  volioc  40975  itgsincmulx  40977  iblcncfioo  40981  itgiccshift  40983  itgperiod  40984  itgsbtaddcnst  40985  volico  40987  volioof  40991  wallispilem2  41070  dirkeritg  41106  fourierdlem16  41127  fourierdlem21  41132  fourierdlem22  41133  fourierdlem39  41150  fourierdlem73  41183  fourierdlem83  41193  fourierdlem103  41213  fourierdlem104  41214  fourierdlem111  41221  fourierdlem112  41222  sqwvfoura  41232  sqwvfourb  41233  etransclem18  41256  etransclem23  41261  ovolval4lem1  41650  ovolval5lem1  41653
  Copyright terms: Public domain W3C validator