volico

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

		Ref	Expression
	Assertion	volico	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) = if (A < B, B - A, 0)$

Proof

Step	Hyp	Ref	Expression
1		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
2	1	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℝ^{*}$
3		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
4	3	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℝ^{*}$
5		simp3	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A < B$
6		snunioo1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{A\} = [A, B)$
7	2 4 5 6	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (A, B) \cup \{A\} = [A, B)$
8	7	eqcomd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to [A, B) = (A, B) \cup \{A\}$
9	8	fveq2d	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ([A, B)) = vol ((A, B) \cup \{A\})$
10		ioombl	$⊢ (A, B) \in dom vol$
11	10	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (A, B) \in dom vol$
12		snmbl	$⊢ A \in ℝ \to \{A\} \in dom vol$
13	12	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to \{A\} \in dom vol$
14		lbioo	$⊢ \neg A \in (A, B)$
15		disjsn	$⊢ (A, B) \cap \{A\} = \emptyset \leftrightarrow \neg A \in (A, B)$
16	14 15	mpbir	$⊢ (A, B) \cap \{A\} = \emptyset$
17	16	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (A, B) \cap \{A\} = \emptyset$
18		ioovolcl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ((A, B)) \in ℝ$
19	18	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) \in ℝ$
20		volsn	$⊢ A \in ℝ \to vol (\{A\}) = 0$
21		0red	$⊢ A \in ℝ \to 0 \in ℝ$
22	20 21	eqeltrd	$⊢ A \in ℝ \to vol (\{A\}) \in ℝ$
23	22	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol (\{A\}) \in ℝ$
24		volun	$⊢ (((A, B) \in dom vol \land \{A\} \in dom vol \land (A, B) \cap \{A\} = \emptyset) \land (vol ((A, B)) \in ℝ \land vol (\{A\}) \in ℝ)) \to vol ((A, B) \cup \{A\}) = vol ((A, B)) + vol (\{A\})$
25	11 13 17 19 23 24	syl32anc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B) \cup \{A\}) = vol ((A, B)) + vol (\{A\})$
26		simp1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℝ$
27		simp2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℝ$
28	26 27 5	ltled	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \leq B$
29		volioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
30	26 27 28 29	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) = B - A$
31	20	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol (\{A\}) = 0$
32	30 31	oveq12d	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) + vol (\{A\}) = B - A + 0$
33	27	recnd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℂ$
34		recn	$⊢ A \in ℝ \to A \in ℂ$
35	34	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℂ$
36	33 35	subcld	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B - A \in ℂ$
37	36	addridd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B - A + 0 = B - A$
38	32 37	eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ((A, B)) + vol (\{A\}) = B - A$
39	9 25 38	3eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to vol ([A, B)) = B - A$
40	39	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land A < B) \to vol ([A, B)) = B - A$
41		iftrue	$⊢ A < B \to if (A < B, B - A, 0) = B - A$
42	41	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land A < B) \to if (A < B, B - A, 0) = B - A$
43	40 42	eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land A < B) \to vol ([A, B)) = if (A < B, B - A, 0)$
44		simpl	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to (A \in ℝ \land B \in ℝ)$
45		simpr	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to \neg A < B$
46	44	simprd	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to B \in ℝ$
47	44	simpld	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to A \in ℝ$
48	46 47	lenltd	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to (B \leq A \leftrightarrow \neg A < B)$
49	45 48	mpbird	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to B \leq A$
50		simpr	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to B \leq A$
51	1	ad2antrr	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to A \in ℝ^{*}$
52	3	ad2antlr	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to B \in ℝ^{*}$
53		ico0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B) = \emptyset \leftrightarrow B \leq A)$
54	51 52 53	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to ([A, B) = \emptyset \leftrightarrow B \leq A)$
55	50 54	mpbird	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to [A, B) = \emptyset$
56	55	fveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to vol ([A, B)) = vol (\emptyset)$
57		vol0	$⊢ vol (\emptyset) = 0$
58	57	a1i	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to vol (\emptyset) = 0$
59	56 58	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land B \leq A) \to vol ([A, B)) = 0$
60	44 49 59	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to vol ([A, B)) = 0$
61		iffalse	$⊢ \neg A < B \to if (A < B, B - A, 0) = 0$
62	61	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to if (A < B, B - A, 0) = 0$
63	60 62	eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land \neg A < B) \to vol ([A, B)) = if (A < B, B - A, 0)$
64	43 63	pm2.61dan	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) = if (A < B, B - A, 0)$

Metamath Proof Explorer

Theorem volico

Proof