ioombl - Metamath Proof Explorer

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

Theorem ioombl 25607

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.

Step	Hyp	Ref	Expression
1		snunioo 13479	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
2	1	3expa 1130	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
3	2	adantrr 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
4		lbico1 13401	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
5	4	3expa 1130	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
6	5	adantrr 727	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ (𝐴[,)𝐵))
7	6	snssd 4744	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ (𝐴[,)𝐵))
8		iccid 13391	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ^* → (𝐴[,]𝐴) = {𝐴})
9	8	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,]𝐴) = {𝐴})
10	9	ineq1d 4171	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ({𝐴} ∩ (𝐴(,)𝐵)))
11		simpll 776	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ ℝ^)
12		simplr 778	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐵 ∈ ℝ^)
13		df-icc 13353	. . . . . . . . . . 11 ⊢ [,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
14		df-ioo 13350	. . . . . . . . . . 11 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15		xrltnle 11246	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴 < 𝑤 ↔ ¬ 𝑤 ≤ 𝐴))
16	13, 14, 15	ixxdisj 13361	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅)
17	11, 11, 12, 16	syl3anc 1389	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,]𝐴) ∩ (𝐴(,)𝐵)) = ∅)
18	10, 17	eqtr3d 2798	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ({𝐴} ∩ (𝐴(,)𝐵)) = ∅)
19		uneqdifeq 4445	. . . . . . . 8 ⊢ (({𝐴} ⊆ (𝐴[,)𝐵) ∧ ({𝐴} ∩ (𝐴(,)𝐵)) = ∅) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)))
20	7, 18, 19	syl2anc 593	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵) ↔ ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)))
21	3, 20	mpbid 234	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵))
22		mnfxr 11236	. . . . . . . . . 10 ⊢ -∞ ∈ ℝ^*
23	22	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ ∈ ℝ^)
24		simprr 782	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → -∞ < 𝐴)
25		simprl 780	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 < 𝐵)
26		xrre2 13170	. . . . . . . . 9 ⊢ (((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (-∞ < 𝐴 ∧ 𝐴 < 𝐵)) → 𝐴 ∈ ℝ)
27	23, 11, 12, 24, 25, 26	syl32anc 1396	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → 𝐴 ∈ ℝ)
28		icombl 25606	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴[,)𝐵) ∈ dom vol)
29	27, 12, 28	syl2anc 593	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴[,)𝐵) ∈ dom vol)
30	27	snssd 4744	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ⊆ ℝ)
31		ovolsn 25537	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0)
32	27, 31	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (vol‘{𝐴}) = 0)
33		nulmbl 25577	. . . . . . . 8 ⊢ (({𝐴} ⊆ ℝ ∧ (vol*‘{𝐴}) = 0) → {𝐴} ∈ dom vol)
34	30, 32, 33	syl2anc 593	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → {𝐴} ∈ dom vol)
35		difmbl 25585	. . . . . . 7 ⊢ (((𝐴[,)𝐵) ∈ dom vol ∧ {𝐴} ∈ dom vol) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol)
36	29, 34, 35	syl2anc 593	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → ((𝐴[,)𝐵) ∖ {𝐴}) ∈ dom vol)
37	21, 36	eqeltrrd 2862	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ -∞ < 𝐴)) → (𝐴(,)𝐵) ∈ dom vol)
38	37	expr 460	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 → (𝐴(,)𝐵) ∈ dom vol))
39		uncom 4111	. . . . . . . . 9 ⊢ ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ((-∞(,)𝐵) ∪ (𝐵[,)+∞))
40	22	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 < 𝐵) → -∞ ∈ ℝ^)
41		simplr 778	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ^)
42		pnfxr 11233	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ^*
43	42	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 < 𝐵) → +∞ ∈ ℝ^)
44		simpll 776	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ^)
45		mnfle 13134	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
46	45	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → -∞ ≤ 𝐴)
47		simpr 488	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
48	40, 44, 41, 46, 47	xrlelttrd 13159	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → -∞ < 𝐵)
49		pnfge 13129	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ +∞)
50	41, 49	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → 𝐵 ≤ +∞)
51		df-ico 13352	. . . . . . . . . . 11 ⊢ [,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
52		xrlenlt 11244	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐵 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐵))
53		xrltletr 13156	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝑤 < 𝐵 ∧ 𝐵 ≤ +∞) → 𝑤 < +∞))
54		xrltletr 13156	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → ((-∞ < 𝐵 ∧ 𝐵 ≤ 𝑤) → -∞ < 𝑤))
55	14, 51, 52, 14, 53, 54	ixxun 13362	. . . . . . . . . 10 ⊢ (((-∞ ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ < 𝐵 ∧ 𝐵 ≤ +∞)) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) = (-∞(,)+∞))
56	40, 41, 43, 48, 50, 55	syl32anc 1396	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∪ (𝐵[,)+∞)) = (-∞(,)+∞))
57	39, 56	eqtrid 2808	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = (-∞(,)+∞))
58		ioomax 13423	. . . . . . . 8 ⊢ (-∞(,)+∞) = ℝ
59	57, 58	eqtrdi 2812	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ)
60		ssun1 4130	. . . . . . . . 9 ⊢ (𝐵[,)+∞) ⊆ ((𝐵[,)+∞) ∪ (-∞(,)𝐵))
61	60, 59	sseqtrid 3978	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ⊆ ℝ)
62		incom 4161	. . . . . . . . 9 ⊢ ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ((-∞(,)𝐵) ∩ (𝐵[,)+∞))
63	14, 51, 52	ixxdisj 13361	. . . . . . . . . 10 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
64	40, 41, 43, 63	syl3anc 1389	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((-∞(,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
65	62, 64	eqtrid 2808	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ∅)
66		uneqdifeq 4445	. . . . . . . 8 ⊢ (((𝐵[,)+∞) ⊆ ℝ ∧ ((𝐵[,)+∞) ∩ (-∞(,)𝐵)) = ∅) → (((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ ↔ (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵)))
67	61, 65, 66	syl2anc 593	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (((𝐵[,)+∞) ∪ (-∞(,)𝐵)) = ℝ ↔ (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵)))
68	59, 67	mpbid 234	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) = (-∞(,)𝐵))
69		rembl 25582	. . . . . . 7 ⊢ ℝ ∈ dom vol
70		xrleloe 13143	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
71	41, 42, 70	sylancl 595	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
72	50, 71	mpbid 234	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ ∨ 𝐵 = +∞))
73		xrre2 13170	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < +∞)) → 𝐵 ∈ ℝ)
74	73	expr 460	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
75	42, 74	mp3anl3 1477	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
76	75	orim1d 978	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐵 < +∞ ∨ 𝐵 = +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞)))
77	72, 76	mpd 15	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
78		icombl1 25605	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ → (𝐵[,)+∞) ∈ dom vol)
79		oveq1 7399	. . . . . . . . . . 11 ⊢ (𝐵 = +∞ → (𝐵[,)+∞) = (+∞[,)+∞))
80		pnfge 13129	. . . . . . . . . . . . 13 ⊢ (+∞ ∈ ℝ^* → +∞ ≤ +∞)
81	42, 80	ax-mp 5	. . . . . . . . . . . 12 ⊢ +∞ ≤ +∞
82		ico0 13392	. . . . . . . . . . . . 13 ⊢ ((+∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞))
83	42, 42, 82	mp2an 702	. . . . . . . . . . . 12 ⊢ ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞)
84	81, 83	mpbir 233	. . . . . . . . . . 11 ⊢ (+∞[,)+∞) = ∅
85	79, 84	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝐵 = +∞ → (𝐵[,)+∞) = ∅)
86		0mbl 25581	. . . . . . . . . 10 ⊢ ∅ ∈ dom vol
87	85, 86	eqeltrdi 2869	. . . . . . . . 9 ⊢ (𝐵 = +∞ → (𝐵[,)+∞) ∈ dom vol)
88	78, 87	jaoi 868	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∨ 𝐵 = +∞) → (𝐵[,)+∞) ∈ dom vol)
89	77, 88	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ∈ dom vol)
90		difmbl 25585	. . . . . . 7 ⊢ ((ℝ ∈ dom vol ∧ (𝐵[,)+∞) ∈ dom vol) → (ℝ ∖ (𝐵[,)+∞)) ∈ dom vol)
91	69, 89, 90	sylancr 596	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (ℝ ∖ (𝐵[,)+∞)) ∈ dom vol)
92	68, 91	eqeltrrd 2862	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (-∞(,)𝐵) ∈ dom vol)
93		oveq1 7399	. . . . . 6 ⊢ (-∞ = 𝐴 → (-∞(,)𝐵) = (𝐴(,)𝐵))
94	93	eleq1d 2846	. . . . 5 ⊢ (-∞ = 𝐴 → ((-∞(,)𝐵) ∈ dom vol ↔ (𝐴(,)𝐵) ∈ dom vol))
95	92, 94	syl5ibcom 247	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (-∞ = 𝐴 → (𝐴(,)𝐵) ∈ dom vol))
96		xrleloe 13143	. . . . . 6 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (-∞ ≤ 𝐴 ↔ (-∞ < 𝐴 ∨ -∞ = 𝐴)))
97	22, 44, 96	sylancr 596	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (-∞ ≤ 𝐴 ↔ (-∞ < 𝐴 ∨ -∞ = 𝐴)))
98	46, 97	mpbid 234	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (-∞ < 𝐴 ∨ -∞ = 𝐴))
99	38, 95, 98	mpjaod 871	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol)
100		ioo0 13371	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴))
101		xrlenlt 11244	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
102	101	ancoms 462	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
103	100, 102	bitrd 281	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴(,)𝐵) = ∅ ↔ ¬ 𝐴 < 𝐵))
104	103	biimpar 481	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) = ∅)
105	104, 86	eqeltrdi 2869	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol)
106	99, 105	pm2.61dan 822	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) ∈ dom vol)
107		ndmioo 13373	. . 3 ⊢ (¬ (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = ∅)
108	107, 86	eqeltrdi 2869	. 2 ⊢ (¬ (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) ∈ dom vol)
109	106, 108	pm2.61i 183	1 ⊢ (𝐴(,)𝐵) ∈ dom vol

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 {csn 4581 class class class wbr 5099 dom cdm 5645 ‘cfv 6517 (class class class)co 7392 ℝcr 11069 0cc0 11070 +∞cpnf 11210 -∞cmnf 11211 ℝ^*cxr 11212 < clt 11213 ≤ cle 11214 (,)cioo 13346 [,)cico 13348 [,]cicc 13349 vol*covol 25504 volcvol 25505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-inf2 9593 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147 ax-pre-sup 11148

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-isom 6526 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-of 7656 df-om 7843 df-1st 7966 df-2nd 7967 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-2o 8433 df-er 8673 df-map 8805 df-pm 8806 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-sup 9385 df-inf 9386 df-oi 9455 df-dju 9856 df-card 9894 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-2 12277 df-3 12278 df-n0 12479 df-z 12566 df-uz 12837 df-q 12947 df-rp 12991 df-xadd 13112 df-ioo 13350 df-ico 13352 df-icc 13353 df-fz 13510 df-fzo 13657 df-fl 13799 df-seq 14012 df-exp 14072 df-hash 14341 df-cj 15109 df-re 15110 df-im 15111 df-sqrt 15245 df-abs 15246 df-clim 15498 df-rlim 15499 df-sum 15697 df-xmet 21397 df-met 21398 df-ovol 25506 df-vol 25507

This theorem is referenced by: iccmbl 25608 ovolioo 25610 volioo 25611 ioovolcl 25612 uniioovol 25621 uniioombllem4 25628 uniioombllem5 25629 opnmblALT 25645 mbfid 25677 ditgcl 25900 ditgswap 25901 ditgsplitlem 25902 ftc1lem1 26077 ftc1lem2 26078 ftc1a 26079 ftc1lem4 26081 ftc2 26086 ftc2ditglem 26087 itgsubstlem 26090 itgpowd 26092 ftc2re 34856 fdvposlt 34857 fdvposle 34859 itgexpif 34864 circlemeth 34898 itg2gt0cn 38138 ftc1cnnclem 38154 ftc1anclem7 38162 ftc1anclem8 38163 ftc1anc 38164 ftc2nc 38165 areacirc 38176 lcmineqlem10 42619 lcmineqlem12 42621 iocmbl 43754 cnioobibld 43755 lhe4.4ex1a 44869 itgsin0pilem1 46488 iblioosinexp 46491 itgsinexplem1 46492 itgsinexp 46493 itgcoscmulx 46507 volioc 46510 itgsincmulx 46512 iblcncfioo 46516 itgiccshift 46518 itgperiod 46519 itgsbtaddcnst 46520 volico 46521 volioof 46525 wallispilem2 46604 dirkeritg 46640 fourierdlem16 46661 fourierdlem21 46666 fourierdlem22 46667 fourierdlem39 46684 fourierdlem73 46717 fourierdlem83 46727 fourierdlem103 46747 fourierdlem104 46748 fourierdlem111 46755 fourierdlem112 46756 sqwvfoura 46766 sqwvfourb 46767 etransclem18 46790 etransclem23 46795 ovolval4lem1 47187 ovolval5lem1 47190

W3C validator