volioc

Description: The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	volioc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B]) = B - A$

Proof

Step	Hyp	Ref	Expression
1		vol0	$⊢ vol (\emptyset) = 0$
2		oveq2	$⊢ A = B \to (A, A] = (A, B]$
3	2	eqcomd	$⊢ A = B \to (A, B] = (A, A]$
4		leid	$⊢ A \in ℝ \to A \leq A$
5		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
6		ioc0	$⊢ (A \in ℝ^{} \land A \in ℝ^{}) \to ((A, A] = \emptyset \leftrightarrow A \leq A)$
7	5 5 6	syl2anc	$⊢ A \in ℝ \to ((A, A] = \emptyset \leftrightarrow A \leq A)$
8	4 7	mpbird	$⊢ A \in ℝ \to (A, A] = \emptyset$
9	3 8	sylan9eqr	$⊢ (A \in ℝ \land A = B) \to (A, B] = \emptyset$
10	9	fveq2d	$⊢ (A \in ℝ \land A = B) \to vol ((A, B]) = vol (\emptyset)$
11		eqcom	$⊢ A = B \leftrightarrow B = A$
12	11	biimpi	$⊢ A = B \to B = A$
13	12	adantl	$⊢ (A \in ℝ \land A = B) \to B = A$
14		recn	$⊢ A \in ℝ \to A \in ℂ$
15	14	adantr	$⊢ (A \in ℝ \land A = B) \to A \in ℂ$
16	13 15	eqeltrd	$⊢ (A \in ℝ \land A = B) \to B \in ℂ$
17	16 13	subeq0bd	$⊢ (A \in ℝ \land A = B) \to B - A = 0$
18	1 10 17	3eqtr4a	$⊢ (A \in ℝ \land A = B) \to vol ((A, B]) = B - A$
19	18	3ad2antl1	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land A = B) \to vol ((A, B]) = B - A$
20		simpl1	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land \neg A = B) \to A \in ℝ$
21		simpl2	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land \neg A = B) \to B \in ℝ$
22		simpl3	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land \neg A = B) \to A \leq B$
23		eqcom	$⊢ B = A \leftrightarrow A = B$
24	23	biimpi	$⊢ B = A \to A = B$
25	24	necon3bi	$⊢ \neg A = B \to B \neq A$
26	25	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land \neg A = B) \to B \neq A$
27	20 21 22 26	leneltd	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land \neg A = B) \to A < B$
28	5	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℝ^{*}$
29		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
30	29	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℝ^{*}$
31		simp3	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A < B$
32		ioounsn	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{B\} = (A, B]$
33	28 30 31 32	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (A, B) \cup \{B\} = (A, B]$
34	33	eqcomd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (A, B] = (A, B) \cup \{B\}$
35	34	fveq2d	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B]) = vol ((A, B) \cup \{B\})$
36		ioombl	$⊢ (A, B) \in dom vol$
37	36	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (A, B) \in dom vol$
38		snmbl	$⊢ B \in ℝ \to \{B\} \in dom vol$
39	38	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to \{B\} \in dom vol$
40		ubioo	$⊢ \neg B \in (A, B)$
41		disjsn	$⊢ (A, B) \cap \{B\} = \emptyset \leftrightarrow \neg B \in (A, B)$
42	40 41	mpbir	$⊢ (A, B) \cap \{B\} = \emptyset$
43	42	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (A, B) \cap \{B\} = \emptyset$
44		ioovolcl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ((A, B)) \in ℝ$
45	44	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) \in ℝ$
46		volsn	$⊢ B \in ℝ \to vol (\{B\}) = 0$
47		0red	$⊢ B \in ℝ \to 0 \in ℝ$
48	46 47	eqeltrd	$⊢ B \in ℝ \to vol (\{B\}) \in ℝ$
49	48	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol (\{B\}) \in ℝ$
50		volun	$⊢ (((A, B) \in dom vol \land \{B\} \in dom vol \land (A, B) \cap \{B\} = \emptyset) \land (vol ((A, B)) \in ℝ \land vol (\{B\}) \in ℝ)) \to vol ((A, B) \cup \{B\}) = vol ((A, B)) + vol (\{B\})$
51	37 39 43 45 49 50	syl32anc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B) \cup \{B\}) = vol ((A, B)) + vol (\{B\})$
52		simp1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℝ$
53		simp2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℝ$
54	52 53 31	ltled	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \leq B$
55		volioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
56	52 53 54 55	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) = B - A$
57	46	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol (\{B\}) = 0$
58	56 57	oveq12d	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) + vol (\{B\}) = B - A + 0$
59	53	recnd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℂ$
60	14	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℂ$
61	59 60	subcld	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B - A \in ℂ$
62	61	addid1d	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B - A + 0 = B - A$
63	58 62	eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) + vol (\{B\}) = B - A$
64	35 51 63	3eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B]) = B - A$
65	20 21 27 64	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land \neg A = B) \to vol ((A, B]) = B - A$
66	19 65	pm2.61dan	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B]) = B - A$

Metamath Proof Explorer

Theorem volioc

Proof