vonicclem2

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

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

Proof

Step	Hyp	Ref	Expression
1		vonicclem2.x	$⊢ φ \to X \in Fin$
2		vonicclem2.a	$⊢ φ \to A : X ⟶ ℝ$
3		vonicclem2.b	$⊢ φ \to B : X ⟶ ℝ$
4		vonicclem2.n	$⊢ φ \to X \neq \emptyset$
5		vonicclem2.t	$⊢ (φ \land k \in X) \to A (k) \leq B (k)$
6		vonicclem2.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k)]$
7		vonicclem2.c	$⊢ C = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
8		vonicclem2.d	$⊢ D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), C (n) (k)))$
9		nfv	$⊢ Ⅎ n φ$
10	1	vonmea	$⊢ φ \to voln (X) \in Meas$
11		1zzd	$⊢ φ \to 1 \in ℤ$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13	1	adantr	$⊢ (φ \land n \in ℕ) \to X \in Fin$
14		eqid	$⊢ dom voln (X) = dom voln (X)$
15	2	adantr	$⊢ (φ \land n \in ℕ) \to A : X ⟶ ℝ$
16	3	ffvelrnda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
17	16	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℝ$
18		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
19	18	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ$
20	17 19	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) + (\frac{1}{n}) \in ℝ$
21	20	fmpttd	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ B (k) + (\frac{1}{n})) : X ⟶ ℝ$
22	7	a1i	$⊢ φ \to C = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
23	1	mptexd	$⊢ φ \to (k \in X ⟼ B (k) + (\frac{1}{n})) \in V$
24	23	adantr	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ B (k) + (\frac{1}{n})) \in V$
25	22 24	fvmpt2d	$⊢ (φ \land n \in ℕ) \to C (n) = (k \in X ⟼ B (k) + (\frac{1}{n}))$
26	25	feq1d	$⊢ (φ \land n \in ℕ) \to (C (n) : X ⟶ ℝ \leftrightarrow (k \in X ⟼ B (k) + (\frac{1}{n})) : X ⟶ ℝ)$
27	21 26	mpbird	$⊢ (φ \land n \in ℕ) \to C (n) : X ⟶ ℝ$
28	13 14 15 27	hoimbl	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k), C (n) (k)) \in dom voln (X)$
29	28 8	fmptd	$⊢ φ \to D : ℕ ⟶ dom voln (X)$
30		nfv	$⊢ Ⅎ k (φ \land n \in ℕ)$
31		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
32	2	ffvelrnda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
33	31 32	sseldi	$⊢ (φ \land k \in X) \to A (k) \in ℝ^{*}$
34	33	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℝ^{*}$
35		ovexd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) + (\frac{1}{n}) \in V$
36	25 35	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) = B (k) + (\frac{1}{n})$
37	36 20	eqeltrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) \in ℝ$
38	37	rexrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) \in ℝ^{*}$
39	15	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℝ$
40	39	leidd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \leq A (k)$
41		1red	$⊢ n \in ℕ \to 1 \in ℝ$
42		nnre	$⊢ n \in ℕ \to n \in ℝ$
43	42 41	readdcld	$⊢ n \in ℕ \to n + 1 \in ℝ$
44		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
45		nnne0	$⊢ n + 1 \in ℕ \to n + 1 \neq 0$
46	44 45	syl	$⊢ n \in ℕ \to n + 1 \neq 0$
47	41 43 46	redivcld	$⊢ n \in ℕ \to \frac{1}{n + 1} \in ℝ$
48	47	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n + 1} \in ℝ$
49	42	ltp1d	$⊢ n \in ℕ \to n < n + 1$
50		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
51	44	nnrpd	$⊢ n \in ℕ \to n + 1 \in ℝ^{+}$
52	50 51	ltrecd	$⊢ n \in ℕ \to (n < n + 1 \leftrightarrow \frac{1}{n + 1} < \frac{1}{n})$
53	49 52	mpbid	$⊢ n \in ℕ \to \frac{1}{n + 1} < \frac{1}{n}$
54	47 18 53	ltled	$⊢ n \in ℕ \to \frac{1}{n + 1} \leq \frac{1}{n}$
55	54	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n + 1} \leq \frac{1}{n}$
56	48 19 17 55	leadd2dd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) + (\frac{1}{n + 1}) \leq B (k) + (\frac{1}{n})$
57		oveq2	$⊢ n = m \to \frac{1}{n} = \frac{1}{m}$
58	57	oveq2d	$⊢ n = m \to B (k) + (\frac{1}{n}) = B (k) + (\frac{1}{m})$
59	58	mpteq2dv	$⊢ n = m \to (k \in X ⟼ B (k) + (\frac{1}{n})) = (k \in X ⟼ B (k) + (\frac{1}{m}))$
60	59	cbvmptv	$⊢ (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n}))) = (m \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{m})))$
61	7 60	eqtri	$⊢ C = (m \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{m})))$
62		oveq2	$⊢ m = n + 1 \to \frac{1}{m} = \frac{1}{n + 1}$
63	62	oveq2d	$⊢ m = n + 1 \to B (k) + (\frac{1}{m}) = B (k) + (\frac{1}{n + 1})$
64	63	mpteq2dv	$⊢ m = n + 1 \to (k \in X ⟼ B (k) + (\frac{1}{m})) = (k \in X ⟼ B (k) + (\frac{1}{n + 1}))$
65		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
66	65	peano2nnd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℕ$
67	13	mptexd	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ B (k) + (\frac{1}{n + 1})) \in V$
68	61 64 66 67	fvmptd3	$⊢ (φ \land n \in ℕ) \to C (n + 1) = (k \in X ⟼ B (k) + (\frac{1}{n + 1}))$
69		ovexd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) + (\frac{1}{n + 1}) \in V$
70	68 69	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n + 1) (k) = B (k) + (\frac{1}{n + 1})$
71	70 36	breq12d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to (C (n + 1) (k) \leq C (n) (k) \leftrightarrow B (k) + (\frac{1}{n + 1}) \leq B (k) + (\frac{1}{n}))$
72	56 71	mpbird	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n + 1) (k) \leq C (n) (k)$
73		icossico	$⊢ ((A (k) \in ℝ^{} \land C (n) (k) \in ℝ^{}) \land (A (k) \leq A (k) \land C (n + 1) (k) \leq C (n) (k))) \to [A (k), C (n + 1) (k)) \subseteq [A (k), C (n) (k))$
74	34 38 40 72 73	syl22anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [A (k), C (n + 1) (k)) \subseteq [A (k), C (n) (k))$
75	30 74	ixpssixp	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k), C (n + 1) (k)) \subseteq \underset{k \in X}{⨉} [A (k), C (n) (k))$
76		fveq2	$⊢ n = m \to C (n) = C (m)$
77	76	fveq1d	$⊢ n = m \to C (n) (k) = C (m) (k)$
78	77	oveq2d	$⊢ n = m \to [A (k), C (n) (k)) = [A (k), C (m) (k))$
79	78	ixpeq2dv	$⊢ n = m \to \underset{k \in X}{⨉} [A (k), C (n) (k)) = \underset{k \in X}{⨉} [A (k), C (m) (k))$
80	79	cbvmptv	$⊢ (n \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), C (n) (k))) = (m \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), C (m) (k)))$
81	8 80	eqtri	$⊢ D = (m \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), C (m) (k)))$
82		fveq2	$⊢ m = n + 1 \to C (m) = C (n + 1)$
83	82	fveq1d	$⊢ m = n + 1 \to C (m) (k) = C (n + 1) (k)$
84	83	oveq2d	$⊢ m = n + 1 \to [A (k), C (m) (k)) = [A (k), C (n + 1) (k))$
85	84	ixpeq2dv	$⊢ m = n + 1 \to \underset{k \in X}{⨉} [A (k), C (m) (k)) = \underset{k \in X}{⨉} [A (k), C (n + 1) (k))$
86		ovex	$⊢ [A (k), C (n + 1) (k)) \in V$
87	86	rgenw	$⊢ \forall k \in X [A (k), C (n + 1) (k)) \in V$
88		ixpexg	$⊢ \forall k \in X [A (k), C (n + 1) (k)) \in V \to \underset{k \in X}{⨉} [A (k), C (n + 1) (k)) \in V$
89	87 88	ax-mp	$⊢ \underset{k \in X}{⨉} [A (k), C (n + 1) (k)) \in V$
90	89	a1i	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k), C (n + 1) (k)) \in V$
91	81 85 66 90	fvmptd3	$⊢ (φ \land n \in ℕ) \to D (n + 1) = \underset{k \in X}{⨉} [A (k), C (n + 1) (k))$
92	8	a1i	$⊢ φ \to D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), C (n) (k)))$
93	28	elexd	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k), C (n) (k)) \in V$
94	92 93	fvmpt2d	$⊢ (φ \land n \in ℕ) \to D (n) = \underset{k \in X}{⨉} [A (k), C (n) (k))$
95	91 94	sseq12d	$⊢ (φ \land n \in ℕ) \to (D (n + 1) \subseteq D (n) \leftrightarrow \underset{k \in X}{⨉} [A (k), C (n + 1) (k)) \subseteq \underset{k \in X}{⨉} [A (k), C (n) (k)))$
96	75 95	mpbird	$⊢ (φ \land n \in ℕ) \to D (n + 1) \subseteq D (n)$
97		1nn	$⊢ 1 \in ℕ$
98	97 12	eleqtri	$⊢ 1 \in ℤ_{\geq 1}$
99	98	a1i	$⊢ φ \to 1 \in ℤ_{\geq 1}$
100		fveq2	$⊢ n = 1 \to C (n) = C (1)$
101	100	fveq1d	$⊢ n = 1 \to C (n) (k) = C (1) (k)$
102	101	oveq2d	$⊢ n = 1 \to [A (k), C (n) (k)) = [A (k), C (1) (k))$
103	102	ixpeq2dv	$⊢ n = 1 \to \underset{k \in X}{⨉} [A (k), C (n) (k)) = \underset{k \in X}{⨉} [A (k), C (1) (k))$
104	97	a1i	$⊢ φ \to 1 \in ℕ$
105		ovex	$⊢ [A (k), C (1) (k)) \in V$
106	105	rgenw	$⊢ \forall k \in X [A (k), C (1) (k)) \in V$
107		ixpexg	$⊢ \forall k \in X [A (k), C (1) (k)) \in V \to \underset{k \in X}{⨉} [A (k), C (1) (k)) \in V$
108	106 107	ax-mp	$⊢ \underset{k \in X}{⨉} [A (k), C (1) (k)) \in V$
109	108	a1i	$⊢ φ \to \underset{k \in X}{⨉} [A (k), C (1) (k)) \in V$
110	8 103 104 109	fvmptd3	$⊢ φ \to D (1) = \underset{k \in X}{⨉} [A (k), C (1) (k))$
111	110	fveq2d	$⊢ φ \to voln (X) (D (1)) = voln (X) (\underset{k \in X}{⨉} [A (k), C (1) (k)))$
112		nfv	$⊢ Ⅎ k φ$
113		simpl	$⊢ (φ \land k \in X) \to φ$
114	97	a1i	$⊢ (φ \land k \in X) \to 1 \in ℕ$
115		simpr	$⊢ (φ \land k \in X) \to k \in X$
116	97	elexi	$⊢ 1 \in V$
117		eleq1	$⊢ n = 1 \to (n \in ℕ \leftrightarrow 1 \in ℕ)$
118	117	anbi2d	$⊢ n = 1 \to ((φ \land n \in ℕ) \leftrightarrow (φ \land 1 \in ℕ))$
119	118	anbi1d	$⊢ n = 1 \to (((φ \land n \in ℕ) \land k \in X) \leftrightarrow ((φ \land 1 \in ℕ) \land k \in X))$
120	101	eleq1d	$⊢ n = 1 \to (C (n) (k) \in ℝ \leftrightarrow C (1) (k) \in ℝ)$
121	119 120	imbi12d	$⊢ n = 1 \to ((((φ \land n \in ℕ) \land k \in X) \to C (n) (k) \in ℝ) \leftrightarrow (((φ \land 1 \in ℕ) \land k \in X) \to C (1) (k) \in ℝ))$
122	116 121 37	vtocl	$⊢ ((φ \land 1 \in ℕ) \land k \in X) \to C (1) (k) \in ℝ$
123	113 114 115 122	syl21anc	$⊢ (φ \land k \in X) \to C (1) (k) \in ℝ$
124	112 1 32 123	vonhoire	$⊢ φ \to voln (X) (\underset{k \in X}{⨉} [A (k), C (1) (k))) \in ℝ$
125	111 124	eqeltrd	$⊢ φ \to voln (X) (D (1)) \in ℝ$
126		eqid	$⊢ (n \in ℕ ⟼ voln (X) (D (n))) = (n \in ℕ ⟼ voln (X) (D (n)))$
127	9 10 11 12 29 96 99 125 126	meaiininc	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) ⇝ voln (X) (⋂_{n \in ℕ} D (n))$
128	112 32 16	iinhoiicc	$⊢ φ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A (k), B (k) + (\frac{1}{n})) = \underset{k \in X}{⨉} [A (k), B (k)]$
129	36	oveq2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [A (k), C (n) (k)) = [A (k), B (k) + (\frac{1}{n}))$
130	129	ixpeq2dva	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k), C (n) (k)) = \underset{k \in X}{⨉} [A (k), B (k) + (\frac{1}{n}))$
131	94 130	eqtrd	$⊢ (φ \land n \in ℕ) \to D (n) = \underset{k \in X}{⨉} [A (k), B (k) + (\frac{1}{n}))$
132	131	iineq2dv	$⊢ φ \to ⋂_{n \in ℕ} D (n) = ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A (k), B (k) + (\frac{1}{n}))$
133	6	a1i	$⊢ φ \to I = \underset{k \in X}{⨉} [A (k), B (k)]$
134	128 132 133	3eqtr4d	$⊢ φ \to ⋂_{n \in ℕ} D (n) = I$
135	134	eqcomd	$⊢ φ \to I = ⋂_{n \in ℕ} D (n)$
136	135	fveq2d	$⊢ φ \to voln (X) (I) = voln (X) (⋂_{n \in ℕ} D (n))$
137	136	eqcomd	$⊢ φ \to voln (X) (⋂_{n \in ℕ} D (n)) = voln (X) (I)$
138	127 137	breqtrd	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) ⇝ voln (X) (I)$
139		2fveq3	$⊢ n = m \to voln (X) (D (n)) = voln (X) (D (m))$
140	139	cbvmptv	$⊢ (n \in ℕ ⟼ voln (X) (D (n))) = (m \in ℕ ⟼ voln (X) (D (m)))$
141	140	a1i	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) = (m \in ℕ ⟼ voln (X) (D (m)))$
142	140	eqcomi	$⊢ (m \in ℕ ⟼ voln (X) (D (m))) = (n \in ℕ ⟼ voln (X) (D (n)))$
143	1 2 3 4 5 7 8 142	vonicclem1	$⊢ φ \to (m \in ℕ ⟼ voln (X) (D (m))) ⇝ \prod_{k \in X} (B (k) - A (k))$
144	141 143	eqbrtrd	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) ⇝ \prod_{k \in X} (B (k) - A (k))$
145		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))$
146	138 144 145	syl2anc	$⊢ φ \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$

Metamath Proof Explorer

Theorem vonicclem2

Proof