icombl

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

		Ref	Expression
	Assertion	icombl	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \in dom vol$

Proof

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

Metamath Proof Explorer

Theorem icombl

Proof