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	biimpi	$⊢ \{⟨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	136	adantl	$⊢ (φ \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))$
138		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⟩\})$
139	2 138	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⟩\})$
140	139	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⟩\})$
141	137 140	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⟩\}$
142		opex	$⊢ ⟨Z, x⟩ \in V$
143	142	sneqr	$⊢ \{⟨Z, x⟩\} = \{⟨Z, y⟩\} \to ⟨Z, x⟩ = ⟨Z, y⟩$
144	143	adantl	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to ⟨Z, x⟩ = ⟨Z, y⟩$
145		vex	$⊢ x \in V$
146	145	a1i	$⊢ φ \to x \in V$
147		opthg	$⊢ (Z \in V \land x \in V) \to (⟨Z, x⟩ = ⟨Z, y⟩ \leftrightarrow (Z = Z \land x = y))$
148	2 146 147	syl2anc	$⊢ φ \to (⟨Z, x⟩ = ⟨Z, y⟩ \leftrightarrow (Z = Z \land x = y))$
149	148	adantr	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to (⟨Z, x⟩ = ⟨Z, y⟩ \leftrightarrow (Z = Z \land x = y))$
150	144 149	mpbid	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to (Z = Z \land x = y)$
151	150	simprd	$⊢ (φ \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to x = y$
152	151	3adant2	$⊢ (φ \land y \in [C (j) (Z), D (j) (Z)) \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to x = y$
153		simp2	$⊢ (φ \land y \in [C (j) (Z), D (j) (Z)) \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to y \in [C (j) (Z), D (j) (Z))$
154	152 153	eqeltrd	$⊢ (φ \land y \in [C (j) (Z), D (j) (Z)) \land \{⟨Z, x⟩\} = \{⟨Z, y⟩\}) \to x \in [C (j) (Z), D (j) (Z))$
155	154	3exp	$⊢ φ \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	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))))$
157	156	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)))$
158	141 157	mpd	$⊢ (φ \land \{⟨Z, x⟩\} \in \underset{k \in X}{⨉} [C (j) (Z), D (j) (Z))) \to x \in [C (j) (Z), D (j) (Z))$
159	158	ex	$⊢ φ \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	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)))$
161	160	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)))$
162	132 161	mpd	$⊢ (φ \land x \in [A (Z), B (Z))) \to \exists j \in ℕ x \in [C (j) (Z), D (j) (Z))$
163		eliun	$⊢ x \in ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z)) \leftrightarrow \exists j \in ℕ x \in [C (j) (Z), D (j) (Z))$
164	162 163	sylibr	$⊢ (φ \land x \in [A (Z), B (Z))) \to x \in ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
165	164	ralrimiva	$⊢ φ \to \forall x \in [A (Z), B (Z)) x \in ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
166		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))$
167	165 166	sylibr	$⊢ φ \to [A (Z), B (Z)) \subseteq ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
168		eqidd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ C (j) (Z)) = (j \in ℕ ⟼ C (j) (Z))$
169		fveq2	$⊢ j = i \to C (j) = C (i)$
170	169	fveq1d	$⊢ j = i \to C (j) (Z) = C (i) (Z)$
171	170	adantl	$⊢ ((φ \land i \in ℕ) \land j = i) \to C (j) (Z) = C (i) (Z)$
172		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
173		fvexd	$⊢ (φ \land i \in ℕ) \to C (i) (Z) \in V$
174	168 171 172 173	fvmptd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ C (j) (Z)) (i) = C (i) (Z)$
175		eqidd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ D (j) (Z)) = (j \in ℕ ⟼ D (j) (Z))$
176		fveq2	$⊢ j = i \to D (j) = D (i)$
177	176	fveq1d	$⊢ j = i \to D (j) (Z) = D (i) (Z)$
178	177	adantl	$⊢ ((φ \land i \in ℕ) \land j = i) \to D (j) (Z) = D (i) (Z)$
179		fvexd	$⊢ (φ \land i \in ℕ) \to D (i) (Z) \in V$
180	175 178 172 179	fvmptd	$⊢ (φ \land i \in ℕ) \to (j \in ℕ ⟼ D (j) (Z)) (i) = D (i) (Z)$
181	174 180	oveq12d	$⊢ (φ \land i \in ℕ) \to [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)) = [C (i) (Z), D (i) (Z))$
182	181	iuneq2dv	$⊢ φ \to ⋃_{i \in ℕ} [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)) = ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z))$
183	170 177	oveq12d	$⊢ j = i \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))$
184	183	cbviunv	$⊢ ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z)) = ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z))$
185	184	eqcomi	$⊢ ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z)) = ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
186	185	a1i	$⊢ φ \to ⋃_{i \in ℕ} [C (i) (Z), D (i) (Z)) = ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z))$
187	182 186	eqtr2d	$⊢ φ \to ⋃_{j \in ℕ} [C (j) (Z), D (j) (Z)) = ⋃_{i \in ℕ} [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))$
188	167 187	sseqtrd	$⊢ φ \to [A (Z), B (Z)) \subseteq ⋃_{i \in ℕ} [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))$
189	188	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))$
190		fvex	$⊢ C (i) (Z) \in V$
191	170 84 190	fvmpt	$⊢ i \in ℕ \to (j \in ℕ ⟼ C (j) (Z)) (i) = C (i) (Z)$
192		fvex	$⊢ D (i) (Z) \in V$
193	177 87 192	fvmpt	$⊢ i \in ℕ \to (j \in ℕ ⟼ D (j) (Z)) (i) = D (i) (Z)$
194	191 193	oveq12d	$⊢ i \in ℕ \to [(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i)) = [C (i) (Z), D (i) (Z))$
195	194	fveq2d	$⊢ i \in ℕ \to vol ([(j \in ℕ ⟼ C (j) (Z)) (i), (j \in ℕ ⟼ D (j) (Z)) (i))) = vol ([C (i) (Z), D (i) (Z)))$
196	195	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))))$
197		eqcom	$⊢ j = i \leftrightarrow i = j$
198	197	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)))$
199		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))$
200	199	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)))$
201	198 200	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)))$
202	183 201	mpbi	$⊢ i = j \to [C (i) (Z), D (i) (Z)) = [C (j) (Z), D (j) (Z))$
203	202	fveq2d	$⊢ i = j \to vol ([C (i) (Z), D (i) (Z))) = vol ([C (j) (Z), D (j) (Z)))$
204	203	cbvmptv	$⊢ (i \in ℕ ⟼ vol ([C (i) (Z), D (i) (Z)))) = (j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z))))$
205	196 204	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))))$
206	205	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)))))$
207	206	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)))))$
208		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 ℝ$
209	207 208	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 ℝ$
210		oveq1	$⊢ w = z \to w - A (Z) = z - A (Z)$
211	193	breq1d	$⊢ i \in ℕ \to ((j \in ℕ ⟼ D (j) (Z)) (i) \leq z \leftrightarrow D (i) (Z) \leq z)$
212	211 193	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)$
213	191 212	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))$
214	213	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)))$
215	214	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))))$
216		fveq2	$⊢ i = h \to C (i) = C (h)$
217	216	fveq1d	$⊢ i = h \to C (i) (Z) = C (h) (Z)$
218		fveq2	$⊢ i = h \to D (i) = D (h)$
219	218	fveq1d	$⊢ i = h \to D (i) (Z) = D (h) (Z)$
220	219	breq1d	$⊢ i = h \to (D (i) (Z) \leq z \leftrightarrow D (h) (Z) \leq z)$
221	220 219	ifbieq1d	$⊢ i = h \to if (D (i) (Z) \leq z, D (i) (Z), z) = if (D (h) (Z) \leq z, D (h) (Z), z)$
222	217 221	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))$
223	222	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)))$
224	223	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))))$
225	215 224	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))))$
226	225	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))))$
227		breq2	$⊢ w = z \to (D (h) (Z) \leq w \leftrightarrow D (h) (Z) \leq z)$
228		id	$⊢ w = z \to w = z$
229	227 228	ifbieq2d	$⊢ w = z \to if (D (h) (Z) \leq w, D (h) (Z), w) = if (D (h) (Z) \leq z, D (h) (Z), z)$
230	229	eqcomd	$⊢ w = z \to if (D (h) (Z) \leq z, D (h) (Z), z) = if (D (h) (Z) \leq w, D (h) (Z), w)$
231	230	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))$
232	231	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)))$
233	232	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))))$
234	226 233	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))))$
235	234	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)))))$
236	210 235	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))))))$
237	236	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)))))\}$
238		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)))))\} ℝ <)$
239	81 82 83 86 89 189 209 237 238	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)))))$
240	239 207	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)))))$
241	25 80 240	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)))))$
242	24 241	pm2.61dan	$⊢ (φ \land A (Z) < B (Z)) \to B (Z) - A (Z) \leq sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
243	1 32 34 4 5	hoidmvn0val	$⊢ φ \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
244	29	prodeq1d	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in \{Z\}} vol ([A (k), B (k)))$
245		volicore	$⊢ (A (Z) \in ℝ \land B (Z) \in ℝ) \to vol ([A (Z), B (Z))) \in ℝ$
246	13 12 245	syl2anc	$⊢ φ \to vol ([A (Z), B (Z))) \in ℝ$
247	246	recnd	$⊢ φ \to vol ([A (Z), B (Z))) \in ℂ$
248	117 119	oveq12d	$⊢ k = Z \to [A (k), B (k)) = [A (Z), B (Z))$
249	248	fveq2d	$⊢ k = Z \to vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
250	249	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)))$
251	2 247 250	syl2anc	$⊢ φ \to \prod_{k \in \{Z\}} vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
252	243 244 251	3eqtrd	$⊢ φ \to A L (X) B = vol ([A (Z), B (Z)))$
253	252	adantr	$⊢ (φ \land A (Z) < B (Z)) \to A L (X) B = vol ([A (Z), B (Z)))$
254		volico	$⊢ (A (Z) \in ℝ \land B (Z) \in ℝ) \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
255	13 12 254	syl2anc	$⊢ φ \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
256	255	adantr	$⊢ (φ \land A (Z) < B (Z)) \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
257		iftrue	$⊢ A (Z) < B (Z) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = B (Z) - A (Z)$
258	257	adantl	$⊢ (φ \land A (Z) < B (Z)) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = B (Z) - A (Z)$
259	253 256 258	3eqtrd	$⊢ (φ \land A (Z) < B (Z)) \to A L (X) B = B (Z) - A (Z)$
260	59	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ vol ([C (j) (Z), D (j) (Z)))))$
261	260	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)))))$
262	259 261	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))))))$
263	242 262	mpbird	$⊢ (φ \land A (Z) < B (Z)) \to A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
264	243	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
265	244	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)))$
266	251	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to \prod_{k \in \{Z\}} vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
267	255	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to vol ([A (Z), B (Z))) = if (A (Z) < B (Z), B (Z) - A (Z), 0)$
268		iffalse	$⊢ \neg A (Z) < B (Z) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = 0$
269	268	adantl	$⊢ (φ \land \neg A (Z) < B (Z)) \to if (A (Z) < B (Z), B (Z) - A (Z), 0) = 0$
270	266 267 269	3eqtrd	$⊢ (φ \land \neg A (Z) < B (Z)) \to \prod_{k \in \{Z\}} vol ([A (k), B (k))) = 0$
271	264 265 270	3eqtrd	$⊢ (φ \land \neg A (Z) < B (Z)) \to A L (X) B = 0$
272	27	a1i	$⊢ φ \to ℕ \in V$
273	272 76	sge0ge0	$⊢ φ \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
274	273	adantr	$⊢ (φ \land \neg A (Z) < B (Z)) \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
275	271 274	eqbrtrd	$⊢ (φ \land \neg A (Z) < B (Z)) \to A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
276	263 275	pm2.61dan	$⊢ φ \to A L (X) B \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$

Metamath Proof Explorer

Theorem hoidmv1le

Proof