# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\to \left[{A},{B}\right)\in \mathrm{dom}vol$

### Proof

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