Metamath Proof Explorer


Theorem icombl

Description: A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion icombl A B * A B dom vol

Proof

Step Hyp Ref Expression
1 uncom B +∞ A B = A B B +∞
2 rexr A A *
3 2 ad2antrr A B * A < B A *
4 simplr A B * A < B B *
5 pnfxr +∞ *
6 5 a1i A B * A < B +∞ *
7 xrltle A * B * A < B A B
8 2 7 sylan A B * A < B A B
9 8 imp A B * A < B A B
10 pnfge B * B +∞
11 4 10 syl A B * A < B B +∞
12 icoun A * B * +∞ * A B B +∞ A B B +∞ = A +∞
13 3 4 6 9 11 12 syl32anc A B * A < B A B B +∞ = A +∞
14 1 13 syl5eq A B * A < B B +∞ A B = A +∞
15 ssun1 B +∞ B +∞ A B
16 15 14 sseqtrid A B * A < B B +∞ A +∞
17 incom B +∞ A B = A B B +∞
18 icodisj A * B * +∞ * A B B +∞ =
19 5 18 mp3an3 A * B * A B B +∞ =
20 3 4 19 syl2anc A B * A < B A B B +∞ =
21 17 20 syl5eq A B * A < B B +∞ A B =
22 uneqdifeq B +∞ A +∞ B +∞ A B = B +∞ A B = A +∞ A +∞ B +∞ = A B
23 16 21 22 syl2anc A B * A < B B +∞ A B = A +∞ A +∞ B +∞ = A B
24 14 23 mpbid A B * A < B A +∞ B +∞ = A B
25 icombl1 A A +∞ dom vol
26 25 ad2antrr A B * A < B A +∞ dom vol
27 xrleloe B * +∞ * B +∞ B < +∞ B = +∞
28 4 6 27 syl2anc A B * A < B B +∞ B < +∞ B = +∞
29 11 28 mpbid A B * A < B B < +∞ B = +∞
30 simpr A B * A < B A < B
31 xrre2 A * B * +∞ * A < B B < +∞ B
32 31 expr A * B * +∞ * A < B B < +∞ B
33 3 4 6 30 32 syl31anc A B * A < B B < +∞ B
34 33 orim1d A B * A < B B < +∞ B = +∞ B B = +∞
35 29 34 mpd A B * A < B B B = +∞
36 icombl1 B B +∞ dom vol
37 oveq1 B = +∞ B +∞ = +∞ +∞
38 pnfge +∞ * +∞ +∞
39 5 38 ax-mp +∞ +∞
40 ico0 +∞ * +∞ * +∞ +∞ = +∞ +∞
41 5 5 40 mp2an +∞ +∞ = +∞ +∞
42 39 41 mpbir +∞ +∞ =
43 37 42 syl6eq B = +∞ B +∞ =
44 0mbl dom vol
45 43 44 eqeltrdi B = +∞ B +∞ dom vol
46 36 45 jaoi B B = +∞ B +∞ dom vol
47 35 46 syl A B * A < B B +∞ dom vol
48 difmbl A +∞ dom vol B +∞ dom vol A +∞ B +∞ dom vol
49 26 47 48 syl2anc A B * A < B A +∞ B +∞ dom vol
50 24 49 eqeltrrd A B * A < B A B dom vol
51 ico0 A * B * A B = B A
52 2 51 sylan A B * A B = B A
53 simpr A B * B *
54 2 adantr A B * A *
55 53 54 xrlenltd A B * B A ¬ A < B
56 52 55 bitrd A B * A B = ¬ A < B
57 56 biimpar A B * ¬ A < B A B =
58 57 44 eqeltrdi A B * ¬ A < B A B dom vol
59 50 58 pm2.61dan A B * A B dom vol