vonioo

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

	Ref	Expression
Hypotheses	vonioo.x	$⊢ φ \to X \in Fin$
	vonioo.a	$⊢ φ \to A : X ⟶ ℝ$
	vonioo.b	$⊢ φ \to B : X ⟶ ℝ$
	vonioo.i	$⊢ I = \underset{k \in X}{⨉} (A (k), B (k))$
	vonioo.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	vonioo	$⊢ φ \to voln (X) (I) = A L (X) B$

Proof

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

Metamath Proof Explorer

Theorem vonioo

Proof