volcn

Description: The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014)

		Ref	Expression
	Hypothesis	volcn.1	$⊢ F = (x \in ℝ ⟼ vol (A \cap [B, x]))$
	Assertion	volcn	$⊢ (A \in dom vol \land B \in ℝ) \to F : ℝ \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		volcn.1	$⊢ F = (x \in ℝ ⟼ vol (A \cap [B, x]))$
2		simpll	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to A \in dom vol$
3		iccmbl	$⊢ (B \in ℝ \land x \in ℝ) \to [B, x] \in dom vol$
4	3	adantll	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to [B, x] \in dom vol$
5		inmbl	$⊢ (A \in dom vol \land [B, x] \in dom vol) \to A \cap [B, x] \in dom vol$
6	2 4 5	syl2anc	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to A \cap [B, x] \in dom vol$
7		mblvol	$⊢ A \cap [B, x] \in dom vol \to vol (A \cap [B, x]) = {vol}^{*} (A \cap [B, x])$
8	6 7	syl	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to vol (A \cap [B, x]) = {vol}^{*} (A \cap [B, x])$
9		inss2	$⊢ A \cap [B, x] \subseteq [B, x]$
10		mblss	$⊢ [B, x] \in dom vol \to [B, x] \subseteq ℝ$
11	4 10	syl	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to [B, x] \subseteq ℝ$
12		mblvol	$⊢ [B, x] \in dom vol \to vol ([B, x]) = {vol}^{*} ([B, x])$
13	4 12	syl	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to vol ([B, x]) = {vol}^{*} ([B, x])$
14		iccvolcl	$⊢ (B \in ℝ \land x \in ℝ) \to vol ([B, x]) \in ℝ$
15	14	adantll	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to vol ([B, x]) \in ℝ$
16	13 15	eqeltrrd	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to {vol}^{*} ([B, x]) \in ℝ$
17		ovolsscl	$⊢ (A \cap [B, x] \subseteq [B, x] \land [B, x] \subseteq ℝ \land {vol}^{} ([B, x]) \in ℝ) \to {vol}^{} (A \cap [B, x]) \in ℝ$
18	9 11 16 17	mp3an2i	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to {vol}^{*} (A \cap [B, x]) \in ℝ$
19	8 18	eqeltrd	$⊢ ((A \in dom vol \land B \in ℝ) \land x \in ℝ) \to vol (A \cap [B, x]) \in ℝ$
20	19 1	fmptd	$⊢ (A \in dom vol \land B \in ℝ) \to F : ℝ ⟶ ℝ$
21		simprr	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \in ℝ \land e \in ℝ^{+})) \to e \in ℝ^{+}$
22		oveq12	$⊢ (v = z \land u = y) \to v - u = z - y$
23	22	ancoms	$⊢ (u = y \land v = z) \to v - u = z - y$
24	23	fveq2d	$⊢ (u = y \land v = z) \to \|v - u\| = \|z - y\|$
25	24	breq1d	$⊢ (u = y \land v = z) \to (\|v - u\| < e \leftrightarrow \|z - y\| < e)$
26		fveq2	$⊢ v = z \to F (v) = F (z)$
27		fveq2	$⊢ u = y \to F (u) = F (y)$
28	26 27	oveqan12rd	$⊢ (u = y \land v = z) \to F (v) - F (u) = F (z) - F (y)$
29	28	fveq2d	$⊢ (u = y \land v = z) \to \|F (v) - F (u)\| = \|F (z) - F (y)\|$
30	29	breq1d	$⊢ (u = y \land v = z) \to (\|F (v) - F (u)\| < e \leftrightarrow \|F (z) - F (y)\| < e)$
31	25 30	imbi12d	$⊢ (u = y \land v = z) \to ((\|v - u\| < e \to \|F (v) - F (u)\| < e) \leftrightarrow (\|z - y\| < e \to \|F (z) - F (y)\| < e))$
32		oveq12	$⊢ (v = y \land u = z) \to v - u = y - z$
33	32	ancoms	$⊢ (u = z \land v = y) \to v - u = y - z$
34	33	fveq2d	$⊢ (u = z \land v = y) \to \|v - u\| = \|y - z\|$
35	34	breq1d	$⊢ (u = z \land v = y) \to (\|v - u\| < e \leftrightarrow \|y - z\| < e)$
36		fveq2	$⊢ v = y \to F (v) = F (y)$
37		fveq2	$⊢ u = z \to F (u) = F (z)$
38	36 37	oveqan12rd	$⊢ (u = z \land v = y) \to F (v) - F (u) = F (y) - F (z)$
39	38	fveq2d	$⊢ (u = z \land v = y) \to \|F (v) - F (u)\| = \|F (y) - F (z)\|$
40	39	breq1d	$⊢ (u = z \land v = y) \to (\|F (v) - F (u)\| < e \leftrightarrow \|F (y) - F (z)\| < e)$
41	35 40	imbi12d	$⊢ (u = z \land v = y) \to ((\|v - u\| < e \to \|F (v) - F (u)\| < e) \leftrightarrow (\|y - z\| < e \to \|F (y) - F (z)\| < e))$
42		ssidd	$⊢ ((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \to ℝ \subseteq ℝ$
43		recn	$⊢ z \in ℝ \to z \in ℂ$
44		recn	$⊢ y \in ℝ \to y \in ℂ$
45		abssub	$⊢ (z \in ℂ \land y \in ℂ) \to \|z - y\| = \|y - z\|$
46	43 44 45	syl2anr	$⊢ (y \in ℝ \land z \in ℝ) \to \|z - y\| = \|y - z\|$
47	46	adantl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ)) \to \|z - y\| = \|y - z\|$
48	47	breq1d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ)) \to (\|z - y\| < e \leftrightarrow \|y - z\| < e)$
49	20	adantr	$⊢ ((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \to F : ℝ ⟶ ℝ$
50		ffvelrn	$⊢ (F : ℝ ⟶ ℝ \land y \in ℝ) \to F (y) \in ℝ$
51		ffvelrn	$⊢ (F : ℝ ⟶ ℝ \land z \in ℝ) \to F (z) \in ℝ$
52	50 51	anim12dan	$⊢ (F : ℝ ⟶ ℝ \land (y \in ℝ \land z \in ℝ)) \to (F (y) \in ℝ \land F (z) \in ℝ)$
53	49 52	sylan	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ)) \to (F (y) \in ℝ \land F (z) \in ℝ)$
54		recn	$⊢ F (z) \in ℝ \to F (z) \in ℂ$
55		recn	$⊢ F (y) \in ℝ \to F (y) \in ℂ$
56		abssub	$⊢ (F (z) \in ℂ \land F (y) \in ℂ) \to \|F (z) - F (y)\| = \|F (y) - F (z)\|$
57	54 55 56	syl2anr	$⊢ (F (y) \in ℝ \land F (z) \in ℝ) \to \|F (z) - F (y)\| = \|F (y) - F (z)\|$
58	53 57	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ)) \to \|F (z) - F (y)\| = \|F (y) - F (z)\|$
59	58	breq1d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ)) \to (\|F (z) - F (y)\| < e \leftrightarrow \|F (y) - F (z)\| < e)$
60	48 59	imbi12d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ)) \to ((\|z - y\| < e \to \|F (z) - F (y)\| < e) \leftrightarrow (\|y - z\| < e \to \|F (y) - F (z)\| < e))$
61		simpr2	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to z \in ℝ$
62		oveq2	$⊢ x = z \to [B, x] = [B, z]$
63	62	ineq2d	$⊢ x = z \to A \cap [B, x] = A \cap [B, z]$
64	63	fveq2d	$⊢ x = z \to vol (A \cap [B, x]) = vol (A \cap [B, z])$
65		fvex	$⊢ vol (A \cap [B, z]) \in V$
66	64 1 65	fvmpt	$⊢ z \in ℝ \to F (z) = vol (A \cap [B, z])$
67	61 66	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (z) = vol (A \cap [B, z])$
68		simplll	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \in dom vol$
69		simplr	$⊢ ((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \to B \in ℝ$
70	69	adantr	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to B \in ℝ$
71		iccmbl	$⊢ (B \in ℝ \land z \in ℝ) \to [B, z] \in dom vol$
72	70 61 71	syl2anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to [B, z] \in dom vol$
73		inmbl	$⊢ (A \in dom vol \land [B, z] \in dom vol) \to A \cap [B, z] \in dom vol$
74	68 72 73	syl2anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \cap [B, z] \in dom vol$
75		mblvol	$⊢ A \cap [B, z] \in dom vol \to vol (A \cap [B, z]) = {vol}^{*} (A \cap [B, z])$
76	74 75	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to vol (A \cap [B, z]) = {vol}^{*} (A \cap [B, z])$
77	67 76	eqtrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (z) = {vol}^{*} (A \cap [B, z])$
78		simpr1	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to y \in ℝ$
79		oveq2	$⊢ x = y \to [B, x] = [B, y]$
80	79	ineq2d	$⊢ x = y \to A \cap [B, x] = A \cap [B, y]$
81	80	fveq2d	$⊢ x = y \to vol (A \cap [B, x]) = vol (A \cap [B, y])$
82		fvex	$⊢ vol (A \cap [B, y]) \in V$
83	81 1 82	fvmpt	$⊢ y \in ℝ \to F (y) = vol (A \cap [B, y])$
84	78 83	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (y) = vol (A \cap [B, y])$
85		simp1	$⊢ (y \in ℝ \land z \in ℝ \land y \leq z) \to y \in ℝ$
86		iccmbl	$⊢ (B \in ℝ \land y \in ℝ) \to [B, y] \in dom vol$
87	69 85 86	syl2an	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to [B, y] \in dom vol$
88		inmbl	$⊢ (A \in dom vol \land [B, y] \in dom vol) \to A \cap [B, y] \in dom vol$
89	68 87 88	syl2anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \cap [B, y] \in dom vol$
90		mblvol	$⊢ A \cap [B, y] \in dom vol \to vol (A \cap [B, y]) = {vol}^{*} (A \cap [B, y])$
91	89 90	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to vol (A \cap [B, y]) = {vol}^{*} (A \cap [B, y])$
92	84 91	eqtrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (y) = {vol}^{*} (A \cap [B, y])$
93	77 92	oveq12d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (z) - F (y) = {vol}^{} (A \cap [B, z]) - {vol}^{} (A \cap [B, y])$
94	49	adantr	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F : ℝ ⟶ ℝ$
95	94 61	ffvelrnd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (z) \in ℝ$
96	77 95	eqeltrrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{*} (A \cap [B, z]) \in ℝ$
97	70	leidd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to B \leq B$
98		simpr3	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to y \leq z$
99		iccss	$⊢ ((B \in ℝ \land z \in ℝ) \land (B \leq B \land y \leq z)) \to [B, y] \subseteq [B, z]$
100	70 61 97 98 99	syl22anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to [B, y] \subseteq [B, z]$
101		sslin	$⊢ [B, y] \subseteq [B, z] \to A \cap [B, y] \subseteq A \cap [B, z]$
102	100 101	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \cap [B, y] \subseteq A \cap [B, z]$
103		mblss	$⊢ A \cap [B, z] \in dom vol \to A \cap [B, z] \subseteq ℝ$
104	74 103	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \cap [B, z] \subseteq ℝ$
105	102 104	sstrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \cap [B, y] \subseteq ℝ$
106		iccssre	$⊢ (y \in ℝ \land z \in ℝ) \to [y, z] \subseteq ℝ$
107	78 61 106	syl2anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to [y, z] \subseteq ℝ$
108	105 107	unssd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to (A \cap [B, y]) \cup [y, z] \subseteq ℝ$
109	94 78	ffvelrnd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (y) \in ℝ$
110	92 109	eqeltrrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{*} (A \cap [B, y]) \in ℝ$
111	61 78	resubcld	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to z - y \in ℝ$
112	110 111	readdcld	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{*} (A \cap [B, y]) + z - y \in ℝ$
113		ovolicc	$⊢ (y \in ℝ \land z \in ℝ \land y \leq z) \to {vol}^{*} ([y, z]) = z - y$
114	113	adantl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{*} ([y, z]) = z - y$
115	114 111	eqeltrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{*} ([y, z]) \in ℝ$
116		ovolun	$⊢ ((A \cap [B, y] \subseteq ℝ \land {vol}^{} (A \cap [B, y]) \in ℝ) \land ([y, z] \subseteq ℝ \land {vol}^{} ([y, z]) \in ℝ)) \to {vol}^{} ((A \cap [B, y]) \cup [y, z]) \leq {vol}^{} (A \cap [B, y]) + {vol}^{*} ([y, z])$
117	105 110 107 115 116	syl22anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{} ((A \cap [B, y]) \cup [y, z]) \leq {vol}^{} (A \cap [B, y]) + {vol}^{*} ([y, z])$
118	114	oveq2d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{} (A \cap [B, y]) + {vol}^{} ([y, z]) = {vol}^{*} (A \cap [B, y]) + z - y$
119	117 118	breqtrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{} ((A \cap [B, y]) \cup [y, z]) \leq {vol}^{} (A \cap [B, y]) + z - y$
120		ovollecl	$⊢ ((A \cap [B, y]) \cup [y, z] \subseteq ℝ \land {vol}^{} (A \cap [B, y]) + z - y \in ℝ \land {vol}^{} ((A \cap [B, y]) \cup [y, z]) \leq {vol}^{} (A \cap [B, y]) + z - y) \to {vol}^{} ((A \cap [B, y]) \cup [y, z]) \in ℝ$
121	108 112 119 120	syl3anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{*} ((A \cap [B, y]) \cup [y, z]) \in ℝ$
122	70	adantr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to B \in ℝ$
123	61	adantr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to z \in ℝ$
124	78	adantr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to y \in ℝ$
125		simpr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to B \leq y$
126	98	adantr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to y \leq z$
127		simp2	$⊢ (y \in ℝ \land z \in ℝ \land y \leq z) \to z \in ℝ$
128		elicc2	$⊢ (B \in ℝ \land z \in ℝ) \to (y \in [B, z] \leftrightarrow (y \in ℝ \land B \leq y \land y \leq z))$
129	69 127 128	syl2an	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to (y \in [B, z] \leftrightarrow (y \in ℝ \land B \leq y \land y \leq z))$
130	129	adantr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to (y \in [B, z] \leftrightarrow (y \in ℝ \land B \leq y \land y \leq z))$
131	124 125 126 130	mpbir3and	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to y \in [B, z]$
132		iccsplit	$⊢ (B \in ℝ \land z \in ℝ \land y \in [B, z]) \to [B, z] = [B, y] \cup [y, z]$
133	122 123 131 132	syl3anc	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to [B, z] = [B, y] \cup [y, z]$
134		eqimss	$⊢ [B, z] = [B, y] \cup [y, z] \to [B, z] \subseteq [B, y] \cup [y, z]$
135	133 134	syl	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land B \leq y) \to [B, z] \subseteq [B, y] \cup [y, z]$
136	78	adantr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land y \leq B) \to y \in ℝ$
137	61	adantr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land y \leq B) \to z \in ℝ$
138		simpr	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land y \leq B) \to y \leq B$
139	137	leidd	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land y \leq B) \to z \leq z$
140		iccss	$⊢ ((y \in ℝ \land z \in ℝ) \land (y \leq B \land z \leq z)) \to [B, z] \subseteq [y, z]$
141	136 137 138 139 140	syl22anc	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land y \leq B) \to [B, z] \subseteq [y, z]$
142		ssun4	$⊢ [B, z] \subseteq [y, z] \to [B, z] \subseteq [B, y] \cup [y, z]$
143	141 142	syl	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \land y \leq B) \to [B, z] \subseteq [B, y] \cup [y, z]$
144	70 78 135 143	lecasei	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to [B, z] \subseteq [B, y] \cup [y, z]$
145		sslin	$⊢ [B, z] \subseteq [B, y] \cup [y, z] \to A \cap [B, z] \subseteq A \cap ([B, y] \cup [y, z])$
146	144 145	syl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \cap [B, z] \subseteq A \cap ([B, y] \cup [y, z])$
147		indi	$⊢ A \cap ([B, y] \cup [y, z]) = (A \cap [B, y]) \cup (A \cap [y, z])$
148		inss2	$⊢ A \cap [y, z] \subseteq [y, z]$
149		unss2	$⊢ A \cap [y, z] \subseteq [y, z] \to (A \cap [B, y]) \cup (A \cap [y, z]) \subseteq (A \cap [B, y]) \cup [y, z]$
150	148 149	ax-mp	$⊢ (A \cap [B, y]) \cup (A \cap [y, z]) \subseteq (A \cap [B, y]) \cup [y, z]$
151	147 150	eqsstri	$⊢ A \cap ([B, y] \cup [y, z]) \subseteq (A \cap [B, y]) \cup [y, z]$
152	146 151	sstrdi	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to A \cap [B, z] \subseteq (A \cap [B, y]) \cup [y, z]$
153		ovolss	$⊢ (A \cap [B, z] \subseteq (A \cap [B, y]) \cup [y, z] \land (A \cap [B, y]) \cup [y, z] \subseteq ℝ) \to {vol}^{} (A \cap [B, z]) \leq {vol}^{} ((A \cap [B, y]) \cup [y, z])$
154	152 108 153	syl2anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{} (A \cap [B, z]) \leq {vol}^{} ((A \cap [B, y]) \cup [y, z])$
155	96 121 112 154 119	letrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{} (A \cap [B, z]) \leq {vol}^{} (A \cap [B, y]) + z - y$
156	96 110 111	lesubadd2d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to ({vol}^{} (A \cap [B, z]) - {vol}^{} (A \cap [B, y]) \leq z - y \leftrightarrow {vol}^{} (A \cap [B, z]) \leq {vol}^{} (A \cap [B, y]) + z - y)$
157	155 156	mpbird	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{} (A \cap [B, z]) - {vol}^{} (A \cap [B, y]) \leq z - y$
158	93 157	eqbrtrd	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (z) - F (y) \leq z - y$
159	95 109	resubcld	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (z) - F (y) \in ℝ$
160		simplr	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to e \in ℝ^{+}$
161	160	rpred	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to e \in ℝ$
162		lelttr	$⊢ (F (z) - F (y) \in ℝ \land z - y \in ℝ \land e \in ℝ) \to ((F (z) - F (y) \leq z - y \land z - y < e) \to F (z) - F (y) < e)$
163	159 111 161 162	syl3anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to ((F (z) - F (y) \leq z - y \land z - y < e) \to F (z) - F (y) < e)$
164	158 163	mpand	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to (z - y < e \to F (z) - F (y) < e)$
165		abssubge0	$⊢ (y \in ℝ \land z \in ℝ \land y \leq z) \to \|z - y\| = z - y$
166	165	adantl	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to \|z - y\| = z - y$
167	166	breq1d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to (\|z - y\| < e \leftrightarrow z - y < e)$
168		ovolss	$⊢ (A \cap [B, y] \subseteq A \cap [B, z] \land A \cap [B, z] \subseteq ℝ) \to {vol}^{} (A \cap [B, y]) \leq {vol}^{} (A \cap [B, z])$
169	102 104 168	syl2anc	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to {vol}^{} (A \cap [B, y]) \leq {vol}^{} (A \cap [B, z])$
170	169 92 77	3brtr4d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to F (y) \leq F (z)$
171	109 95 170	abssubge0d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to \|F (z) - F (y)\| = F (z) - F (y)$
172	171	breq1d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to (\|F (z) - F (y)\| < e \leftrightarrow F (z) - F (y) < e)$
173	164 167 172	3imtr4d	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ \land y \leq z)) \to (\|z - y\| < e \to \|F (z) - F (y)\| < e)$
174	31 41 42 60 173	wlogle	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land (y \in ℝ \land z \in ℝ)) \to (\|z - y\| < e \to \|F (z) - F (y)\| < e)$
175	174	anassrs	$⊢ ((((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land y \in ℝ) \land z \in ℝ) \to (\|z - y\| < e \to \|F (z) - F (y)\| < e)$
176	175	ralrimiva	$⊢ (((A \in dom vol \land B \in ℝ) \land e \in ℝ^{+}) \land y \in ℝ) \to \forall z \in ℝ (\|z - y\| < e \to \|F (z) - F (y)\| < e)$
177	176	anasss	$⊢ ((A \in dom vol \land B \in ℝ) \land (e \in ℝ^{+} \land y \in ℝ)) \to \forall z \in ℝ (\|z - y\| < e \to \|F (z) - F (y)\| < e)$
178	177	ancom2s	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \in ℝ \land e \in ℝ^{+})) \to \forall z \in ℝ (\|z - y\| < e \to \|F (z) - F (y)\| < e)$
179		breq2	$⊢ d = e \to (\|z - y\| < d \leftrightarrow \|z - y\| < e)$
180	179	rspceaimv	$⊢ (e \in ℝ^{+} \land \forall z \in ℝ (\|z - y\| < e \to \|F (z) - F (y)\| < e)) \to \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|F (z) - F (y)\| < e)$
181	21 178 180	syl2anc	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \in ℝ \land e \in ℝ^{+})) \to \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|F (z) - F (y)\| < e)$
182	181	ralrimivva	$⊢ (A \in dom vol \land B \in ℝ) \to \forall y \in ℝ \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|F (z) - F (y)\| < e)$
183		ax-resscn	$⊢ ℝ \subseteq ℂ$
184		elcncf2	$⊢ (ℝ \subseteq ℂ \land ℝ \subseteq ℂ) \to (F : ℝ \underset{cn}{⟶} ℝ \leftrightarrow (F : ℝ ⟶ ℝ \land \forall y \in ℝ \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|F (z) - F (y)\| < e)))$
185	183 183 184	mp2an	$⊢ F : ℝ \underset{cn}{⟶} ℝ \leftrightarrow (F : ℝ ⟶ ℝ \land \forall y \in ℝ \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|F (z) - F (y)\| < e))$
186	20 182 185	sylanbrc	$⊢ (A \in dom vol \land B \in ℝ) \to F : ℝ \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem volcn

Proof