hoidmv1le

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of Fremlin1 p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmv1le.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmv1le.z	$⊢ φ \to Z \in V$
	hoidmv1le.x	$⊢ X = \{Z\}$
	hoidmv1le.a	$⊢ φ \to A : X ⟶ ℝ$
	hoidmv1le.b	$⊢ φ \to B : X ⟶ ℝ$
	hoidmv1le.c	$⊢ φ \to C : ℕ ⟶ ℝ^{X}$
	hoidmv1le.d	$⊢ φ \to D : ℕ ⟶ ℝ^{X}$
	hoidmv1le.s	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
Assertion	hoidmv1le	$⊢ φ \to A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$

Proof

Step	Hyp	Ref	Expression
1		hoidmv1le.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
2		hoidmv1le.z	$⊢ φ \to Z \in V$
3		hoidmv1le.x	$⊢ X = \{Z\}$
4		hoidmv1le.a	$⊢ φ \to A : X ⟶ ℝ$
5		hoidmv1le.b	$⊢ φ \to B : X ⟶ ℝ$
6		hoidmv1le.c	$⊢ φ \to C : ℕ ⟶ ℝ^{X}$
7		hoidmv1le.d	$⊢ φ \to D : ℕ ⟶ ℝ^{X}$
8		hoidmv1le.s	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
9		snidg	$⊢ Z \in V \to Z \in \{Z\}$
10	2 9	syl	$⊢ φ \to Z \in \{Z\}$
11	10 3	eleqtrrdi	$⊢ φ \to Z \in X$
12	5 11	ffvelcdmd	$⊢ φ \to B (Z) \in ℝ$
13	4 11	ffvelcdmd	$⊢ φ \to A (Z) \in ℝ$
14	12 13	resubcld	$⊢ φ \to B (Z) - A (Z) \in ℝ$
15	14	rexrd	$⊢ φ \to B (Z) - A (Z) \in ℝ^{*}$
16		pnfxr	$⊢ +∞ \in ℝ^{*}$
17	16	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
18	14	ltpnfd	$⊢ φ \to B (Z) - A (Z) < +∞$
19	15 17 18	xrltled	$⊢ φ \to B (Z) - A (Z) \leq +∞$
20	19	ad2antrr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to B (Z) - A (Z) \leq +∞$
21		id	$⊢ sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞ \to sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞$
22	21	eqcomd	$⊢ sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞ \to +∞ = sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
23	22	adantl	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to +∞ = sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
24	20 23	breqtrd	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to B (Z) - A (Z) \leq sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
25		simpl	$⊢ ((φ \land A (Z) < B (Z)) \land \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to (φ \land A (Z) < B (Z))$
26		simpr	$⊢ ((φ \land A (Z) < B (Z)) \land \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞$
27		nnex	$⊢ ℕ \in V$
28	27	a1i	$⊢ ((φ \land A (Z) < B (Z)) \land \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to ℕ \in V$
29	3	a1i	$⊢ φ \to X = \{Z\}$
30		snfi	$⊢ \{Z\} \in Fin$
31	30	a1i	$⊢ φ \to \{Z\} \in Fin$
32	29 31	eqeltrd	$⊢ φ \to X \in Fin$
33	32	adantr	$⊢ (φ \land j \in ℕ) \to X \in Fin$
34	11	ne0d	$⊢ φ \to X \neq \emptyset$
35	34	adantr	$⊢ (φ \land j \in ℕ) \to X \neq \emptyset$
36	6	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{X})$
37		elmapi	$⊢ C (j) \in (ℝ^{X}) \to C (j) : X ⟶ ℝ$
38	36 37	syl	$⊢ (φ \land j \in ℕ) \to C (j) : X ⟶ ℝ$
39	7	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{X})$
40		elmapi	$⊢ D (j) \in (ℝ^{X}) \to D (j) : X ⟶ ℝ$
41	39 40	syl	$⊢ (φ \land j \in ℕ) \to D (j) : X ⟶ ℝ$
42	1 33 35 38 41	hoidmvn0val	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) = \prod_{k \in X} vol ([C (j) (k), D (j) (k)))$
43	3	prodeq1i	$⊢ \prod_{k \in X} vol ([C (j) (k), D (j) (k))) = \prod_{k \in \{Z\}} vol ([C (j) (k), D (j) (k)))$
44	43	a1i	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} vol ([C (j) (k), D (j) (k))) = \prod_{k \in \{Z\}} vol ([C (j) (k), D (j) (k)))$
45	2	adantr	$⊢ (φ \land j \in ℕ) \to Z \in V$
46	11	adantr	$⊢ (φ \land j \in ℕ) \to Z \in X$
47	38 46	ffvelcdmd	$⊢ (φ \land j \in ℕ) \to C (j) (Z) \in ℝ$
48	41 46	ffvelcdmd	$⊢ (φ \land j \in ℕ) \to D (j) (Z) \in ℝ$
49		volicore	$⊢ (C (j) (Z) \in ℝ \land D (j) (Z) \in ℝ) \to vol ([C (j) (Z), D (j) (Z))) \in ℝ$
50	47 48 49	syl2anc	$⊢ (φ \land j \in ℕ) \to vol ([C (j) (Z), D (j) (Z))) \in ℝ$
51	50	recnd	$⊢ (φ \land j \in ℕ) \to vol ([C (j) (Z), D (j) (Z))) \in ℂ$
52		fveq2	$⊢ k = Z \to C (j) (k) = C (j) (Z)$
53		fveq2	$⊢ k = Z \to D (j) (k) = D (j) (Z)$
54	52 53	oveq12d	$⊢ k = Z \to [C (j) (k), D (j) (k)) = [C (j) (Z), D (j) (Z))$
55	54	fveq2d	$⊢ k = Z \to vol ([C (j) (k), D (j) (k))) = vol ([C (j) (Z), D (j) (Z)))$
56	55	prodsn	$⊢ (Z \in V \land vol ([C (j) (Z), D (j) (Z))) \in ℂ) \to \prod_{k \in \{Z\}} vol ([C (j) (k), D (j) (k))) = vol ([C (j) (Z), D (j) (Z)))$
57	45 51 56	syl2anc	$⊢ (φ \land j \in ℕ) \to \prod_{k \in \{Z\}} vol ([C (j) (k), D (j) (k))) = vol ([C (j) (Z), D (j) (Z)))$
58	42 44 57	3eqtrd	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) = vol ([C (j) (Z), D (j) (Z)))$
59	58	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ C (j) L (X) D (j)) = (j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))$
60		fveq2	$⊢ k = l \to a (k) = a (l)$
61		fveq2	$⊢ k = l \to b (k) = b (l)$
62	60 61	oveq12d	$⊢ k = l \to [a (k), b (k)) = [a (l), b (l))$
63	62	fveq2d	$⊢ k = l \to vol ([a (k), b (k))) = vol ([a (l), b (l)))$
64	63	cbvprodv	$⊢ \prod_{k \in x} vol ([a (k), b (k))) = \prod_{l \in x} vol ([a (l), b (l)))$
65		ifeq2	$⊢ \prod_{k \in x} vol ([a (k), b (k))) = \prod_{l \in x} vol ([a (l), b (l))) \to if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))) = if (x = \emptyset, 0, \prod_{l \in x} vol ([a (l), b (l))))$
66	64 65	ax-mp	$⊢ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))) = if (x = \emptyset, 0, \prod_{l \in x} vol ([a (l), b (l))))$
67	66	a1i	$⊢ (a \in (ℝ^{x}) \land b \in (ℝ^{x})) \to if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))) = if (x = \emptyset, 0, \prod_{l \in x} vol ([a (l), b (l))))$
68	67	mpoeq3ia	$⊢ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))) = (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{l \in x} vol ([a (l), b (l)))))$
69	68	mpteq2i	$⊢ (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))) = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{l \in x} vol ([a (l), b (l))))))$
70	1 69	eqtri	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{l \in x} vol ([a (l), b (l))))))$
71	70 33 38 41	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) \in [0, +∞)$
72		eqid	$⊢ (j \in ℕ ⟼ C (j) L (X) D (j)) = (j \in ℕ ⟼ C (j) L (X) D (j))$
73	71 72	fmptd	$⊢ φ \to (j \in ℕ ⟼ C (j) L (X) D (j)) : ℕ ⟶ [0, +∞)$
74		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
75	74	a1i	$⊢ φ \to [0, +∞) \subseteq [0, +∞]$
76	73 75	fssd	$⊢ φ \to (j \in ℕ ⟼ C (j) L (X) D (j)) : ℕ ⟶ [0, +∞]$
77	59 76	feq1dd	$⊢ φ \to (j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))) : ℕ ⟶ [0, +∞]$
78	77	ad2antrr	$⊢ ((φ \land A (Z) < B (Z)) \land \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to (j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))) : ℕ ⟶ [0, +∞]$
79	28 78	sge0repnf	$⊢ ((φ \land A (Z) < B (Z)) \land \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to (sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ \leftrightarrow \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞)$
80	26 79	mpbird	$⊢ ((φ \land A (Z) < B (Z)) \land \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ$
81	13	ad2antrr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to A (Z) \in ℝ$
82	12	ad2antrr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to B (Z) \in ℝ$
83		simplr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to A (Z) < B (Z)$
84		eqid	$⊢ (j \in ℕ ⟼ C (j) (Z)) = (j \in ℕ ⟼ C (j) (Z))$
85	47 84	fmptd	$⊢ φ \to (j \in ℕ ⟼ C (j) (Z)) : ℕ ⟶ ℝ$
86	85	ad2antrr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to (j \in ℕ ⟼ C (j) (Z)) : ℕ ⟶ ℝ$
87		eqid	$⊢ (j \in ℕ ⟼ D (j) (Z)) = (j \in ℕ ⟼ D (j) (Z))$
88	48 87	fmptd	$⊢ φ \to (j \in ℕ ⟼ D (j) (Z)) : ℕ ⟶ ℝ$
89	88	ad2antrr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to (j \in ℕ ⟼ D (j) (Z)) : ℕ ⟶ ℝ$
90	3	eleq2i	$⊢ k \in X \leftrightarrow k \in \{Z\}$
91	90	biimpi	$⊢ k \in X \to k \in \{Z\}$
92		elsni	$⊢ k \in \{Z\} \to k = Z$
93	91 92	syl	$⊢ k \in X \to k = Z$
94	93 54	syl	$⊢ k \in X \to [C (j) (k), D (j) (k)) = [C (j) (Z), D (j) (Z))$
95	94	rgen	$⊢ \forall k \in X [C (j) (k), D (j) (k)) = [C (j) (Z), D (j) (Z))$
96		ixpeq2	$⊢ \forall k \in X [C (j) (k), D (j) (k)) = [C (j) (Z), D (j) (Z)) \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
97	95 96	ax-mp	$⊢ \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
98	97	a1i	$⊢ j \in ℕ \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
99	98	iuneq2i	$⊢ ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
100	99	a1i	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
101	8 100	sseqtrd	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
102	101	adantr	$⊢ (φ \land x \in [A (Z), B (Z))) \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
103		id	$⊢ x \in [A (Z), B (Z)) \to x \in [A (Z), B (Z))$
104		eqidd	$⊢ x \in [A (Z), B (Z)) \to \{⟨Z, x⟩\} = \{⟨Z, x⟩\}$
105		opeq2	$⊢ y = x \to ⟨Z, y⟩ = ⟨Z, x⟩$
106	105	sneqd	$⊢ y = x \to \{⟨Z, y⟩\} = \{⟨Z, x⟩\}$
107	106	rspceeqv	$⊢ (x \in [A (Z), B (Z)) \land \{⟨Z, x⟩\} = \{⟨Z, x⟩\}) \to \exists y \in [A (Z), B (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\}$
108	103 104 107	syl2anc	$⊢ x \in [A (Z), B (Z)) \to \exists y \in [A (Z), B (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\}$
109	108	adantl	$⊢ (φ \land x \in [A (Z), B (Z))) \to \exists y \in [A (Z), B (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\}$
110		elixpsn	$⊢ Z \in V \to (\{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) \leftrightarrow \exists y \in [A (Z), B (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\})$
111	2 110	syl	$⊢ φ \to (\{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) \leftrightarrow \exists y \in [A (Z), B (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\})$
112	111	adantr	$⊢ (φ \land x \in [A (Z), B (Z))) \to (\{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) \leftrightarrow \exists y \in [A (Z), B (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\})$
113	109 112	mpbird	$⊢ (φ \land x \in [A (Z), B (Z))) \to \{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [A (Z), B (Z))$
114	3	eqcomi	$⊢ \{Z\} = X$
115		ixpeq1	$⊢ \{Z\} = X \to \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) = \underset{k \in X}{⨉} [A (Z), B (Z))$
116	114 115	ax-mp	$⊢ \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) = \underset{k \in X}{⨉} [A (Z), B (Z))$
117		fveq2	$⊢ k = Z \to A (k) = A (Z)$
118	93 117	syl	$⊢ k \in X \to A (k) = A (Z)$
119		fveq2	$⊢ k = Z \to B (k) = B (Z)$
120	93 119	syl	$⊢ k \in X \to B (k) = B (Z)$
121	118 120	oveq12d	$⊢ k \in X \to [A (k), B (k)) = [A (Z), B (Z))$
122	121	eqcomd	$⊢ k \in X \to [A (Z), B (Z)) = [A (k), B (k))$
123	122	rgen	$⊢ \forall k \in X [A (Z), B (Z)) = [A (k), B (k))$
124		ixpeq2	$⊢ \forall k \in X [A (Z), B (Z)) = [A (k), B (k)) \to \underset{k \in X}{⨉} [A (Z), B (Z)) = \underset{k \in X}{⨉} [A (k), B (k))$
125	123 124	ax-mp	$⊢ \underset{k \in X}{⨉} [A (Z), B (Z)) = \underset{k \in X}{⨉} [A (k), B (k))$
126	116 125	eqtri	$⊢ \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) = \underset{k \in X}{⨉} [A (k), B (k))$
127	126	a1i	$⊢ φ \to \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) = \underset{k \in X}{⨉} [A (k), B (k))$
128	127	adantr	$⊢ (φ \land x \in [A (Z), B (Z))) \to \underset{k \in \{Z\}}{⨉} [A (Z), B (Z)) = \underset{k \in X}{⨉} [A (k), B (k))$
129	113 128	eleqtrd	$⊢ (φ \land x \in [A (Z), B (Z))) \to \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [A (k), B (k))$
130	102 129	sseldd	$⊢ (φ \land x \in [A (Z), B (Z))) \to \{⟨Z, x⟩\} \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
131		eliun	$⊢ \{⟨Z, x⟩\} \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z)) \leftrightarrow \exists j \in ℕ \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
132	130 131	sylib	$⊢ (φ \land x \in [A (Z), B (Z))) \to \exists j \in ℕ \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))$
133		ixpeq1	$⊢ X = \{Z\} \to \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z)) = \underset{k \in \{Z\}}{⨉} [C (j) (Z), D (j) (Z))$
134	3 133	ax-mp	$⊢ \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z)) = \underset{k \in \{Z\}}{⨉} [C (j) (Z), D (j) (Z))$
135	134	eleq2i	$⊢ \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z)) \leftrightarrow \{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [C (j) (Z), D (j) (Z))$
136	135	bilani	$⊢ (φ \land \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))) \to \{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [C (j) (Z), D (j) (Z))$
137		elixpsn	$⊢ Z \in V \to (\{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [C (j) (Z), D (j) (Z)) \leftrightarrow \exists y \in [C (j) (Z), D (j) (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\})$
138	2 137	syl	$⊢ φ \to (\{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [C (j) (Z), D (j) (Z)) \leftrightarrow \exists y \in [C (j) (Z), D (j) (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\})$
139	138	adantr	$⊢ (φ \land \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))) \to (\{⟨Z, x⟩\} \in \underset{k \in \{Z\}}{⨉} [C (j) (Z), D (j) (Z)) \leftrightarrow \exists y \in [C (j) (Z), D (j) (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\})$
140	136 139	mpbid	$⊢ (φ \land \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))) \to \exists y \in [C (j) (Z), D (j) (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\}$
141		opex	$⊢ ⟨Z, x⟩ \in V$
142	141	sneqr	$⊢ \{⟨Z, x⟩\} = \{⟨Z, y⟩\} \to ⟨Z, x⟩ = ⟨Z, y⟩$
143	142	adantl	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to ⟨Z, x⟩ = ⟨Z, y⟩$
144		vex	$⊢ x \in V$
145	144	a1i	$⊢ φ \to x \in V$
146		opthg	$⊢ (Z \in V \land x \in V) \to (⟨Z, x⟩ = ⟨Z, y⟩ \leftrightarrow (Z = Z \land x = y))$
147	2 145 146	syl2anc	$⊢ φ \to (⟨Z, x⟩ = ⟨Z, y⟩ \leftrightarrow (Z = Z \land x = y))$
148	147	adantr	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to (⟨Z, x⟩ = ⟨Z, y⟩ \leftrightarrow (Z = Z \land x = y))$
149	143 148	mpbid	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to (Z = Z \land x = y)$
150	149	simprd	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to x = y$
151	150	3adant2	$⊢ (φ \land y \in [C (j) (Z), D (j) (Z)) \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to x = y$
152		simp2	$⊢ (φ \land y \in [C (j) (Z), D (j) (Z)) \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to y \in [C (j) (Z), D (j) (Z))$
153	151 152	eqeltrd	$⊢ (φ \land y \in [C (j) (Z), D (j) (Z)) \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to x \in [C (j) (Z), D (j) (Z))$
154	153	3exp	$⊢ φ \to (y \in [C (j) (Z), D (j) (Z)) \to (\{⟨Z, x⟩\} = \{⟨Z, y⟩\} \to x \in [C (j) (Z), D (j) (Z))))$
155	154	adantr	$⊢ (φ \land \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))) \to (y \in [C (j) (Z), D (j) (Z)) \to (\{⟨Z, x⟩\} = \{⟨Z, y⟩\} \to x \in [C (j) (Z), D (j) (Z))))$
156	155	rexlimdv	$⊢ (φ \land \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))) \to (\exists y \in [C (j) (Z), D (j) (Z)) \{⟨Z, x⟩\} = \{⟨Z, y⟩\} \to x \in [C (j) (Z), D (j) (Z)))$
157	140 156	mpd	$⊢ (φ \land \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))) \to x \in [C (j) (Z), D (j) (Z))$
158	157	ex	$⊢ φ \to (\{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z)) \to x \in [C (j) (Z), D (j) (Z)))$
159	158	ad2antrr	$⊢ ((φ \land x \in [A (Z), B (Z))) \land j \in ℕ) \to (\{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z)) \to x \in [C (j) (Z), D (j) (Z)))$
160	159	reximdva	$⊢ (φ \land x \in [A (Z), B (Z))) \to (\exists j \in ℕ \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z)) \to \exists j \in ℕ x \in [C (j) (Z), D (j) (Z)))$
161	132 160	mpd	$⊢ (φ \land x \in [A (Z), B (Z))) \to \exists j \in ℕ x \in [C (j) (Z), D (j) (Z))$
162		eliun	$⊢ x \in ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z)) \leftrightarrow \exists j \in ℕ x \in [C (j) (Z), D (j) (Z))$
163	161 162	sylibr	$⊢ (φ \land x \in [A (Z), B (Z))) \to x \in ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
164	163	ralrimiva	$⊢ φ \to \forall x \in [A (Z), B (Z)) x \in ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
165		dfss3	$⊢ [A (Z), B (Z)) \subseteq ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z)) \leftrightarrow \forall x \in [A (Z), B (Z)) x \in ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
166	164 165	sylibr	$⊢ φ \to [A (Z), B (Z)) \subseteq ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
167		eqidd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ C (j) (Z)) = (j \in ℕ ⟼ C (j) (Z))$
168		fveq2	$⊢ j = i \to C (j) = C (i)$
169	168	fveq1d	$⊢ j = i \to C (j) (Z) = C (i) (Z)$
170	169	adantl	$⊢ ((φ \land i \in ℕ) \land j = i) \to C (j) (Z) = C (i) (Z)$
171		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
172		fvexd	$⊢ (φ \land i \in ℕ) \to C (i) (Z) \in V$
173	167 170 171 172	fvmptd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ C (j) (Z)) (i) = C (i) (Z)$
174		eqidd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ D (j) (Z)) = (j \in ℕ ⟼ D (j) (Z))$
175		fveq2	$⊢ j = i \to D (j) = D (i)$
176	175	fveq1d	$⊢ j = i \to D (j) (Z) = D (i) (Z)$
177	176	adantl	$⊢ ((φ \land i \in ℕ) \land j = i) \to D (j) (Z) = D (i) (Z)$
178		fvexd	$⊢ (φ \land i \in ℕ) \to D (i) (Z) \in V$
179	174 177 171 178	fvmptd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ D (j) (Z)) (i) = D (i) (Z)$
180	173 179	oveq12d	$⊢ (φ \land i \in ℕ) \to [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)) = [C (i) (Z), D (i) (Z))$
181	180	iuneq2dv	$⊢ φ \to ⋃_{i \in ℕ} [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)) = ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z))$
182	169 176	oveq12d	$⊢ j = i \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))$
183	182	cbviunv	$⊢ ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z)) = ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z))$
184	183	eqcomi	$⊢ ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z)) = ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
185	184	a1i	$⊢ φ \to ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z)) = ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
186	181 185	eqtr2d	$⊢ φ \to ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z)) = ⋃_{i \in ℕ} [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))$
187	166 186	sseqtrd	$⊢ φ \to [A (Z), B (Z)) \subseteq ⋃_{i \in ℕ} [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))$
188	187	ad2antrr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to [A (Z), B (Z)) \subseteq ⋃_{i \in ℕ} [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))$
189		fvex	$⊢ C (i) (Z) \in V$
190	169 84 189	fvmpt	$⊢ i \in ℕ \to (j \in ℕ ⟼ C (j) (Z)) (i) = C (i) (Z)$
191		fvex	$⊢ D (i) (Z) \in V$
192	176 87 191	fvmpt	$⊢ i \in ℕ \to (j \in ℕ ⟼ D (j) (Z)) (i) = D (i) (Z)$
193	190 192	oveq12d	$⊢ i \in ℕ \to [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)) = [C (i) (Z), D (i) (Z))$
194	193	fveq2d	$⊢ i \in ℕ \to vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))) = vol ([C (i) (Z), D (i) (Z)))$
195	194	mpteq2ia	$⊢ (i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)))) = (i \in ℕ ⟼ vol ([C (i) (Z), D (i) (Z))))$
196		eqcom	$⊢ j = i \leftrightarrow i = j$
197	196	imbi1i	$⊢ (j = i \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))) \leftrightarrow (i = j \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z)))$
198		eqcom	$⊢ [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z)) \leftrightarrow [C (i) (Z), D (i) (Z)) = [C (j) (Z), D (j) (Z))$
199	198	imbi2i	$⊢ (i = j \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))) \leftrightarrow (i = j \to [C (i) (Z), D (i) (Z)) = [C (j) (Z), D (j) (Z)))$
200	197 199	bitri	$⊢ (j = i \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))) \leftrightarrow (i = j \to [C (i) (Z), D (i) (Z)) = [C (j) (Z), D (j) (Z)))$
201	182 200	mpbi	$⊢ i = j \to [C (i) (Z), D (i) (Z)) = [C (j) (Z), D (j) (Z))$
202	201	fveq2d	$⊢ i = j \to vol ([C (i) (Z), D (i) (Z))) = vol ([C (j) (Z), D (j) (Z)))$
203	202	cbvmptv	$⊢ (i \in ℕ ⟼ vol ([C (i) (Z), D (i) (Z)))) = (j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))$
204	195 203	eqtri	$⊢ (i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)))) = (j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))$
205	204	fveq2i	$⊢ sum^((i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))))) = sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
206	205	a1i	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to sum^((i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))))) = sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
207		simpr	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ$
208	206 207	eqeltrd	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to sum^((i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))))) \in ℝ$
209		oveq1	$⊢ w = z \to w - A (Z) = z - A (Z)$
210	192	breq1d	$⊢ i \in ℕ \to ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z \leftrightarrow D (i) (Z) \leq z)$
211	210 192	ifbieq1d	$⊢ i \in ℕ \to if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z) = if (D (i) (Z) \leq z, D (i) (Z), z)$
212	190 211	oveq12d	$⊢ i \in ℕ \to [(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z)) = [C (i) (Z), if (D (i) (Z) \leq z, D (i) (Z), z))$
213	212	fveq2d	$⊢ i \in ℕ \to vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z))) = vol ([C (i) (Z), if (D (i) (Z) \leq z, D (i) (Z), z)))$
214	213	mpteq2ia	$⊢ (i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z)))) = (i \in ℕ ⟼ vol ([C (i) (Z), if (D (i) (Z) \leq z, D (i) (Z), z))))$
215		fveq2	$⊢ i = h \to C (i) = C (h)$
216	215	fveq1d	$⊢ i = h \to C (i) (Z) = C (h) (Z)$
217		fveq2	$⊢ i = h \to D (i) = D (h)$
218	217	fveq1d	$⊢ i = h \to D (i) (Z) = D (h) (Z)$
219	218	breq1d	$⊢ i = h \to (D (i) (Z) \leq z \leftrightarrow D (h) (Z) \leq z)$
220	219 218	ifbieq1d	$⊢ i = h \to if (D (i) (Z) \leq z, D (i) (Z), z) = if (D (h) (Z) \leq z, D (h) (Z), z)$
221	216 220	oveq12d	$⊢ i = h \to [C (i) (Z), if (D (i) (Z) \leq z, D (i) (Z), z)) = [C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z))$
222	221	fveq2d	$⊢ i = h \to vol ([C (i) (Z), if (D (i) (Z) \leq z, D (i) (Z), z))) = vol ([C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z)))$
223	222	cbvmptv	$⊢ (i \in ℕ ⟼ vol ([C (i) (Z), if (D (i) (Z) \leq z, D (i) (Z), z)))) = (h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z))))$
224	214 223	eqtri	$⊢ (i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z)))) = (h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z))))$
225	224	a1i	$⊢ w = z \to (i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z)))) = (h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z))))$
226		breq2	$⊢ w = z \to (D (h) (Z) \leq w \leftrightarrow D (h) (Z) \leq z)$
227		id	$⊢ w = z \to w = z$
228	226 227	ifbieq2d	$⊢ w = z \to if (D (h) (Z) \leq w, D (h) (Z), w) = if (D (h) (Z) \leq z, D (h) (Z), z)$
229	228	eqcomd	$⊢ w = z \to if (D (h) (Z) \leq z, D (h) (Z), z) = if (D (h) (Z) \leq w, D (h) (Z), w)$
230	229	oveq2d	$⊢ w = z \to [C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z)) = [C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w))$
231	230	fveq2d	$⊢ w = z \to vol ([C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z))) = vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w)))$
232	231	mpteq2dv	$⊢ w = z \to (h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq z, D (h) (Z), z)))) = (h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w))))$
233	225 232	eqtr2d	$⊢ w = z \to (h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w)))) = (i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z))))$
234	233	fveq2d	$⊢ w = z \to sum^((h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w))))) = sum^((i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z)))))$
235	209 234	breq12d	$⊢ w = z \to (w - A (Z) \leq sum^((h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w))))) \leftrightarrow z - A (Z) \leq sum^((i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z))))))$
236	235	cbvrabv	$⊢ \{w \in [A (Z), B (Z)] \| w - A (Z) \leq sum^((h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w)))))\} = \{z \in [A (Z), B (Z)] \| z - A (Z) \leq sum^((i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), if ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z, (j \in ℕ ⟼ D (j) (Z)) (i), z)))))\}$
237		eqid	$⊢ sup (\{w \in [A (Z), B (Z)] \| w - A (Z) \leq sum^((h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w)))))\} ℝ <) = sup (\{w \in [A (Z), B (Z)] \| w - A (Z) \leq sum^((h \in ℕ ⟼ vol ([C (h) (Z), if (D (h) (Z) \leq w, D (h) (Z), w)))))\} ℝ <)$
238	81 82 83 86 89 188 208 236 237	hoidmv1lelem3	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to B (Z) - A (Z) \leq sum^((i \in ℕ ⟼ vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)))))$
239	238 206	breqtrd	$⊢ ((φ \land A (Z) < B (Z)) \land sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) \in ℝ) \to B (Z) - A (Z) \leq sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
240	25 80 239	syl2anc	$⊢ ((φ \land A (Z) < B (Z)) \land \neg sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))) = +∞) \to B (Z) - A (Z) \leq sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
241	24 240	pm2.61dan	$⊢ (φ \land A (Z) < B (Z)) \to B (Z) - A (Z) \leq sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
242	1 32 34 4 5	hoidmvn0val	$⊢ φ \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
243	29	prodeq1d	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in \{Z\}} vol ([A (k), B (k)))$
244		volicore	$⊢ (A (Z) \in ℝ \land B (Z) \in ℝ) \to vol ([A (Z), B (Z))) \in ℝ$
245	13 12 244	syl2anc	$⊢ φ \to vol ([A (Z), B (Z))) \in ℝ$
246	245	recnd	$⊢ φ \to vol ([A (Z), B (Z))) \in ℂ$
247	117 119	oveq12d	$⊢ k = Z \to [A (k), B (k)) = [A (Z), B (Z))$
248	247	fveq2d	$⊢ k = Z \to vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
249	248	prodsn	$⊢ (Z \in V \land vol ([A (Z), B (Z))) \in ℂ) \to \prod_{k \in \{Z\}} vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
250	2 246 249	syl2anc	$⊢ φ \to \prod_{k \in \{Z\}} vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
251	242 243 250	3eqtrd	$⊢ φ \to A L (X) B = vol ([A (Z), B (Z)))$
252	251	adantr	$⊢ (φ \land A (Z) < B (Z)) \to A L (X) B = vol ([A (Z), B (Z)))$
253		volico	$⊢ (A (Z) \in ℝ \land B (Z) \in ℝ) \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
254	13 12 253	syl2anc	$⊢ φ \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
255	254	adantr	$⊢ (φ \land A (Z) < B (Z)) \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
256		iftrue	$⊢ A (Z) < B (Z) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = B (Z) - A (Z)$
257	256	adantl	$⊢ (φ \land A (Z) < B (Z)) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = B (Z) - A (Z)$
258	252 255 257	3eqtrd	$⊢ (φ \land A (Z) < B (Z)) \to A L (X) B = B (Z) - A (Z)$
259	59	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
260	259	adantr	$⊢ (φ \land A (Z) < B (Z)) \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
261	258 260	breq12d	$⊢ (φ \land A (Z) < B (Z)) \to (A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \leftrightarrow B (Z) - A (Z) \leq sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))))$
262	241 261	mpbird	$⊢ (φ \land A (Z) < B (Z)) \to A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
263	242	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
264	243	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in \{Z\}} vol ([A (k), B (k)))$
265	250	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to \prod_{k \in \{Z\}} vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
266	254	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
267		iffalse	$⊢ \neg A (Z) < B (Z) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = 0$
268	267	adantl	$⊢ (φ \land \neg A (Z) < B (Z)) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = 0$
269	265 266 268	3eqtrd	$⊢ (φ \land \neg A (Z) < B (Z)) \to \prod_{k \in \{Z\}} vol ([A (k), B (k))) = 0$
270	263 264 269	3eqtrd	$⊢ (φ \land \neg A (Z) < B (Z)) \to A L (X) B = 0$
271	27	a1i	$⊢ φ \to ℕ \in V$
272	271 76	sge0ge0	$⊢ φ \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
273	272	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
274	270 273	eqbrtrd	$⊢ (φ \land \neg A (Z) < B (Z)) \to A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
275	262 274	pm2.61dan	$⊢ φ \to A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$

Metamath Proof Explorer

Theorem hoidmv1le

Proof