vonicclem1

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

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

Proof

Step	Hyp	Ref	Expression
1		vonicclem1.x	$⊢ φ \to X \in Fin$
2		vonicclem1.a	$⊢ φ \to A : X ⟶ ℝ$
3		vonicclem1.b	$⊢ φ \to B : X ⟶ ℝ$
4		vonicclem1.u	$⊢ φ \to X \neq \emptyset$
5		vonicclem1.t	$⊢ (φ \land k \in X) \to A (k) \leq B (k)$
6		vonicclem1.c	$⊢ C = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
7		vonicclem1.d	$⊢ D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), C (n) (k)))$
8		vonicclem1.s	$⊢ S = (n \in ℕ ⟼ voln (X) (D (n)))$
9	8	a1i	$⊢ φ \to S = (n \in ℕ ⟼ voln (X) (D (n)))$
10		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
11	7	a1i	$⊢ φ \to D = (n \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), C (n) (k)))$
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	3	ffvelrnda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
16	15	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℝ$
17		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
18	17	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ$
19	16 18	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) + (\frac{1}{n}) \in ℝ$
20	19	fmpttd	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ B (k) + (\frac{1}{n})) : X ⟶ ℝ$
21	6	a1i	$⊢ φ \to C = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
22	1	mptexd	$⊢ φ \to (k \in X ⟼ B (k) + (\frac{1}{n})) \in V$
23	22	adantr	$⊢ (φ \land n \in ℕ) \to (k \in X ⟼ B (k) + (\frac{1}{n})) \in V$
24	21 23	fvmpt2d	$⊢ (φ \land n \in ℕ) \to C (n) = (k \in X ⟼ B (k) + (\frac{1}{n}))$
25	24	feq1d	$⊢ (φ \land n \in ℕ) \to (C (n) : X ⟶ ℝ \leftrightarrow (k \in X ⟼ B (k) + (\frac{1}{n})) : X ⟶ ℝ)$
26	20 25	mpbird	$⊢ (φ \land n \in ℕ) \to C (n) : X ⟶ ℝ$
27	12 13 14 26	hoimbl	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k), C (n) (k)) \in dom voln (X)$
28	27	elexd	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A (k), C (n) (k)) \in V$
29	11 28	fvmpt2d	$⊢ (φ \land n \in ℕ) \to D (n) = \underset{k \in X}{⨉} [A (k), C (n) (k))$
30	10 29	syldan	$⊢ (φ \land n \in ℕ) \to D (n) = \underset{k \in X}{⨉} [A (k), C (n) (k))$
31	30	fveq2d	$⊢ (φ \land n \in ℕ) \to voln (X) (D (n)) = voln (X) (\underset{k \in X}{⨉} [A (k), C (n) (k)))$
32	4	adantr	$⊢ (φ \land n \in ℕ) \to X \neq \emptyset$
33	10 26	syldan	$⊢ (φ \land n \in ℕ) \to C (n) : X ⟶ ℝ$
34		eqid	$⊢ \underset{k \in X}{⨉} [A (k), C (n) (k)) = \underset{k \in X}{⨉} [A (k), C (n) (k))$
35	12 32 14 33 34	vonn0hoi	$⊢ (φ \land n \in ℕ) \to voln (X) (\underset{k \in X}{⨉} [A (k), C (n) (k))) = \prod_{k \in X} vol ([A (k), C (n) (k)))$
36	14	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℝ$
37	10 36	syldanl	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℝ$
38	33	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) \in ℝ$
39		volico	$⊢ (A (k) \in ℝ \land C (n) (k) \in ℝ) \to vol ([A (k), C (n) (k))) = if (A (k) < C (n) (k), C (n) (k) - A (k), 0)$
40	37 38 39	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to vol ([A (k), C (n) (k))) = if (A (k) < C (n) (k), C (n) (k) - A (k), 0)$
41	10 16	syldanl	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℝ$
42	5	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \leq B (k)$
43		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
44	43	rpreccld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
45	44	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ^{+}$
46	41 45	ltaddrpd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) < B (k) + (\frac{1}{n})$
47	19	elexd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) + (\frac{1}{n}) \in V$
48	24 47	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) = B (k) + (\frac{1}{n})$
49	10 48	syldanl	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) = B (k) + (\frac{1}{n})$
50	46 49	breqtrrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) < C (n) (k)$
51	37 41 38 42 50	lelttrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) < C (n) (k)$
52	51	iftrued	$⊢ ((φ \land n \in ℕ) \land k \in X) \to if (A (k) < C (n) (k), C (n) (k) - A (k), 0) = C (n) (k) - A (k)$
53	40 52	eqtrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to vol ([A (k), C (n) (k))) = C (n) (k) - A (k)$
54	53	prodeq2dv	$⊢ (φ \land n \in ℕ) \to \prod_{k \in X} vol ([A (k), C (n) (k))) = \prod_{k \in X} (C (n) (k) - A (k))$
55	31 35 54	3eqtrd	$⊢ (φ \land n \in ℕ) \to voln (X) (D (n)) = \prod_{k \in X} (C (n) (k) - A (k))$
56	48	oveq1d	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) - A (k) = B (k) + (\frac{1}{n}) - A (k)$
57	16	recnd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) \in ℂ$
58	18	recnd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℂ$
59	36	recnd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A (k) \in ℂ$
60	57 58 59	addsubd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B (k) + (\frac{1}{n}) - A (k) = B (k) - A (k) + (\frac{1}{n})$
61	56 60	eqtrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C (n) (k) - A (k) = B (k) - A (k) + (\frac{1}{n})$
62	61	prodeq2dv	$⊢ (φ \land n \in ℕ) \to \prod_{k \in X} (C (n) (k) - A (k)) = \prod_{k \in X} (B (k) - A (k) + (\frac{1}{n}))$
63	55 62	eqtrd	$⊢ (φ \land n \in ℕ) \to voln (X) (D (n)) = \prod_{k \in X} (B (k) - A (k) + (\frac{1}{n}))$
64	63	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ voln (X) (D (n))) = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) + (\frac{1}{n})))$
65	9 64	eqtrd	$⊢ φ \to S = (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) + (\frac{1}{n})))$
66		nfv	$⊢ Ⅎ k φ$
67	2	ffvelrnda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
68	15 67	resubcld	$⊢ (φ \land k \in X) \to B (k) - A (k) \in ℝ$
69	68	recnd	$⊢ (φ \land k \in X) \to B (k) - A (k) \in ℂ$
70		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})))$
71	66 1 69 70	fprodaddrecnncnv	$⊢ φ \to (n \in ℕ ⟼ \prod_{k \in X} (B (k) - A (k) + (\frac{1}{n}))) ⇝ \prod_{k \in X} (B (k) - A (k))$
72	65 71	eqbrtrd	$⊢ φ \to S ⇝ \prod_{k \in X} (B (k) - A (k))$

Metamath Proof Explorer

Theorem vonicclem1

Proof