Metamath Proof Explorer


Theorem ioombl

Description: An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion ioombl A B dom vol

Proof

Step Hyp Ref Expression
1 snunioo A * B * A < B A A B = A B
2 1 3expa A * B * A < B A A B = A B
3 2 adantrr A * B * A < B −∞ < A A A B = A B
4 lbico1 A * B * A < B A A B
5 4 3expa A * B * A < B A A B
6 5 adantrr A * B * A < B −∞ < A A A B
7 6 snssd A * B * A < B −∞ < A A A B
8 iccid A * A A = A
9 8 ad2antrr A * B * A < B −∞ < A A A = A
10 9 ineq1d A * B * A < B −∞ < A A A A B = A A B
11 simpll A * B * A < B −∞ < A A *
12 simplr A * B * A < B −∞ < A B *
13 df-icc . = x * , y * z * | x z z y
14 df-ioo . = x * , y * z * | x < z z < y
15 xrltnle A * w * A < w ¬ w A
16 13 14 15 ixxdisj A * A * B * A A A B =
17 11 11 12 16 syl3anc A * B * A < B −∞ < A A A A B =
18 10 17 eqtr3d A * B * A < B −∞ < A A A B =
19 uneqdifeq A A B A A B = A A B = A B A B A = A B
20 7 18 19 syl2anc A * B * A < B −∞ < A A A B = A B A B A = A B
21 3 20 mpbid A * B * A < B −∞ < A A B A = A B
22 mnfxr −∞ *
23 22 a1i A * B * A < B −∞ < A −∞ *
24 simprr A * B * A < B −∞ < A −∞ < A
25 simprl A * B * A < B −∞ < A A < B
26 xrre2 −∞ * A * B * −∞ < A A < B A
27 23 11 12 24 25 26 syl32anc A * B * A < B −∞ < A A
28 icombl A B * A B dom vol
29 27 12 28 syl2anc A * B * A < B −∞ < A A B dom vol
30 27 snssd A * B * A < B −∞ < A A
31 ovolsn A vol * A = 0
32 27 31 syl A * B * A < B −∞ < A vol * A = 0
33 nulmbl A vol * A = 0 A dom vol
34 30 32 33 syl2anc A * B * A < B −∞ < A A dom vol
35 difmbl A B dom vol A dom vol A B A dom vol
36 29 34 35 syl2anc A * B * A < B −∞ < A A B A dom vol
37 21 36 eqeltrrd A * B * A < B −∞ < A A B dom vol
38 37 expr A * B * A < B −∞ < A A B dom vol
39 uncom B +∞ −∞ B = −∞ B B +∞
40 22 a1i A * B * A < B −∞ *
41 simplr A * B * A < B B *
42 pnfxr +∞ *
43 42 a1i A * B * A < B +∞ *
44 simpll A * B * A < B A *
45 mnfle A * −∞ A
46 45 ad2antrr A * B * A < B −∞ A
47 simpr A * B * A < B A < B
48 40 44 41 46 47 xrlelttrd A * B * A < B −∞ < B
49 pnfge B * B +∞
50 41 49 syl A * B * A < B B +∞
51 df-ico . = x * , y * z * | x z z < y
52 xrlenlt B * w * B w ¬ w < B
53 xrltletr w * B * +∞ * w < B B +∞ w < +∞
54 xrltletr −∞ * B * w * −∞ < B B w −∞ < w
55 14 51 52 14 53 54 ixxun −∞ * B * +∞ * −∞ < B B +∞ −∞ B B +∞ = −∞ +∞
56 40 41 43 48 50 55 syl32anc A * B * A < B −∞ B B +∞ = −∞ +∞
57 39 56 syl5eq A * B * A < B B +∞ −∞ B = −∞ +∞
58 ioomax −∞ +∞ =
59 57 58 syl6eq A * B * A < B B +∞ −∞ B =
60 ssun1 B +∞ B +∞ −∞ B
61 60 59 sseqtrid A * B * A < B B +∞
62 incom B +∞ −∞ B = −∞ B B +∞
63 14 51 52 ixxdisj −∞ * B * +∞ * −∞ B B +∞ =
64 40 41 43 63 syl3anc A * B * A < B −∞ B B +∞ =
65 62 64 syl5eq A * B * A < B B +∞ −∞ B =
66 uneqdifeq B +∞ B +∞ −∞ B = B +∞ −∞ B = B +∞ = −∞ B
67 61 65 66 syl2anc A * B * A < B B +∞ −∞ B = B +∞ = −∞ B
68 59 67 mpbid A * B * A < B B +∞ = −∞ B
69 rembl dom vol
70 xrleloe B * +∞ * B +∞ B < +∞ B = +∞
71 41 42 70 sylancl A * B * A < B B +∞ B < +∞ B = +∞
72 50 71 mpbid A * B * A < B B < +∞ B = +∞
73 xrre2 A * B * +∞ * A < B B < +∞ B
74 73 expr A * B * +∞ * A < B B < +∞ B
75 42 74 mp3anl3 A * B * A < B B < +∞ B
76 75 orim1d A * B * A < B B < +∞ B = +∞ B B = +∞
77 72 76 mpd A * B * A < B B B = +∞
78 icombl1 B B +∞ dom vol
79 oveq1 B = +∞ B +∞ = +∞ +∞
80 pnfge +∞ * +∞ +∞
81 42 80 ax-mp +∞ +∞
82 ico0 +∞ * +∞ * +∞ +∞ = +∞ +∞
83 42 42 82 mp2an +∞ +∞ = +∞ +∞
84 81 83 mpbir +∞ +∞ =
85 79 84 syl6eq B = +∞ B +∞ =
86 0mbl dom vol
87 85 86 eqeltrdi B = +∞ B +∞ dom vol
88 78 87 jaoi B B = +∞ B +∞ dom vol
89 77 88 syl A * B * A < B B +∞ dom vol
90 difmbl dom vol B +∞ dom vol B +∞ dom vol
91 69 89 90 sylancr A * B * A < B B +∞ dom vol
92 68 91 eqeltrrd A * B * A < B −∞ B dom vol
93 oveq1 −∞ = A −∞ B = A B
94 93 eleq1d −∞ = A −∞ B dom vol A B dom vol
95 92 94 syl5ibcom A * B * A < B −∞ = A A B dom vol
96 xrleloe −∞ * A * −∞ A −∞ < A −∞ = A
97 22 44 96 sylancr A * B * A < B −∞ A −∞ < A −∞ = A
98 46 97 mpbid A * B * A < B −∞ < A −∞ = A
99 38 95 98 mpjaod A * B * A < B A B dom vol
100 ioo0 A * B * A B = B A
101 xrlenlt B * A * B A ¬ A < B
102 101 ancoms A * B * B A ¬ A < B
103 100 102 bitrd A * B * A B = ¬ A < B
104 103 biimpar A * B * ¬ A < B A B =
105 104 86 eqeltrdi A * B * ¬ A < B A B dom vol
106 99 105 pm2.61dan A * B * A B dom vol
107 ndmioo ¬ A * B * A B =
108 107 86 eqeltrdi ¬ A * B * A B dom vol
109 106 108 pm2.61i A B dom vol