vonioolem2

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

	Ref	Expression
Hypotheses	vonioolem2.x	$⊢ φ \to X \in Fin$
	vonioolem2.a	$⊢ φ \to A : X ⟶ ℝ$
	vonioolem2.b	$⊢ φ \to B : X ⟶ ℝ$
	vonioolem2.n	$⊢ φ \to X \neq \emptyset$
	vonioolem2.t	$⊢ (φ \land k \in X) \to A (k) < B (k)$
	vonioolem2.i	$⊢ I = \underset{k \in X}{⨉} (A (k), B (k))$
	vonioolem2.c	$⊢ C = (n \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{n})))$
	vonioolem2.d	$⊢ D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [C (n) (k), B (k)))$
Assertion	vonioolem2	$⊢ φ \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$

Proof

Step	Hyp	Ref	Expression
1		vonioolem2.x	$⊢ φ \to X \in Fin$
2		vonioolem2.a	$⊢ φ \to A : X ⟶ ℝ$
3		vonioolem2.b	$⊢ φ \to B : X ⟶ ℝ$
4		vonioolem2.n	$⊢ φ \to X \neq \emptyset$
5		vonioolem2.t	$⊢ (φ \land k \in X) \to A (k) < B (k)$
6		vonioolem2.i	$⊢ I = \underset{k \in X}{⨉} (A (k), B (k))$
7		vonioolem2.c	$⊢ C = (n \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{n})))$
8		vonioolem2.d	$⊢ D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [C (n) (k), B (k)))$
9	1	vonmea	$⊢ φ \to voln (X) \in Meas$
10		1zzd	$⊢ φ \to 1 \in ℤ$
11		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
12	1	adantr	$⊢ (φ \land n \in ℕ) \to X \in Fin$
13		eqid	$⊢ dom voln (X) = dom voln (X)$
14	2	adantr	$⊢ (φ \land n \in ℕ) \to A : X ⟶ ℝ$
15	14	ffvelcdmda	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℝ$
16		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
17	16	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ$
18	15 17	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) + (\frac{1}{n}) \in ℝ$
19	18	fmpttd	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ A (k) + (\frac{1}{n})) : X ⟶ ℝ$
20	7	a1i	$⊢ φ \to C = (n \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{n})))$
21	1	mptexd	$⊢ φ \to (k \in X ⟼ A (k) + (\frac{1}{n})) \in V$
22	21	adantr	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ A (k) + (\frac{1}{n})) \in V$
23	20 22	fvmpt2d	$⊢ (φ \land n \in ℕ) \to C (n) = (k \in X ⟼ A (k) + (\frac{1}{n}))$
24	23	feq1d	$⊢ (φ \land n \in ℕ) \to (C (n) : X ⟶ ℝ \leftrightarrow (k \in X ⟼ A (k) + (\frac{1}{n})) : X ⟶ ℝ)$
25	19 24	mpbird	$⊢ (φ \land n \in ℕ) \to C (n) : X ⟶ ℝ$
26	3	adantr	$⊢ (φ \land n \in ℕ) \to B : X ⟶ ℝ$
27	12 13 25 26	hoimbl	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [C (n) (k), B (k)) \in dom voln (X)$
28	27 8	fmptd	$⊢ φ \to D : ℕ ⟶ dom voln (X)$
29		nfv	$⊢ Ⅎ k (φ \land n \in ℕ)$
30		oveq2	$⊢ n = m \to \frac{1}{n} = \frac{1}{m}$
31	30	oveq2d	$⊢ n = m \to A (k) + (\frac{1}{n}) = A (k) + (\frac{1}{m})$
32	31	mpteq2dv	$⊢ n = m \to (k \in X ⟼ A (k) + (\frac{1}{n})) = (k \in X ⟼ A (k) + (\frac{1}{m}))$
33	32	cbvmptv	$⊢ (n \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{n}))) = (m \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{m})))$
34	7 33	eqtri	$⊢ C = (m \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{m})))$
35		oveq2	$⊢ m = n + 1 \to \frac{1}{m} = \frac{1}{n + 1}$
36	35	oveq2d	$⊢ m = n + 1 \to A (k) + (\frac{1}{m}) = A (k) + (\frac{1}{n + 1})$
37	36	mpteq2dv	$⊢ m = n + 1 \to (k \in X ⟼ A (k) + (\frac{1}{m})) = (k \in X ⟼ A (k) + (\frac{1}{n + 1}))$
38		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
39	38	peano2nnd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℕ$
40	12	mptexd	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ A (k) + (\frac{1}{n + 1})) \in V$
41	34 37 39 40	fvmptd3	$⊢ (φ \land n \in ℕ) \to C (n + 1) = (k \in X ⟼ A (k) + (\frac{1}{n + 1}))$
42		ovexd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) + (\frac{1}{n + 1}) \in V$
43	41 42	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n + 1) (k) = A (k) + (\frac{1}{n + 1})$
44		1red	$⊢ n \in ℕ \to 1 \in ℝ$
45		nnre	$⊢ n \in ℕ \to n \in ℝ$
46	45 44	readdcld	$⊢ n \in ℕ \to n + 1 \in ℝ$
47		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
48		nnne0	$⊢ n + 1 \in ℕ \to n + 1 \neq 0$
49	47 48	syl	$⊢ n \in ℕ \to n + 1 \neq 0$
50	44 46 49	redivcld	$⊢ n \in ℕ \to \frac{1}{n + 1} \in ℝ$
51	50	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n + 1} \in ℝ$
52	15 51	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) + (\frac{1}{n + 1}) \in ℝ$
53	43 52	eqeltrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n + 1) (k) \in ℝ$
54	53	rexrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n + 1) (k) \in ℝ^{*}$
55		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
56	3	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
57	55 56	sselid	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
58	57	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℝ^{*}$
59	45	ltp1d	$⊢ n \in ℕ \to n < n + 1$
60		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
61	47	nnrpd	$⊢ n \in ℕ \to n + 1 \in ℝ^{+}$
62	60 61	ltrecd	$⊢ n \in ℕ \to (n < n + 1 \leftrightarrow \frac{1}{n + 1} < \frac{1}{n})$
63	59 62	mpbid	$⊢ n \in ℕ \to \frac{1}{n + 1} < \frac{1}{n}$
64	50 16 63	ltled	$⊢ n \in ℕ \to \frac{1}{n + 1} \leq \frac{1}{n}$
65	64	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n + 1} \leq \frac{1}{n}$
66	51 17 15 65	leadd2dd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) + (\frac{1}{n + 1}) \leq A (k) + (\frac{1}{n})$
67		ovexd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) + (\frac{1}{n}) \in V$
68	23 67	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) = A (k) + (\frac{1}{n})$
69	43 68	breq12d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to (C (n + 1) (k) \leq C (n) (k) \leftrightarrow A (k) + (\frac{1}{n + 1}) \leq A (k) + (\frac{1}{n}))$
70	66 69	mpbird	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n + 1) (k) \leq C (n) (k)$
71	56	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℝ$
72		eqidd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) = B (k)$
73	71 72	eqled	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \leq B (k)$
74		icossico	$⊢ ((C (n + 1) (k) \in ℝ^{} \land B (k) \in ℝ^{}) \land (C (n + 1) (k) \leq C (n) (k) \land B (k) \leq B (k))) \to [C (n) (k), B (k)) \subseteq [C (n + 1) (k), B (k))$
75	54 58 70 73 74	syl22anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [C (n) (k), B (k)) \subseteq [C (n + 1) (k), B (k))$
76	29 75	ixpssixp	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [C (n) (k), B (k)) \subseteq \underset{k \in X}{⨉} [C (n + 1) (k), B (k))$
77	8	a1i	$⊢ φ \to D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [C (n) (k), B (k)))$
78	27	elexd	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [C (n) (k), B (k)) \in V$
79	77 78	fvmpt2d	$⊢ (φ \land n \in ℕ) \to D (n) = \underset{k \in X}{⨉} [C (n) (k), B (k))$
80		fveq2	$⊢ n = m \to C (n) = C (m)$
81	80	fveq1d	$⊢ n = m \to C (n) (k) = C (m) (k)$
82	81	oveq1d	$⊢ n = m \to [C (n) (k), B (k)) = [C (m) (k), B (k))$
83	82	ixpeq2dv	$⊢ n = m \to \underset{k \in X}{⨉} [C (n) (k), B (k)) = \underset{k \in X}{⨉} [C (m) (k), B (k))$
84	83	cbvmptv	$⊢ (n \in ℕ ⟼ \underset{k \in X}{⨉} [C (n) (k), B (k))) = (m \in ℕ ⟼ \underset{k \in X}{⨉} [C (m) (k), B (k)))$
85	8 84	eqtri	$⊢ D = (m \in ℕ ⟼ \underset{k \in X}{⨉} [C (m) (k), B (k)))$
86		fveq2	$⊢ m = n + 1 \to C (m) = C (n + 1)$
87	86	fveq1d	$⊢ m = n + 1 \to C (m) (k) = C (n + 1) (k)$
88	87	oveq1d	$⊢ m = n + 1 \to [C (m) (k), B (k)) = [C (n + 1) (k), B (k))$
89	88	ixpeq2dv	$⊢ m = n + 1 \to \underset{k \in X}{⨉} [C (m) (k), B (k)) = \underset{k \in X}{⨉} [C (n + 1) (k), B (k))$
90		ovex	$⊢ [C (n + 1) (k), B (k)) \in V$
91	90	rgenw	$⊢ \forall k \in X [C (n + 1) (k), B (k)) \in V$
92		ixpexg	$⊢ \forall k \in X [C (n + 1) (k), B (k)) \in V \to \underset{k \in X}{⨉} [C (n + 1) (k), B (k)) \in V$
93	91 92	ax-mp	$⊢ \underset{k \in X}{⨉} [C (n + 1) (k), B (k)) \in V$
94	93	a1i	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [C (n + 1) (k), B (k)) \in V$
95	85 89 39 94	fvmptd3	$⊢ (φ \land n \in ℕ) \to D (n + 1) = \underset{k \in X}{⨉} [C (n + 1) (k), B (k))$
96	79 95	sseq12d	$⊢ (φ \land n \in ℕ) \to (D (n) \subseteq D (n + 1) \leftrightarrow \underset{k \in X}{⨉} [C (n) (k), B (k)) \subseteq \underset{k \in X}{⨉} [C (n + 1) (k), B (k)))$
97	76 96	mpbird	$⊢ (φ \land n \in ℕ) \to D (n) \subseteq D (n + 1)$
98	1 13 2 3	hoimbl	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) \in dom voln (X)$
99		nfv	$⊢ Ⅎ k φ$
100	2	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
101	99 1 100 56	vonhoire	$⊢ φ \to voln (X) (\underset{k \in X}{⨉} [A (k), B (k))) \in ℝ$
102	6	a1i	$⊢ φ \to I = \underset{k \in X}{⨉} (A (k), B (k))$
103		nftru	$⊢ Ⅎ k ⊤$
104		ioossico	$⊢ (A (k), B (k)) \subseteq [A (k), B (k))$
105	104	a1i	$⊢ (⊤ \land k \in X) \to (A (k), B (k)) \subseteq [A (k), B (k))$
106	103 105	ixpssixp	$⊢ ⊤ \to \underset{k \in X}{⨉} (A (k), B (k)) \subseteq \underset{k \in X}{⨉} [A (k), B (k))$
107	106	mptru	$⊢ \underset{k \in X}{⨉} (A (k), B (k)) \subseteq \underset{k \in X}{⨉} [A (k), B (k))$
108	107	a1i	$⊢ φ \to \underset{k \in X}{⨉} (A (k), B (k)) \subseteq \underset{k \in X}{⨉} [A (k), B (k))$
109	102 108	eqsstrd	$⊢ φ \to I \subseteq \underset{k \in X}{⨉} [A (k), B (k))$
110	55	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
111	2 110	fssd	$⊢ φ \to A : X ⟶ ℝ^{*}$
112	3 110	fssd	$⊢ φ \to B : X ⟶ ℝ^{*}$
113	1 13 111 112	ioovonmbl	$⊢ φ \to \underset{k \in X}{⨉} (A (k), B (k)) \in dom voln (X)$
114	6 113	eqeltrid	$⊢ φ \to I \in dom voln (X)$
115	9 98 101 109 114	meassre	$⊢ φ \to voln (X) (I) \in ℝ$
116	9	adantr	$⊢ (φ \land n \in ℕ) \to voln (X) \in Meas$
117	79 27	eqeltrd	$⊢ (φ \land n \in ℕ) \to D (n) \in dom voln (X)$
118	114	adantr	$⊢ (φ \land n \in ℕ) \to I \in dom voln (X)$
119	55 100	sselid	$⊢ (φ \land k \in X) \to A (k) \in ℝ^{*}$
120	119	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℝ^{*}$
121	60	rpreccld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
122	121	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ^{+}$
123	15 122	ltaddrpd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) < A (k) + (\frac{1}{n})$
124		icossioo	$⊢ ((A (k) \in ℝ^{} \land B (k) \in ℝ^{}) \land (A (k) < A (k) + (\frac{1}{n}) \land B (k) \leq B (k))) \to [A (k) + (\frac{1}{n}), B (k)) \subseteq (A (k), B (k))$
125	120 58 123 73 124	syl22anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [A (k) + (\frac{1}{n}), B (k)) \subseteq (A (k), B (k))$
126	29 125	ixpssixp	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k) + (\frac{1}{n}), B (k)) \subseteq \underset{k \in X}{⨉} (A (k), B (k))$
127	68	oveq1d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [C (n) (k), B (k)) = [A (k) + (\frac{1}{n}), B (k))$
128	127	ixpeq2dva	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [C (n) (k), B (k)) = \underset{k \in X}{⨉} [A (k) + (\frac{1}{n}), B (k))$
129	79 128	eqtrd	$⊢ (φ \land n \in ℕ) \to D (n) = \underset{k \in X}{⨉} [A (k) + (\frac{1}{n}), B (k))$
130	6	a1i	$⊢ (φ \land n \in ℕ) \to I = \underset{k \in X}{⨉} (A (k), B (k))$
131	129 130	sseq12d	$⊢ (φ \land n \in ℕ) \to (D (n) \subseteq I \leftrightarrow \underset{k \in X}{⨉} [A (k) + (\frac{1}{n}), B (k)) \subseteq \underset{k \in X}{⨉} (A (k), B (k)))$
132	126 131	mpbird	$⊢ (φ \land n \in ℕ) \to D (n) \subseteq I$
133	116 13 117 118 132	meassle	$⊢ (φ \land n \in ℕ) \to voln (X) (D (n)) \leq voln (X) (I)$
134		eqid	$⊢ (n \in ℕ ⟼ voln (X) (D (n))) = (n \in ℕ ⟼ voln (X) (D (n)))$
135	9 10 11 28 97 115 133 134	meaiuninc2	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) ⇝ voln (X) (⋃_{n \in ℕ} D (n))$
136	99 1 100 57	iunhoiioo	$⊢ φ \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A (k) + (\frac{1}{n}), B (k)) = \underset{k \in X}{⨉} (A (k), B (k))$
137	129	iuneq2dv	$⊢ φ \to ⋃_{n \in ℕ} D (n) = ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A (k) + (\frac{1}{n}), B (k))$
138	136 137 102	3eqtr4d	$⊢ φ \to ⋃_{n \in ℕ} D (n) = I$
139	138	eqcomd	$⊢ φ \to I = ⋃_{n \in ℕ} D (n)$
140	139	fveq2d	$⊢ φ \to voln (X) (I) = voln (X) (⋃_{n \in ℕ} D (n))$
141	140	eqcomd	$⊢ φ \to voln (X) (⋃_{n \in ℕ} D (n)) = voln (X) (I)$
142	135 141	breqtrd	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) ⇝ voln (X) (I)$
143		2fveq3	$⊢ n = m \to voln (X) (D (n)) = voln (X) (D (m))$
144	143	cbvmptv	$⊢ (n \in ℕ ⟼ voln (X) (D (n))) = (m \in ℕ ⟼ voln (X) (D (m)))$
145	144	a1i	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) = (m \in ℕ ⟼ voln (X) (D (m)))$
146	144	eqcomi	$⊢ (m \in ℕ ⟼ voln (X) (D (m))) = (n \in ℕ ⟼ voln (X) (D (n)))$
147		eqcom	$⊢ n = m \leftrightarrow m = n$
148	147	imbi1i	$⊢ (n = m \to C (n) (k) = C (m) (k)) \leftrightarrow (m = n \to C (n) (k) = C (m) (k))$
149		eqcom	$⊢ C (n) (k) = C (m) (k) \leftrightarrow C (m) (k) = C (n) (k)$
150	149	imbi2i	$⊢ (m = n \to C (n) (k) = C (m) (k)) \leftrightarrow (m = n \to C (m) (k) = C (n) (k))$
151	148 150	bitri	$⊢ (n = m \to C (n) (k) = C (m) (k)) \leftrightarrow (m = n \to C (m) (k) = C (n) (k))$
152	81 151	mpbi	$⊢ m = n \to C (m) (k) = C (n) (k)$
153	152	oveq2d	$⊢ m = n \to B (k) - C (m) (k) = B (k) - C (n) (k)$
154	153	prodeq2ad	$⊢ m = n \to \prod_{k \in X} (B (k) - C (m) (k)) = \prod_{k \in X} (B (k) - C (n) (k))$
155	154	cbvmptv	$⊢ (m \in ℕ ⟼ \prod_{k \in X} (B (k) - C (m) (k))) = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - C (n) (k)))$
156		eqid	$⊢ inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <) = inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)$
157		eqid	$⊢ ⌊\frac{1}{inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)}⌋ + 1 = ⌊\frac{1}{inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)}⌋ + 1$
158		fveq2	$⊢ j = k \to B (j) = B (k)$
159		fveq2	$⊢ j = k \to A (j) = A (k)$
160	158 159	oveq12d	$⊢ j = k \to B (j) - A (j) = B (k) - A (k)$
161	160	cbvmptv	$⊢ (j \in X ⟼ B (j) - A (j)) = (k \in X ⟼ B (k) - A (k))$
162	161	rneqi	$⊢ ran (j \in X ⟼ B (j) - A (j)) = ran (k \in X ⟼ B (k) - A (k))$
163	162	infeq1i	$⊢ inf (ran (j \in X ⟼ B (j) - A (j)) ℝ <) = inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)$
164	163	oveq2i	$⊢ \frac{1}{inf (ran (j \in X ⟼ B (j) - A (j)) ℝ <)} = \frac{1}{inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)}$
165	164	fveq2i	$⊢ ⌊\frac{1}{inf (ran (j \in X ⟼ B (j) - A (j)) ℝ <)}⌋ = ⌊\frac{1}{inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)}⌋$
166	165	oveq1i	$⊢ ⌊\frac{1}{inf (ran (j \in X ⟼ B (j) - A (j)) ℝ <)}⌋ + 1 = ⌊\frac{1}{inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)}⌋ + 1$
167	166	fveq2i	$⊢ ℤ_{\geq (⌊\frac{1}{inf (ran (j \in X ⟼ B (j) - A (j)) ℝ <)}⌋ + 1)} = ℤ_{\geq (⌊\frac{1}{inf (ran (k \in X ⟼ B (k) - A (k)) ℝ <)}⌋ + 1)}$
168	1 2 3 4 5 7 8 146 155 156 157 167	vonioolem1	$⊢ φ \to (m \in ℕ ⟼ voln (X) (D (m))) ⇝ \prod_{k \in X} (B (k) - A (k))$
169	145 168	eqbrtrd	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) ⇝ \prod_{k \in X} (B (k) - A (k))$
170		climuni	$⊢ ((n \in ℕ ⟼ voln (X) (D (n))) ⇝ voln (X) (I) \land (n \in ℕ ⟼ voln (X) (D (n))) ⇝ \prod_{k \in X} (B (k) - A (k))) \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$
171	142 169 170	syl2anc	$⊢ φ \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$

Metamath Proof Explorer

Theorem vonioolem2

Proof