vonioolem1

Description: The sequence of the measures of the half-open intervals converges to the measure of their union. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonioolem1.x	$⊢ φ \to X \in Fin$
	vonioolem1.a	$⊢ φ \to A : X ⟶ ℝ$
	vonioolem1.b	$⊢ φ \to B : X ⟶ ℝ$
	vonioolem1.u	$⊢ φ \to X \neq \emptyset$
	vonioolem1.t	$⊢ (φ \land k \in X) \to A (k) < B (k)$
	vonioolem1.c	$⊢ C = (n \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{n})))$
	vonioolem1.d	$⊢ D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [C (n) (k), B (k)))$
	vonioolem1.s	$⊢ S = (n \in ℕ ⟼ voln (X) (D (n)))$
	vonioolem1.r	$⊢ T = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - C (n) (k)))$
	vonioolem1.e	$⊢ E = sup (ran (k \in X ⟼ B (k) - A (k)) ℝ <)$
	vonioolem1.n	$⊢ N = ⌊\frac{1}{E}⌋ + 1$
	vonioolem1.z	$⊢ Z = ℤ_{\geq N}$
Assertion	vonioolem1	$⊢ φ \to S ⇝ \prod_{k \in X} (B (k) - A (k))$

Proof

Step	Hyp	Ref	Expression
1		vonioolem1.x	$⊢ φ \to X \in Fin$
2		vonioolem1.a	$⊢ φ \to A : X ⟶ ℝ$
3		vonioolem1.b	$⊢ φ \to B : X ⟶ ℝ$
4		vonioolem1.u	$⊢ φ \to X \neq \emptyset$
5		vonioolem1.t	$⊢ (φ \land k \in X) \to A (k) < B (k)$
6		vonioolem1.c	$⊢ C = (n \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{n})))$
7		vonioolem1.d	$⊢ D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [C (n) (k), B (k)))$
8		vonioolem1.s	$⊢ S = (n \in ℕ ⟼ voln (X) (D (n)))$
9		vonioolem1.r	$⊢ T = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - C (n) (k)))$
10		vonioolem1.e	$⊢ E = sup (ran (k \in X ⟼ B (k) - A (k)) ℝ <)$
11		vonioolem1.n	$⊢ N = ⌊\frac{1}{E}⌋ + 1$
12		vonioolem1.z	$⊢ Z = ℤ_{\geq N}$
13	9	a1i	$⊢ φ \to T = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - C (n) (k)))$
14	6	a1i	$⊢ φ \to C = (n \in ℕ ⟼ (k \in X ⟼ A (k) + (\frac{1}{n})))$
15	1	mptexd	$⊢ φ \to (k \in X ⟼ A (k) + (\frac{1}{n})) \in V$
16	15	adantr	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ A (k) + (\frac{1}{n})) \in V$
17	14 16	fvmpt2d	$⊢ (φ \land n \in ℕ) \to C (n) = (k \in X ⟼ A (k) + (\frac{1}{n}))$
18		ovexd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) + (\frac{1}{n}) \in V$
19	17 18	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) = A (k) + (\frac{1}{n})$
20	19	oveq2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) - C (n) (k) = B (k) - (A (k) + (\frac{1}{n}))$
21	3	ffvelrnda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
22	21	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℝ$
23	22	recnd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℂ$
24	2	adantr	$⊢ (φ \land n \in ℕ) \to A : X ⟶ ℝ$
25	24	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℝ$
26	25	recnd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℂ$
27		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
28	27	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ$
29	28	recnd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℂ$
30	23 26 29	subsub4d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) - A (k) - (\frac{1}{n}) = B (k) - (A (k) + (\frac{1}{n}))$
31	20 30	eqtr4d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) - C (n) (k) = B (k) - A (k) - (\frac{1}{n})$
32	31	prodeq2dv	$⊢ (φ \land n \in ℕ) \to \prod_{k \in X} (B (k) - C (n) (k)) = \prod_{k \in X} (B (k) - A (k) - (\frac{1}{n}))$
33	32	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ \prod_{k \in X} (B (k) - C (n) (k))) = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) - (\frac{1}{n})))$
34	13 33	eqtrd	$⊢ φ \to T = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) - (\frac{1}{n})))$
35		nfv	$⊢ Ⅎ k φ$
36		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
37	2	ffvelrnda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
38		difrp	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to (A (k) < B (k) \leftrightarrow B (k) - A (k) \in ℝ^{+})$
39	37 21 38	syl2anc	$⊢ (φ \land k \in X) \to (A (k) < B (k) \leftrightarrow B (k) - A (k) \in ℝ^{+})$
40	5 39	mpbid	$⊢ (φ \land k \in X) \to B (k) - A (k) \in ℝ^{+}$
41	36 40	sseldi	$⊢ (φ \land k \in X) \to B (k) - A (k) \in ℝ$
42	41	recnd	$⊢ (φ \land k \in X) \to B (k) - A (k) \in ℂ$
43		eqid	$⊢ (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) - (\frac{1}{n}))) = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) - (\frac{1}{n})))$
44	35 1 42 43	fprodsubrecnncnv	$⊢ φ \to (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) - (\frac{1}{n}))) ⇝ \prod_{k \in X} (B (k) - A (k))$
45	34 44	eqbrtrd	$⊢ φ \to T ⇝ \prod_{k \in X} (B (k) - A (k))$
46		nnex	$⊢ ℕ \in V$
47	46	mptex	$⊢ (n \in ℕ ⟼ \prod_{k \in X} (B (k) - C (n) (k))) \in V$
48	47	a1i	$⊢ φ \to (n \in ℕ ⟼ \prod_{k \in X} (B (k) - C (n) (k))) \in V$
49	9 48	eqeltrid	$⊢ φ \to T \in V$
50	46	mptex	$⊢ (n \in ℕ ⟼ voln (X) (D (n))) \in V$
51	50	a1i	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) \in V$
52	8 51	eqeltrid	$⊢ φ \to S \in V$
53		1rp	$⊢ 1 \in ℝ^{+}$
54	53	a1i	$⊢ φ \to 1 \in ℝ^{+}$
55		eqid	$⊢ (k \in X ⟼ B (k) - A (k)) = (k \in X ⟼ B (k) - A (k))$
56	35 55 40	rnmptssd	$⊢ φ \to ran (k \in X ⟼ B (k) - A (k)) \subseteq ℝ^{+}$
57		ltso	$⊢ < Or ℝ$
58	57	a1i	$⊢ φ \to < Or ℝ$
59	55	rnmptfi	$⊢ X \in Fin \to ran (k \in X ⟼ B (k) - A (k)) \in Fin$
60	1 59	syl	$⊢ φ \to ran (k \in X ⟼ B (k) - A (k)) \in Fin$
61	35 40 55 4	rnmptn0	$⊢ φ \to ran (k \in X ⟼ B (k) - A (k)) \neq \emptyset$
62	36	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
63	56 62	sstrd	$⊢ φ \to ran (k \in X ⟼ B (k) - A (k)) \subseteq ℝ$
64		fiinfcl	$⊢ (< Or ℝ \land (ran (k \in X ⟼ B (k) - A (k)) \in Fin \land ran (k \in X ⟼ B (k) - A (k)) \neq \emptyset \land ran (k \in X ⟼ B (k) - A (k)) \subseteq ℝ)) \to sup (ran (k \in X ⟼ B (k) - A (k)) ℝ <) \in ran (k \in X ⟼ B (k) - A (k))$
65	58 60 61 63 64	syl13anc	$⊢ φ \to sup (ran (k \in X ⟼ B (k) - A (k)) ℝ <) \in ran (k \in X ⟼ B (k) - A (k))$
66	10 65	eqeltrid	$⊢ φ \to E \in ran (k \in X ⟼ B (k) - A (k))$
67	56 66	sseldd	$⊢ φ \to E \in ℝ^{+}$
68	54 67	rpdivcld	$⊢ φ \to \frac{1}{E} \in ℝ^{+}$
69	68	rpred	$⊢ φ \to \frac{1}{E} \in ℝ$
70	68	rpge0d	$⊢ φ \to 0 \leq \frac{1}{E}$
71		flge0nn0	$⊢ (\frac{1}{E} \in ℝ \land 0 \leq \frac{1}{E}) \to ⌊\frac{1}{E}⌋ \in ℕ_{0}$
72	69 70 71	syl2anc	$⊢ φ \to ⌊\frac{1}{E}⌋ \in ℕ_{0}$
73		nn0p1nn	$⊢ ⌊\frac{1}{E}⌋ \in ℕ_{0} \to ⌊\frac{1}{E}⌋ + 1 \in ℕ$
74	72 73	syl	$⊢ φ \to ⌊\frac{1}{E}⌋ + 1 \in ℕ$
75	74	nnzd	$⊢ φ \to ⌊\frac{1}{E}⌋ + 1 \in ℤ$
76	11 75	eqeltrid	$⊢ φ \to N \in ℤ$
77	11	recnnltrp	$⊢ E \in ℝ^{+} \to (N \in ℕ \land \frac{1}{N} < E)$
78	67 77	syl	$⊢ φ \to (N \in ℕ \land \frac{1}{N} < E)$
79	78	simpld	$⊢ φ \to N \in ℕ$
80		uznnssnn	$⊢ N \in ℕ \to ℤ_{\geq N} \subseteq ℕ$
81	79 80	syl	$⊢ φ \to ℤ_{\geq N} \subseteq ℕ$
82	12 81	eqsstrid	$⊢ φ \to Z \subseteq ℕ$
83	82	adantr	$⊢ (φ \land n \in Z) \to Z \subseteq ℕ$
84		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
85	83 84	sseldd	$⊢ (φ \land n \in Z) \to n \in ℕ$
86	7	a1i	$⊢ φ \to D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [C (n) (k), B (k)))$
87	1	adantr	$⊢ (φ \land n \in ℕ) \to X \in Fin$
88		eqid	$⊢ dom voln (X) = dom voln (X)$
89	25 28	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) + (\frac{1}{n}) \in ℝ$
90	89	fmpttd	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ A (k) + (\frac{1}{n})) : X ⟶ ℝ$
91	17	feq1d	$⊢ (φ \land n \in ℕ) \to (C (n) : X ⟶ ℝ \leftrightarrow (k \in X ⟼ A (k) + (\frac{1}{n})) : X ⟶ ℝ)$
92	90 91	mpbird	$⊢ (φ \land n \in ℕ) \to C (n) : X ⟶ ℝ$
93	3	adantr	$⊢ (φ \land n \in ℕ) \to B : X ⟶ ℝ$
94	87 88 92 93	hoimbl	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [C (n) (k), B (k)) \in dom voln (X)$
95	94	elexd	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [C (n) (k), B (k)) \in V$
96	86 95	fvmpt2d	$⊢ (φ \land n \in ℕ) \to D (n) = \underset{k \in X}{⨉} [C (n) (k), B (k))$
97	85 96	syldan	$⊢ (φ \land n \in Z) \to D (n) = \underset{k \in X}{⨉} [C (n) (k), B (k))$
98	97	fveq2d	$⊢ (φ \land n \in Z) \to voln (X) (D (n)) = voln (X) (\underset{k \in X}{⨉} [C (n) (k), B (k)))$
99	1	adantr	$⊢ (φ \land n \in Z) \to X \in Fin$
100	4	adantr	$⊢ (φ \land n \in Z) \to X \neq \emptyset$
101	85 92	syldan	$⊢ (φ \land n \in Z) \to C (n) : X ⟶ ℝ$
102	3	adantr	$⊢ (φ \land n \in Z) \to B : X ⟶ ℝ$
103		eqid	$⊢ \underset{k \in X}{⨉} [C (n) (k), B (k)) = \underset{k \in X}{⨉} [C (n) (k), B (k))$
104	99 100 101 102 103	vonn0hoi	$⊢ (φ \land n \in Z) \to voln (X) (\underset{k \in X}{⨉} [C (n) (k), B (k))) = \prod_{k \in X} vol ([C (n) (k), B (k)))$
105	101	ffvelrnda	$⊢ ((φ \land n \in Z) \land k \in X) \to C (n) (k) \in ℝ$
106	85 22	syldanl	$⊢ ((φ \land n \in Z) \land k \in X) \to B (k) \in ℝ$
107		volico	$⊢ (C (n) (k) \in ℝ \land B (k) \in ℝ) \to vol ([C (n) (k), B (k))) = if (C (n) (k) < B (k), B (k) - C (n) (k), 0)$
108	105 106 107	syl2anc	$⊢ ((φ \land n \in Z) \land k \in X) \to vol ([C (n) (k), B (k))) = if (C (n) (k) < B (k), B (k) - C (n) (k), 0)$
109	85 19	syldanl	$⊢ ((φ \land n \in Z) \land k \in X) \to C (n) (k) = A (k) + (\frac{1}{n})$
110	85 28	syldanl	$⊢ ((φ \land n \in Z) \land k \in X) \to \frac{1}{n} \in ℝ$
111	79	nnrecred	$⊢ φ \to \frac{1}{N} \in ℝ$
112	111	ad2antrr	$⊢ ((φ \land n \in Z) \land k \in X) \to \frac{1}{N} \in ℝ$
113	41	adantlr	$⊢ ((φ \land n \in Z) \land k \in X) \to B (k) - A (k) \in ℝ$
114	12	eleq2i	$⊢ n \in Z \leftrightarrow n \in ℤ_{\geq N}$
115	114	biimpi	$⊢ n \in Z \to n \in ℤ_{\geq N}$
116		eluzle	$⊢ n \in ℤ_{\geq N} \to N \leq n$
117	115 116	syl	$⊢ n \in Z \to N \leq n$
118	117	adantl	$⊢ (φ \land n \in Z) \to N \leq n$
119	79	nnrpd	$⊢ φ \to N \in ℝ^{+}$
120	119	adantr	$⊢ (φ \land n \in Z) \to N \in ℝ^{+}$
121		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
122	85 121	syl	$⊢ (φ \land n \in Z) \to n \in ℝ^{+}$
123	120 122	lerecd	$⊢ (φ \land n \in Z) \to (N \leq n \leftrightarrow \frac{1}{n} \leq \frac{1}{N})$
124	118 123	mpbid	$⊢ (φ \land n \in Z) \to \frac{1}{n} \leq \frac{1}{N}$
125	124	adantr	$⊢ ((φ \land n \in Z) \land k \in X) \to \frac{1}{n} \leq \frac{1}{N}$
126	111	adantr	$⊢ (φ \land k \in X) \to \frac{1}{N} \in ℝ$
127	36 67	sseldi	$⊢ φ \to E \in ℝ$
128	127	adantr	$⊢ (φ \land k \in X) \to E \in ℝ$
129	78	simprd	$⊢ φ \to \frac{1}{N} < E$
130	129	adantr	$⊢ (φ \land k \in X) \to \frac{1}{N} < E$
131	63	adantr	$⊢ (φ \land k \in X) \to ran (k \in X ⟼ B (k) - A (k)) \subseteq ℝ$
132	60	adantr	$⊢ (φ \land k \in X) \to ran (k \in X ⟼ B (k) - A (k)) \in Fin$
133		id	$⊢ k \in X \to k \in X$
134		ovexd	$⊢ k \in X \to B (k) - A (k) \in V$
135	55	elrnmpt1	$⊢ (k \in X \land B (k) - A (k) \in V) \to B (k) - A (k) \in ran (k \in X ⟼ B (k) - A (k))$
136	133 134 135	syl2anc	$⊢ k \in X \to B (k) - A (k) \in ran (k \in X ⟼ B (k) - A (k))$
137	136	adantl	$⊢ (φ \land k \in X) \to B (k) - A (k) \in ran (k \in X ⟼ B (k) - A (k))$
138		infrefilb	$⊢ (ran (k \in X ⟼ B (k) - A (k)) \subseteq ℝ \land ran (k \in X ⟼ B (k) - A (k)) \in Fin \land B (k) - A (k) \in ran (k \in X ⟼ B (k) - A (k))) \to sup (ran (k \in X ⟼ B (k) - A (k)) ℝ <) \leq B (k) - A (k)$
139	131 132 137 138	syl3anc	$⊢ (φ \land k \in X) \to sup (ran (k \in X ⟼ B (k) - A (k)) ℝ <) \leq B (k) - A (k)$
140	10 139	eqbrtrid	$⊢ (φ \land k \in X) \to E \leq B (k) - A (k)$
141	126 128 41 130 140	ltletrd	$⊢ (φ \land k \in X) \to \frac{1}{N} < B (k) - A (k)$
142	141	adantlr	$⊢ ((φ \land n \in Z) \land k \in X) \to \frac{1}{N} < B (k) - A (k)$
143	110 112 113 125 142	lelttrd	$⊢ ((φ \land n \in Z) \land k \in X) \to \frac{1}{n} < B (k) - A (k)$
144	85 25	syldanl	$⊢ ((φ \land n \in Z) \land k \in X) \to A (k) \in ℝ$
145	144 110 106	ltaddsub2d	$⊢ ((φ \land n \in Z) \land k \in X) \to (A (k) + (\frac{1}{n}) < B (k) \leftrightarrow \frac{1}{n} < B (k) - A (k))$
146	143 145	mpbird	$⊢ ((φ \land n \in Z) \land k \in X) \to A (k) + (\frac{1}{n}) < B (k)$
147	109 146	eqbrtrd	$⊢ ((φ \land n \in Z) \land k \in X) \to C (n) (k) < B (k)$
148	147	iftrued	$⊢ ((φ \land n \in Z) \land k \in X) \to if (C (n) (k) < B (k), B (k) - C (n) (k), 0) = B (k) - C (n) (k)$
149	108 148	eqtrd	$⊢ ((φ \land n \in Z) \land k \in X) \to vol ([C (n) (k), B (k))) = B (k) - C (n) (k)$
150	149	prodeq2dv	$⊢ (φ \land n \in Z) \to \prod_{k \in X} vol ([C (n) (k), B (k))) = \prod_{k \in X} (B (k) - C (n) (k))$
151	98 104 150	3eqtrd	$⊢ (φ \land n \in Z) \to voln (X) (D (n)) = \prod_{k \in X} (B (k) - C (n) (k))$
152		fvexd	$⊢ (φ \land n \in Z) \to voln (X) (D (n)) \in V$
153	8	fvmpt2	$⊢ (n \in ℕ \land voln (X) (D (n)) \in V) \to S (n) = voln (X) (D (n))$
154	85 152 153	syl2anc	$⊢ (φ \land n \in Z) \to S (n) = voln (X) (D (n))$
155		prodex	$⊢ \prod_{k \in X} (B (k) - C (n) (k)) \in V$
156	155	a1i	$⊢ (φ \land n \in Z) \to \prod_{k \in X} (B (k) - C (n) (k)) \in V$
157	9	fvmpt2	$⊢ (n \in ℕ \land \prod_{k \in X} (B (k) - C (n) (k)) \in V) \to T (n) = \prod_{k \in X} (B (k) - C (n) (k))$
158	85 156 157	syl2anc	$⊢ (φ \land n \in Z) \to T (n) = \prod_{k \in X} (B (k) - C (n) (k))$
159	151 154 158	3eqtr4rd	$⊢ (φ \land n \in Z) \to T (n) = S (n)$
160	12 49 52 76 159	climeq	$⊢ φ \to (T ⇝ \prod_{k \in X} (B (k) - A (k)) \leftrightarrow S ⇝ \prod_{k \in X} (B (k) - A (k)))$
161	45 160	mpbid	$⊢ φ \to S ⇝ \prod_{k \in X} (B (k) - A (k))$

Metamath Proof Explorer

Theorem vonioolem1

Proof