hoidmv1lelem3

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the nonempty, finite generalized sum, sub case in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmv1lelem3.a	$⊢ φ \to A \in ℝ$
	hoidmv1lelem3.b	$⊢ φ \to B \in ℝ$
	hoidmv1lelem3.l	$⊢ φ \to A < B$
	hoidmv1lelem3.c	$⊢ φ \to C : ℕ ⟶ ℝ$
	hoidmv1lelem3.d	$⊢ φ \to D : ℕ ⟶ ℝ$
	hoidmv1lelem3.x	$⊢ φ \to [A, B) \subseteq ⋃_{j \in ℕ} [C (j), D (j))$
	hoidmv1lelem3.r	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), D (j))))) \in ℝ$
	hoidmv1lelem3.u	$⊢ U = \{z \in [A, B] \| z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))))\}$
	hoidmv1lelem3.s	$⊢ S = sup (U ℝ <)$
Assertion	hoidmv1lelem3	$⊢ φ \to B - A \leq sum^((j \in ℕ ⟼ vol ([C (j), D (j)))))$

Proof

Step	Hyp	Ref	Expression
1		hoidmv1lelem3.a	$⊢ φ \to A \in ℝ$
2		hoidmv1lelem3.b	$⊢ φ \to B \in ℝ$
3		hoidmv1lelem3.l	$⊢ φ \to A < B$
4		hoidmv1lelem3.c	$⊢ φ \to C : ℕ ⟶ ℝ$
5		hoidmv1lelem3.d	$⊢ φ \to D : ℕ ⟶ ℝ$
6		hoidmv1lelem3.x	$⊢ φ \to [A, B) \subseteq ⋃_{j \in ℕ} [C (j), D (j))$
7		hoidmv1lelem3.r	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), D (j))))) \in ℝ$
8		hoidmv1lelem3.u	$⊢ U = \{z \in [A, B] \| z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))))\}$
9		hoidmv1lelem3.s	$⊢ S = sup (U ℝ <)$
10	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
11		nnex	$⊢ ℕ \in V$
12	11	a1i	$⊢ φ \to ℕ \in V$
13		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
14		0xr	$⊢ 0 \in ℝ^{*}$
15	14	a1i	$⊢ (φ \land j \in ℕ) \to 0 \in ℝ^{*}$
16		pnfxr	$⊢ +∞ \in ℝ^{*}$
17	16	a1i	$⊢ (φ \land j \in ℕ) \to +∞ \in ℝ^{*}$
18	4	ffvelrnda	$⊢ (φ \land j \in ℕ) \to C (j) \in ℝ$
19	5	ffvelrnda	$⊢ (φ \land j \in ℕ) \to D (j) \in ℝ$
20	2	adantr	$⊢ (φ \land j \in ℕ) \to B \in ℝ$
21	19 20	ifcld	$⊢ (φ \land j \in ℕ) \to if (D (j) \leq B, D (j), B) \in ℝ$
22		volicore	$⊢ (C (j) \in ℝ \land if (D (j) \leq B, D (j), B) \in ℝ) \to vol ([C (j), if (D (j) \leq B, D (j), B))) \in ℝ$
23	18 21 22	syl2anc	$⊢ (φ \land j \in ℕ) \to vol ([C (j), if (D (j) \leq B, D (j), B))) \in ℝ$
24	23	rexrd	$⊢ (φ \land j \in ℕ) \to vol ([C (j), if (D (j) \leq B, D (j), B))) \in ℝ^{*}$
25	21	rexrd	$⊢ (φ \land j \in ℕ) \to if (D (j) \leq B, D (j), B) \in ℝ^{*}$
26		icombl	$⊢ (C (j) \in ℝ \land if (D (j) \leq B, D (j), B) \in ℝ^{*}) \to [C (j), if (D (j) \leq B, D (j), B)) \in dom vol$
27	18 25 26	syl2anc	$⊢ (φ \land j \in ℕ) \to [C (j), if (D (j) \leq B, D (j), B)) \in dom vol$
28		volge0	$⊢ [C (j), if (D (j) \leq B, D (j), B)) \in dom vol \to 0 \leq vol ([C (j), if (D (j) \leq B, D (j), B)))$
29	27 28	syl	$⊢ (φ \land j \in ℕ) \to 0 \leq vol ([C (j), if (D (j) \leq B, D (j), B)))$
30	23	ltpnfd	$⊢ (φ \land j \in ℕ) \to vol ([C (j), if (D (j) \leq B, D (j), B))) < +∞$
31	15 17 24 29 30	elicod	$⊢ (φ \land j \in ℕ) \to vol ([C (j), if (D (j) \leq B, D (j), B))) \in [0, +∞)$
32	13 31	sselid	$⊢ (φ \land j \in ℕ) \to vol ([C (j), if (D (j) \leq B, D (j), B))) \in [0, +∞]$
33		eqid	$⊢ (j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B)))) = (j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))$
34	32 33	fmptd	$⊢ φ \to (j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B)))) : ℕ ⟶ [0, +∞]$
35	12 34	sge0xrcl	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) \in ℝ^{*}$
36	16	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
37	7	rexrd	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), D (j))))) \in ℝ^{*}$
38		nfv	$⊢ Ⅎ j φ$
39		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
40	39	a1i	$⊢ (φ \land j \in ℕ) \to vol : dom vol ⟶ [0, +∞]$
41	19	rexrd	$⊢ (φ \land j \in ℕ) \to D (j) \in ℝ^{*}$
42		icombl	$⊢ (C (j) \in ℝ \land D (j) \in ℝ^{*}) \to [C (j), D (j)) \in dom vol$
43	18 41 42	syl2anc	$⊢ (φ \land j \in ℕ) \to [C (j), D (j)) \in dom vol$
44	40 43	ffvelrnd	$⊢ (φ \land j \in ℕ) \to vol ([C (j), D (j))) \in [0, +∞]$
45	18	rexrd	$⊢ (φ \land j \in ℕ) \to C (j) \in ℝ^{*}$
46	18	leidd	$⊢ (φ \land j \in ℕ) \to C (j) \leq C (j)$
47		min1	$⊢ (D (j) \in ℝ \land B \in ℝ) \to if (D (j) \leq B, D (j), B) \leq D (j)$
48	19 20 47	syl2anc	$⊢ (φ \land j \in ℕ) \to if (D (j) \leq B, D (j), B) \leq D (j)$
49		icossico	$⊢ ((C (j) \in ℝ^{} \land D (j) \in ℝ^{}) \land (C (j) \leq C (j) \land if (D (j) \leq B, D (j), B) \leq D (j))) \to [C (j), if (D (j) \leq B, D (j), B)) \subseteq [C (j), D (j))$
50	45 41 46 48 49	syl22anc	$⊢ (φ \land j \in ℕ) \to [C (j), if (D (j) \leq B, D (j), B)) \subseteq [C (j), D (j))$
51		volss	$⊢ ([C (j), if (D (j) \leq B, D (j), B)) \in dom vol \land [C (j), D (j)) \in dom vol \land [C (j), if (D (j) \leq B, D (j), B)) \subseteq [C (j), D (j))) \to vol ([C (j), if (D (j) \leq B, D (j), B))) \leq vol ([C (j), D (j)))$
52	27 43 50 51	syl3anc	$⊢ (φ \land j \in ℕ) \to vol ([C (j), if (D (j) \leq B, D (j), B))) \leq vol ([C (j), D (j)))$
53	38 12 32 44 52	sge0lempt	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) \leq sum^((j \in ℕ ⟼ vol ([C (j), D (j)))))$
54	7	ltpnfd	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), D (j))))) < +∞$
55	35 37 36 53 54	xrlelttrd	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) < +∞$
56	35 36 55	xrltned	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) \neq +∞$
57	56	neneqd	$⊢ φ \to \neg sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) = +∞$
58	12 34	sge0repnf	$⊢ φ \to (sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) \in ℝ \leftrightarrow \neg sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) = +∞)$
59	57 58	mpbird	$⊢ φ \to sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))) \in ℝ$
60	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
61	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
62		ssrab2	$⊢ \{z \in [A, B] \| z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))))\} \subseteq [A, B]$
63	8 62	eqsstri	$⊢ U \subseteq [A, B]$
64	1 2 3 4 5 7 8 9	hoidmv1lelem1	$⊢ φ \to (S \in U \land A \in U \land \exists x \in ℝ \forall y \in U y \leq x)$
65	64	simp1d	$⊢ φ \to S \in U$
66	63 65	sselid	$⊢ φ \to S \in [A, B]$
67	61 66	sseldd	$⊢ φ \to S \in ℝ$
68	67	rexrd	$⊢ φ \to S \in ℝ^{*}$
69		simpl	$⊢ (φ \land \neg B \leq S) \to φ$
70		simpr	$⊢ (φ \land \neg B \leq S) \to \neg B \leq S$
71	69 67	syl	$⊢ (φ \land \neg B \leq S) \to S \in ℝ$
72	69 2	syl	$⊢ (φ \land \neg B \leq S) \to B \in ℝ$
73	71 72	ltnled	$⊢ (φ \land \neg B \leq S) \to (S < B \leftrightarrow \neg B \leq S)$
74	70 73	mpbird	$⊢ (φ \land \neg B \leq S) \to S < B$
75	6	adantr	$⊢ (φ \land S < B) \to [A, B) \subseteq ⋃_{j \in ℕ} [C (j), D (j))$
76	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
77	76	adantr	$⊢ (φ \land S < B) \to A \in ℝ^{*}$
78	60	adantr	$⊢ (φ \land S < B) \to B \in ℝ^{*}$
79	68	adantr	$⊢ (φ \land S < B) \to S \in ℝ^{*}$
80	63 61	sstrid	$⊢ φ \to U \subseteq ℝ$
81	65	ne0d	$⊢ φ \to U \neq \emptyset$
82	64	simp3d	$⊢ φ \to \exists x \in ℝ \forall y \in U y \leq x$
83	64	simp2d	$⊢ φ \to A \in U$
84		suprub	$⊢ ((U \subseteq ℝ \land U \neq \emptyset \land \exists x \in ℝ \forall y \in U y \leq x) \land A \in U) \to A \leq sup (U ℝ <)$
85	80 81 82 83 84	syl31anc	$⊢ φ \to A \leq sup (U ℝ <)$
86	85 9	breqtrrdi	$⊢ φ \to A \leq S$
87	86	adantr	$⊢ (φ \land S < B) \to A \leq S$
88		simpr	$⊢ (φ \land S < B) \to S < B$
89	77 78 79 87 88	elicod	$⊢ (φ \land S < B) \to S \in [A, B)$
90	75 89	sseldd	$⊢ (φ \land S < B) \to S \in ⋃_{j \in ℕ} [C (j), D (j))$
91		eliun	$⊢ S \in ⋃_{j \in ℕ} [C (j), D (j)) \leftrightarrow \exists j \in ℕ S \in [C (j), D (j))$
92	90 91	sylib	$⊢ (φ \land S < B) \to \exists j \in ℕ S \in [C (j), D (j))$
93	1	adantr	$⊢ (φ \land S < B) \to A \in ℝ$
94	93	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to A \in ℝ$
95	2	adantr	$⊢ (φ \land S < B) \to B \in ℝ$
96	95	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to B \in ℝ$
97	4	adantr	$⊢ (φ \land S < B) \to C : ℕ ⟶ ℝ$
98	97	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to C : ℕ ⟶ ℝ$
99	5	adantr	$⊢ (φ \land S < B) \to D : ℕ ⟶ ℝ$
100	99	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to D : ℕ ⟶ ℝ$
101		fveq2	$⊢ i = j \to C (i) = C (j)$
102		fveq2	$⊢ i = j \to D (i) = D (j)$
103	101 102	oveq12d	$⊢ i = j \to [C (i), D (i)) = [C (j), D (j))$
104	103	fveq2d	$⊢ i = j \to vol ([C (i), D (i))) = vol ([C (j), D (j)))$
105	104	cbvmptv	$⊢ (i \in ℕ ⟼ vol ([C (i), D (i)))) = (j \in ℕ ⟼ vol ([C (j), D (j))))$
106	105	fveq2i	$⊢ sum^((i \in ℕ ⟼ vol ([C (i), D (i))))) = sum^((j \in ℕ ⟼ vol ([C (j), D (j)))))$
107	106 7	eqeltrid	$⊢ φ \to sum^((i \in ℕ ⟼ vol ([C (i), D (i))))) \in ℝ$
108	107	adantr	$⊢ (φ \land S < B) \to sum^((i \in ℕ ⟼ vol ([C (i), D (i))))) \in ℝ$
109	108	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to sum^((i \in ℕ ⟼ vol ([C (i), D (i))))) \in ℝ$
110	102	breq1d	$⊢ i = j \to (D (i) \leq z \leftrightarrow D (j) \leq z)$
111	110 102	ifbieq1d	$⊢ i = j \to if (D (i) \leq z, D (i), z) = if (D (j) \leq z, D (j), z)$
112	101 111	oveq12d	$⊢ i = j \to [C (i), if (D (i) \leq z, D (i), z)) = [C (j), if (D (j) \leq z, D (j), z))$
113	112	fveq2d	$⊢ i = j \to vol ([C (i), if (D (i) \leq z, D (i), z))) = vol ([C (j), if (D (j) \leq z, D (j), z)))$
114	113	cbvmptv	$⊢ (i \in ℕ ⟼ vol ([C (i), if (D (i) \leq z, D (i), z)))) = (j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z))))$
115	114	eqcomi	$⊢ (j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))) = (i \in ℕ ⟼ vol ([C (i), if (D (i) \leq z, D (i), z))))$
116	115	fveq2i	$⊢ sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z))))) = sum^((i \in ℕ ⟼ vol ([C (i), if (D (i) \leq z, D (i), z)))))$
117	116	breq2i	$⊢ z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z))))) \leftrightarrow z - A \leq sum^((i \in ℕ ⟼ vol ([C (i), if (D (i) \leq z, D (i), z)))))$
118	117	rabbii	$⊢ \{z \in [A, B] \| z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))))\} = \{z \in [A, B] \| z - A \leq sum^((i \in ℕ ⟼ vol ([C (i), if (D (i) \leq z, D (i), z)))))\}$
119	8 118	eqtri	$⊢ U = \{z \in [A, B] \| z - A \leq sum^((i \in ℕ ⟼ vol ([C (i), if (D (i) \leq z, D (i), z)))))\}$
120	65	adantr	$⊢ (φ \land S < B) \to S \in U$
121	120	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to S \in U$
122	87	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to A \leq S$
123	88	3ad2ant1	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to S < B$
124		simp2	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to j \in ℕ$
125		simp3	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to S \in [C (j), D (j))$
126		eqid	$⊢ if (D (j) \leq B, D (j), B) = if (D (j) \leq B, D (j), B)$
127	94 96 98 100 109 119 121 122 123 124 125 126	hoidmv1lelem2	$⊢ ((φ \land S < B) \land j \in ℕ \land S \in [C (j), D (j))) \to \exists u \in U S < u$
128	127	3exp	$⊢ (φ \land S < B) \to (j \in ℕ \to (S \in [C (j), D (j)) \to \exists u \in U S < u))$
129	128	rexlimdv	$⊢ (φ \land S < B) \to (\exists j \in ℕ S \in [C (j), D (j)) \to \exists u \in U S < u)$
130	92 129	mpd	$⊢ (φ \land S < B) \to \exists u \in U S < u$
131	69 74 130	syl2anc	$⊢ (φ \land \neg B \leq S) \to \exists u \in U S < u$
132	61	adantr	$⊢ (φ \land u \in U) \to [A, B] \subseteq ℝ$
133	63 132	sstrid	$⊢ (φ \land u \in U) \to U \subseteq ℝ$
134	81	adantr	$⊢ (φ \land u \in U) \to U \neq \emptyset$
135	1 2	jca	$⊢ φ \to (A \in ℝ \land B \in ℝ)$
136	135	adantr	$⊢ (φ \land u \in U) \to (A \in ℝ \land B \in ℝ)$
137	63	a1i	$⊢ (φ \land u \in U) \to U \subseteq [A, B]$
138	65	adantr	$⊢ (φ \land u \in U) \to S \in U$
139		iccsupr	$⊢ ((A \in ℝ \land B \in ℝ) \land U \subseteq [A, B] \land S \in U) \to (U \subseteq ℝ \land U \neq \emptyset \land \exists x \in ℝ \forall y \in U y \leq x)$
140	136 137 138 139	syl3anc	$⊢ (φ \land u \in U) \to (U \subseteq ℝ \land U \neq \emptyset \land \exists x \in ℝ \forall y \in U y \leq x)$
141	140	simp3d	$⊢ (φ \land u \in U) \to \exists x \in ℝ \forall y \in U y \leq x$
142		simpr	$⊢ (φ \land u \in U) \to u \in U$
143		suprub	$⊢ ((U \subseteq ℝ \land U \neq \emptyset \land \exists x \in ℝ \forall y \in U y \leq x) \land u \in U) \to u \leq sup (U ℝ <)$
144	133 134 141 142 143	syl31anc	$⊢ (φ \land u \in U) \to u \leq sup (U ℝ <)$
145	144 9	breqtrrdi	$⊢ (φ \land u \in U) \to u \leq S$
146	145	ralrimiva	$⊢ φ \to \forall u \in U u \leq S$
147	63	sseli	$⊢ u \in U \to u \in [A, B]$
148	147	adantl	$⊢ (φ \land u \in U) \to u \in [A, B]$
149	132 148	sseldd	$⊢ (φ \land u \in U) \to u \in ℝ$
150	67	adantr	$⊢ (φ \land u \in U) \to S \in ℝ$
151	149 150	lenltd	$⊢ (φ \land u \in U) \to (u \leq S \leftrightarrow \neg S < u)$
152	151	ralbidva	$⊢ φ \to (\forall u \in U u \leq S \leftrightarrow \forall u \in U \neg S < u)$
153	146 152	mpbid	$⊢ φ \to \forall u \in U \neg S < u$
154		ralnex	$⊢ \forall u \in U \neg S < u \leftrightarrow \neg \exists u \in U S < u$
155	153 154	sylib	$⊢ φ \to \neg \exists u \in U S < u$
156	155	adantr	$⊢ (φ \land \neg B \leq S) \to \neg \exists u \in U S < u$
157	131 156	condan	$⊢ φ \to B \leq S$
158		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land S \in [A, B]) \to S \leq B$
159	76 60 66 158	syl3anc	$⊢ φ \to S \leq B$
160	60 68 157 159	xrletrid	$⊢ φ \to B = S$
161	160 65	eqeltrd	$⊢ φ \to B \in U$
162	161 8	eleqtrdi	$⊢ φ \to B \in \{z \in [A, B] \| z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))))\}$
163		oveq1	$⊢ z = B \to z - A = B - A$
164		breq2	$⊢ z = B \to (D (j) \leq z \leftrightarrow D (j) \leq B)$
165		id	$⊢ z = B \to z = B$
166	164 165	ifbieq2d	$⊢ z = B \to if (D (j) \leq z, D (j), z) = if (D (j) \leq B, D (j), B)$
167	166	oveq2d	$⊢ z = B \to [C (j), if (D (j) \leq z, D (j), z)) = [C (j), if (D (j) \leq B, D (j), B))$
168	167	fveq2d	$⊢ z = B \to vol ([C (j), if (D (j) \leq z, D (j), z))) = vol ([C (j), if (D (j) \leq B, D (j), B)))$
169	168	mpteq2dv	$⊢ z = B \to (j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))) = (j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))$
170	169	fveq2d	$⊢ z = B \to sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z))))) = sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B)))))$
171	163 170	breq12d	$⊢ z = B \to (z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z))))) \leftrightarrow B - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))))$
172	171	elrab	$⊢ B \in \{z \in [A, B] \| z - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq z, D (j), z)))))\} \leftrightarrow (B \in [A, B] \land B - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))))$
173	162 172	sylib	$⊢ φ \to (B \in [A, B] \land B - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B))))))$
174	173	simprd	$⊢ φ \to B - A \leq sum^((j \in ℕ ⟼ vol ([C (j), if (D (j) \leq B, D (j), B)))))$
175	10 59 7 174 53	letrd	$⊢ φ \to B - A \leq sum^((j \in ℕ ⟼ vol ([C (j), D (j)))))$

Metamath Proof Explorer

Theorem hoidmv1lelem3

Proof