vonicc

Description: The n-dimensional Lebesgue measure of a closed interval. This is the second statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonicc.x	$⊢ φ \to X \in Fin$
	vonicc.a	$⊢ φ \to A : X ⟶ ℝ$
	vonicc.b	$⊢ φ \to B : X ⟶ ℝ$
	vonicc.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k)]$
	vonicc.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
Assertion	vonicc	$⊢ φ \to voln (X) (I) = A L (X) B$

Proof

Step	Hyp	Ref	Expression
1		vonicc.x	$⊢ φ \to X \in Fin$
2		vonicc.a	$⊢ φ \to A : X ⟶ ℝ$
3		vonicc.b	$⊢ φ \to B : X ⟶ ℝ$
4		vonicc.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k)]$
5		vonicc.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
6	2	adantr	$⊢ (φ \land X = \emptyset) \to A : X ⟶ ℝ$
7		feq2	$⊢ X = \emptyset \to (A : X ⟶ ℝ \leftrightarrow A : \emptyset ⟶ ℝ)$
8	7	adantl	$⊢ (φ \land X = \emptyset) \to (A : X ⟶ ℝ \leftrightarrow A : \emptyset ⟶ ℝ)$
9	6 8	mpbid	$⊢ (φ \land X = \emptyset) \to A : \emptyset ⟶ ℝ$
10	3	adantr	$⊢ (φ \land X = \emptyset) \to B : X ⟶ ℝ$
11		feq2	$⊢ X = \emptyset \to (B : X ⟶ ℝ \leftrightarrow B : \emptyset ⟶ ℝ)$
12	11	adantl	$⊢ (φ \land X = \emptyset) \to (B : X ⟶ ℝ \leftrightarrow B : \emptyset ⟶ ℝ)$
13	10 12	mpbid	$⊢ (φ \land X = \emptyset) \to B : \emptyset ⟶ ℝ$
14	5 9 13	hoidmv0val	$⊢ (φ \land X = \emptyset) \to A L (\emptyset) B = 0$
15	14	eqcomd	$⊢ (φ \land X = \emptyset) \to 0 = A L (\emptyset) B$
16		fveq2	$⊢ X = \emptyset \to voln (X) = voln (\emptyset)$
17	4	a1i	$⊢ X = \emptyset \to I = \underset{k \in X}{⨉} [A (k), B (k)]$
18		ixpeq1	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [A (k), B (k)] = \underset{k \in \emptyset}{⨉} [A (k), B (k)]$
19	17 18	eqtrd	$⊢ X = \emptyset \to I = \underset{k \in \emptyset}{⨉} [A (k), B (k)]$
20	16 19	fveq12d	$⊢ X = \emptyset \to voln (X) (I) = voln (\emptyset) (\underset{k \in \emptyset}{⨉} [A (k), B (k)])$
21	20	adantl	$⊢ (φ \land X = \emptyset) \to voln (X) (I) = voln (\emptyset) (\underset{k \in \emptyset}{⨉} [A (k), B (k)])$
22		0fi	$⊢ \emptyset \in Fin$
23	22	a1i	$⊢ (φ \land X = \emptyset) \to \emptyset \in Fin$
24		eqid	$⊢ dom voln (\emptyset) = dom voln (\emptyset)$
25	23 24 9 13	iccvonmbl	$⊢ (φ \land X = \emptyset) \to \underset{k \in \emptyset}{⨉} [A (k), B (k)] \in dom voln (\emptyset)$
26	25	von0val	$⊢ (φ \land X = \emptyset) \to voln (\emptyset) (\underset{k \in \emptyset}{⨉} [A (k), B (k)]) = 0$
27	21 26	eqtrd	$⊢ (φ \land X = \emptyset) \to voln (X) (I) = 0$
28		fveq2	$⊢ X = \emptyset \to L (X) = L (\emptyset)$
29	28	oveqd	$⊢ X = \emptyset \to A L (X) B = A L (\emptyset) B$
30	29	adantl	$⊢ (φ \land X = \emptyset) \to A L (X) B = A L (\emptyset) B$
31	15 27 30	3eqtr4d	$⊢ (φ \land X = \emptyset) \to voln (X) (I) = A L (X) B$
32		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
33	32	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
34		nfv	$⊢ Ⅎ k (φ \land X \neq \emptyset)$
35		nfra1	$⊢ Ⅎ k \forall k \in X A (k) \leq B (k)$
36	34 35	nfan	$⊢ Ⅎ k ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k))$
37	2	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
38	3	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
39		volico2	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) = if (A (k) \leq B (k), B (k) - A (k), 0)$
40	37 38 39	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) = if (A (k) \leq B (k), B (k) - A (k), 0)$
41	40	ad4ant14	$⊢ (((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \land k \in X) \to vol ([A (k), B (k))) = if (A (k) \leq B (k), B (k) - A (k), 0)$
42		rspa	$⊢ (\forall k \in X A (k) \leq B (k) \land k \in X) \to A (k) \leq B (k)$
43	42	iftrued	$⊢ (\forall k \in X A (k) \leq B (k) \land k \in X) \to if (A (k) \leq B (k), B (k) - A (k), 0) = B (k) - A (k)$
44	43	adantll	$⊢ (((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \land k \in X) \to if (A (k) \leq B (k), B (k) - A (k), 0) = B (k) - A (k)$
45	41 44	eqtrd	$⊢ (((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \land k \in X) \to vol ([A (k), B (k))) = B (k) - A (k)$
46	45	ex	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to (k \in X \to vol ([A (k), B (k))) = B (k) - A (k))$
47	36 46	ralrimi	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \forall k \in X vol ([A (k), B (k))) = B (k) - A (k)$
48	47	prodeq2d	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in X} (B (k) - A (k))$
49	48	eqcomd	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \prod_{k \in X} (B (k) - A (k)) = \prod_{k \in X} vol ([A (k), B (k)))$
50		fveq2	$⊢ k = j \to A (k) = A (j)$
51		fveq2	$⊢ k = j \to B (k) = B (j)$
52	50 51	breq12d	$⊢ k = j \to (A (k) \leq B (k) \leftrightarrow A (j) \leq B (j))$
53	52	cbvralvw	$⊢ \forall k \in X A (k) \leq B (k) \leftrightarrow \forall j \in X A (j) \leq B (j)$
54	53	bilani	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \forall j \in X A (j) \leq B (j)$
55	1	adantr	$⊢ (φ \land X \neq \emptyset) \to X \in Fin$
56	55	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to X \in Fin$
57	2	adantr	$⊢ (φ \land X \neq \emptyset) \to A : X ⟶ ℝ$
58	57	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to A : X ⟶ ℝ$
59	3	adantr	$⊢ (φ \land X \neq \emptyset) \to B : X ⟶ ℝ$
60	59	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to B : X ⟶ ℝ$
61		simpr	$⊢ (φ \land X \neq \emptyset) \to X \neq \emptyset$
62	61	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to X \neq \emptyset$
63	53 42	sylanbr	$⊢ (\forall j \in X A (j) \leq B (j) \land k \in X) \to A (k) \leq B (k)$
64	63	adantll	$⊢ (((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \land k \in X) \to A (k) \leq B (k)$
65		fveq2	$⊢ j = k \to B (j) = B (k)$
66	65	oveq1d	$⊢ j = k \to B (j) + (\frac{1}{m}) = B (k) + (\frac{1}{m})$
67	66	cbvmptv	$⊢ (j \in X ⟼ B (j) + (\frac{1}{m})) = (k \in X ⟼ B (k) + (\frac{1}{m}))$
68	67	mpteq2i	$⊢ (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) = (m \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{m})))$
69		oveq2	$⊢ m = n \to \frac{1}{m} = \frac{1}{n}$
70	69	oveq2d	$⊢ m = n \to B (k) + (\frac{1}{m}) = B (k) + (\frac{1}{n})$
71	70	mpteq2dv	$⊢ m = n \to (k \in X ⟼ B (k) + (\frac{1}{m})) = (k \in X ⟼ B (k) + (\frac{1}{n}))$
72	71	cbvmptv	$⊢ (m \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{m}))) = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
73	68 72	eqtri	$⊢ (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
74		fveq2	$⊢ i = n \to (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) = (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n)$
75	74	fveq1d	$⊢ i = n \to (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k) = (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k)$
76	75	oveq2d	$⊢ i = n \to [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k)) = [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k))$
77	76	ixpeq2dv	$⊢ i = n \to \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k)) = \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k))$
78	77	cbvmptv	$⊢ (i \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k))) = (n \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k)))$
79	56 58 60 62 64 4 73 78	vonicclem2	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$
80	54 79	syldan	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$
81	5 55 61 57 59	hoidmvn0val	$⊢ (φ \land X \neq \emptyset) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
82	81	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
83	49 80 82	3eqtr4d	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to voln (X) (I) = A L (X) B$
84		rexnal	$⊢ \exists k \in X \neg A (k) \leq B (k) \leftrightarrow \neg \forall k \in X A (k) \leq B (k)$
85	84	bilanri	$⊢ (φ \land \neg \forall k \in X A (k) \leq B (k)) \to \exists k \in X \neg A (k) \leq B (k)$
86		simpr	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to \neg A (k) \leq B (k)$
87	38	adantr	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to B (k) \in ℝ$
88	37	adantr	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to A (k) \in ℝ$
89	87 88	ltnled	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to (B (k) < A (k) \leftrightarrow \neg A (k) \leq B (k))$
90	86 89	mpbird	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to B (k) < A (k)$
91	90	ex	$⊢ (φ \land k \in X) \to (\neg A (k) \leq B (k) \to B (k) < A (k))$
92	91	reximdva	$⊢ φ \to (\exists k \in X \neg A (k) \leq B (k) \to \exists k \in X B (k) < A (k))$
93	92	adantr	$⊢ (φ \land \neg \forall k \in X A (k) \leq B (k)) \to (\exists k \in X \neg A (k) \leq B (k) \to \exists k \in X B (k) < A (k))$
94	85 93	mpd	$⊢ (φ \land \neg \forall k \in X A (k) \leq B (k)) \to \exists k \in X B (k) < A (k)$
95	94	adantlr	$⊢ ((φ \land X \neq \emptyset) \land \neg \forall k \in X A (k) \leq B (k)) \to \exists k \in X B (k) < A (k)$
96		nfcv	$⊢ \underline{Ⅎ} k voln (X)$
97		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in X}{⨉} [A (k), B (k)]$
98	4 97	nfcxfr	$⊢ \underline{Ⅎ} k I$
99	96 98	nffv	$⊢ \underline{Ⅎ} k voln (X) (I)$
100		nfcv	$⊢ \underline{Ⅎ} k A$
101		nfcv	$⊢ \underline{Ⅎ} k Fin$
102		nfcv	$⊢ \underline{Ⅎ} k (ℝ^{x})$
103		nfv	$⊢ Ⅎ k x = \emptyset$
104		nfcv	$⊢ \underline{Ⅎ} k 0$
105		nfcv	$⊢ \underline{Ⅎ} k x$
106	105	nfcprod1	$⊢ \underline{Ⅎ} k \prod_{k \in x} vol ([a (k), b (k)))$
107	103 104 106	nfif	$⊢ \underline{Ⅎ} k if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))$
108	102 102 107	nfmpo	$⊢ \underline{Ⅎ} k (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))$
109	101 108	nfmpt	$⊢ \underline{Ⅎ} k (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
110	5 109	nfcxfr	$⊢ \underline{Ⅎ} k L$
111		nfcv	$⊢ \underline{Ⅎ} k X$
112	110 111	nffv	$⊢ \underline{Ⅎ} k L (X)$
113		nfcv	$⊢ \underline{Ⅎ} k B$
114	100 112 113	nfov	$⊢ \underline{Ⅎ} k (A L (X) B)$
115	99 114	nfeq	$⊢ Ⅎ k voln (X) (I) = A L (X) B$
116	1	vonmea	$⊢ φ \to voln (X) \in Meas$
117	116	mea0	$⊢ φ \to voln (X) (\emptyset) = 0$
118	117	3ad2ant1	$⊢ (φ \land k \in X \land B (k) < A (k)) \to voln (X) (\emptyset) = 0$
119	4	a1i	$⊢ (φ \land k \in X \land B (k) < A (k)) \to I = \underset{k \in X}{⨉} [A (k), B (k)]$
120		simp2	$⊢ (φ \land k \in X \land B (k) < A (k)) \to k \in X$
121		simp3	$⊢ (φ \land k \in X \land B (k) < A (k)) \to B (k) < A (k)$
122		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
123	122 37	sselid	$⊢ (φ \land k \in X) \to A (k) \in ℝ^{*}$
124	122 38	sselid	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
125		icc0	$⊢ (A (k) \in ℝ^{} \land B (k) \in ℝ^{}) \to ([A (k), B (k)] = \emptyset \leftrightarrow B (k) < A (k))$
126	123 124 125	syl2anc	$⊢ (φ \land k \in X) \to ([A (k), B (k)] = \emptyset \leftrightarrow B (k) < A (k))$
127	126	3adant3	$⊢ (φ \land k \in X \land B (k) < A (k)) \to ([A (k), B (k)] = \emptyset \leftrightarrow B (k) < A (k))$
128	121 127	mpbird	$⊢ (φ \land k \in X \land B (k) < A (k)) \to [A (k), B (k)] = \emptyset$
129		rspe	$⊢ (k \in X \land [A (k), B (k)] = \emptyset) \to \exists k \in X [A (k), B (k)] = \emptyset$
130	120 128 129	syl2anc	$⊢ (φ \land k \in X \land B (k) < A (k)) \to \exists k \in X [A (k), B (k)] = \emptyset$
131		ixp0	$⊢ \exists k \in X [A (k), B (k)] = \emptyset \to \underset{k \in X}{⨉} [A (k), B (k)] = \emptyset$
132	130 131	syl	$⊢ (φ \land k \in X \land B (k) < A (k)) \to \underset{k \in X}{⨉} [A (k), B (k)] = \emptyset$
133	119 132	eqtrd	$⊢ (φ \land k \in X \land B (k) < A (k)) \to I = \emptyset$
134	133	fveq2d	$⊢ (φ \land k \in X \land B (k) < A (k)) \to voln (X) (I) = voln (X) (\emptyset)$
135		ne0i	$⊢ k \in X \to X \neq \emptyset$
136	135	adantl	$⊢ (φ \land k \in X) \to X \neq \emptyset$
137	136 81	syldan	$⊢ (φ \land k \in X) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
138	137	3adant3	$⊢ (φ \land k \in X \land B (k) < A (k)) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
139		eleq1w	$⊢ j = k \to (j \in X \leftrightarrow k \in X)$
140		fveq2	$⊢ j = k \to A (j) = A (k)$
141	65 140	breq12d	$⊢ j = k \to (B (j) < A (j) \leftrightarrow B (k) < A (k))$
142	139 141	3anbi23d	$⊢ j = k \to ((φ \land j \in X \land B (j) < A (j)) \leftrightarrow (φ \land k \in X \land B (k) < A (k)))$
143	142	imbi1d	$⊢ j = k \to (((φ \land j \in X \land B (j) < A (j)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0) \leftrightarrow ((φ \land k \in X \land B (k) < A (k)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0))$
144		nfv	$⊢ Ⅎ k (φ \land j \in X \land B (j) < A (j))$
145	1	3ad2ant1	$⊢ (φ \land j \in X \land B (j) < A (j)) \to X \in Fin$
146		volicore	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) \in ℝ$
147	37 38 146	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℝ$
148	147	recnd	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℂ$
149	148	3ad2antl1	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k \in X) \to vol ([A (k), B (k))) \in ℂ$
150		simp2	$⊢ (φ \land j \in X \land B (j) < A (j)) \to j \in X$
151	50 51	oveq12d	$⊢ k = j \to [A (k), B (k)) = [A (j), B (j))$
152	151	fveq2d	$⊢ k = j \to vol ([A (k), B (k))) = vol ([A (j), B (j)))$
153	152	adantl	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k = j) \to vol ([A (k), B (k))) = vol ([A (j), B (j)))$
154	2	ffvelcdmda	$⊢ (φ \land j \in X) \to A (j) \in ℝ$
155	3	ffvelcdmda	$⊢ (φ \land j \in X) \to B (j) \in ℝ$
156		volico2	$⊢ (A (j) \in ℝ \land B (j) \in ℝ) \to vol ([A (j), B (j))) = if (A (j) \leq B (j), B (j) - A (j), 0)$
157	154 155 156	syl2anc	$⊢ (φ \land j \in X) \to vol ([A (j), B (j))) = if (A (j) \leq B (j), B (j) - A (j), 0)$
158	157	3adant3	$⊢ (φ \land j \in X \land B (j) < A (j)) \to vol ([A (j), B (j))) = if (A (j) \leq B (j), B (j) - A (j), 0)$
159		simp3	$⊢ (φ \land j \in X \land B (j) < A (j)) \to B (j) < A (j)$
160	155 154	ltnled	$⊢ (φ \land j \in X) \to (B (j) < A (j) \leftrightarrow \neg A (j) \leq B (j))$
161	160	3adant3	$⊢ (φ \land j \in X \land B (j) < A (j)) \to (B (j) < A (j) \leftrightarrow \neg A (j) \leq B (j))$
162	159 161	mpbid	$⊢ (φ \land j \in X \land B (j) < A (j)) \to \neg A (j) \leq B (j)$
163	162	iffalsed	$⊢ (φ \land j \in X \land B (j) < A (j)) \to if (A (j) \leq B (j), B (j) - A (j), 0) = 0$
164	158 163	eqtrd	$⊢ (φ \land j \in X \land B (j) < A (j)) \to vol ([A (j), B (j))) = 0$
165	164	adantr	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k = j) \to vol ([A (j), B (j))) = 0$
166	153 165	eqtrd	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k = j) \to vol ([A (k), B (k))) = 0$
167	144 145 149 150 166	fprodeq0g	$⊢ (φ \land j \in X \land B (j) < A (j)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0$
168	143 167	chvarvv	$⊢ (φ \land k \in X \land B (k) < A (k)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0$
169	138 168	eqtrd	$⊢ (φ \land k \in X \land B (k) < A (k)) \to A L (X) B = 0$
170	118 134 169	3eqtr4d	$⊢ (φ \land k \in X \land B (k) < A (k)) \to voln (X) (I) = A L (X) B$
171	170	3exp	$⊢ φ \to (k \in X \to (B (k) < A (k) \to voln (X) (I) = A L (X) B))$
172	171	adantr	$⊢ (φ \land X \neq \emptyset) \to (k \in X \to (B (k) < A (k) \to voln (X) (I) = A L (X) B))$
173	34 115 172	rexlimd	$⊢ (φ \land X \neq \emptyset) \to (\exists k \in X B (k) < A (k) \to voln (X) (I) = A L (X) B)$
174	173	imp	$⊢ ((φ \land X \neq \emptyset) \land \exists k \in X B (k) < A (k)) \to voln (X) (I) = A L (X) B$
175	95 174	syldan	$⊢ ((φ \land X \neq \emptyset) \land \neg \forall k \in X A (k) \leq B (k)) \to voln (X) (I) = A L (X) B$
176	83 175	pm2.61dan	$⊢ (φ \land X \neq \emptyset) \to voln (X) (I) = A L (X) B$
177	33 176	syldan	$⊢ (φ \land \neg X = \emptyset) \to voln (X) (I) = A L (X) B$
178	31 177	pm2.61dan	$⊢ φ \to voln (X) (I) = A L (X) B$

Metamath Proof Explorer

Theorem vonicc

Proof