ovolioo

Description: The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014)

		Ref	Expression
	Assertion	ovolioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ((A, B)) = B - A$

Proof

Step	Hyp	Ref	Expression
1		ioombl	$⊢ (A, B) \in dom vol$
2		mblvol	$⊢ (A, B) \in dom vol \to vol ((A, B)) = {vol}^{*} ((A, B))$
3	1 2	ax-mp	$⊢ vol ((A, B)) = {vol}^{*} ((A, B))$
4		iccmbl	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in dom vol$
5		mblvol	$⊢ [A, B] \in dom vol \to vol ([A, B]) = {vol}^{*} ([A, B])$
6	4 5	syl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B]) = {vol}^{*} ([A, B])$
7	6	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ([A, B]) = {vol}^{*} ([A, B])$
8	1	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to (A, B) \in dom vol$
9		prssi	$⊢ (A \in ℝ \land B \in ℝ) \to \{A, B\} \subseteq ℝ$
10	9	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \{A, B\} \subseteq ℝ$
11		prfi	$⊢ \{A, B\} \in Fin$
12		ovolfi	$⊢ (\{A, B\} \in Fin \land \{A, B\} \subseteq ℝ) \to {vol}^{*} (\{A, B\}) = 0$
13	11 10 12	sylancr	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} (\{A, B\}) = 0$
14		nulmbl	$⊢ (\{A, B\} \subseteq ℝ \land {vol}^{*} (\{A, B\}) = 0) \to \{A, B\} \in dom vol$
15	10 13 14	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \{A, B\} \in dom vol$
16		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
17	16	ineq2i	$⊢ (A, B) \cap \{A, B\} = (A, B) \cap (\{A\} \cup \{B\})$
18		indi	$⊢ (A, B) \cap (\{A\} \cup \{B\}) = ((A, B) \cap \{A\}) \cup ((A, B) \cap \{B\})$
19	17 18	eqtri	$⊢ (A, B) \cap \{A, B\} = ((A, B) \cap \{A\}) \cup ((A, B) \cap \{B\})$
20		simp1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \in ℝ$
21	20	ltnrd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \neg A < A$
22		eliooord	$⊢ A \in (A, B) \to (A < A \land A < B)$
23	22	simpld	$⊢ A \in (A, B) \to A < A$
24	21 23	nsyl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \neg A \in (A, B)$
25		disjsn	$⊢ (A, B) \cap \{A\} = \emptyset \leftrightarrow \neg A \in (A, B)$
26	24 25	sylibr	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to (A, B) \cap \{A\} = \emptyset$
27		simp2	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B \in ℝ$
28	27	ltnrd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \neg B < B$
29		eliooord	$⊢ B \in (A, B) \to (A < B \land B < B)$
30	29	simprd	$⊢ B \in (A, B) \to B < B$
31	28 30	nsyl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \neg B \in (A, B)$
32		disjsn	$⊢ (A, B) \cap \{B\} = \emptyset \leftrightarrow \neg B \in (A, B)$
33	31 32	sylibr	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to (A, B) \cap \{B\} = \emptyset$
34	26 33	uneq12d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ((A, B) \cap \{A\}) \cup ((A, B) \cap \{B\}) = \emptyset \cup \emptyset$
35		un0	$⊢ \emptyset \cup \emptyset = \emptyset$
36	34 35	eqtrdi	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ((A, B) \cap \{A\}) \cup ((A, B) \cap \{B\}) = \emptyset$
37	19 36	eqtrid	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to (A, B) \cap \{A, B\} = \emptyset$
38		ioossicc	$⊢ (A, B) \subseteq [A, B]$
39		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
40	39	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [A, B] \subseteq ℝ$
41		ovolicc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$
42	27 20	resubcld	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B - A \in ℝ$
43	41 42	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) \in ℝ$
44		ovolsscl	$⊢ ((A, B) \subseteq [A, B] \land [A, B] \subseteq ℝ \land {vol}^{} ([A, B]) \in ℝ) \to {vol}^{} ((A, B)) \in ℝ$
45	38 40 43 44	mp3an2i	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ((A, B)) \in ℝ$
46	3 45	eqeltrid	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) \in ℝ$
47		mblvol	$⊢ \{A, B\} \in dom vol \to vol (\{A, B\}) = {vol}^{*} (\{A, B\})$
48	15 47	syl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol (\{A, B\}) = {vol}^{*} (\{A, B\})$
49	48 13	eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol (\{A, B\}) = 0$
50		0re	$⊢ 0 \in ℝ$
51	49 50	eqeltrdi	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol (\{A, B\}) \in ℝ$
52		volun	$⊢ (((A, B) \in dom vol \land \{A, B\} \in dom vol \land (A, B) \cap \{A, B\} = \emptyset) \land (vol ((A, B)) \in ℝ \land vol (\{A, B\}) \in ℝ)) \to vol ((A, B) \cup \{A, B\}) = vol ((A, B)) + vol (\{A, B\})$
53	8 15 37 46 51 52	syl32anc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B) \cup \{A, B\}) = vol ((A, B)) + vol (\{A, B\})$
54		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
55		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
56		id	$⊢ A \leq B \to A \leq B$
57		prunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
58	54 55 56 57	syl3an	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
59	58	fveq2d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B) \cup \{A, B\}) = vol ([A, B])$
60	49	oveq2d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) + vol (\{A, B\}) = vol ((A, B)) + 0$
61	46	recnd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) \in ℂ$
62	61	addid1d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) + 0 = vol ((A, B))$
63	60 62	eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) + vol (\{A, B\}) = vol ((A, B))$
64	53 59 63	3eqtr3d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ([A, B]) = vol ((A, B))$
65	7 64 41	3eqtr3d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
66	3 65	eqtr3id	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ((A, B)) = B - A$

Metamath Proof Explorer

Theorem ovolioo

Proof