voliune

Description: The Lebesgue measure function is countably additive. This formulation on the extended reals, allows for +oo for the measure of any set in the sum. Cf. ovoliun and voliun . (Contributed by Thierry Arnoux, 16-Oct-2017)

		Ref	Expression
	Assertion	voliune	$⊢ (\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \to vol (⋃_{n \in ℕ} A) = \underset{n \in ℕ}{\sum^{*}} vol (A)$

Proof

Step	Hyp	Ref	Expression
1		r19.26	$⊢ \forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \leftrightarrow (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ)$
2		eqid	$⊢ seq 1 (+ (n \in ℕ ⟼ vol (A))) = seq 1 (+ (n \in ℕ ⟼ vol (A)))$
3		eqid	$⊢ (n \in ℕ ⟼ vol (A)) = (n \in ℕ ⟼ vol (A))$
4	2 3	voliun	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to vol (⋃_{n \in ℕ} A) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (A))) ℝ^{*} <)$
5	1 4	sylanbr	$⊢ ((\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to vol (⋃_{n \in ℕ} A) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (A))) ℝ^{*} <)$
6	5	an32s	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \forall n \in ℕ vol (A) \in ℝ) \to vol (⋃_{n \in ℕ} A) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (A))) ℝ^{*} <)$
7		nfra1	$⊢ Ⅎ n \forall n \in ℕ A \in dom vol$
8		nfra1	$⊢ Ⅎ n \forall n \in ℕ vol (A) \in ℝ$
9	7 8	nfan	$⊢ Ⅎ n (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ)$
10		simpr	$⊢ (\forall n \in ℕ A \in dom vol \land n \in ℕ) \to n \in ℕ$
11		rspa	$⊢ (\forall n \in ℕ A \in dom vol \land n \in ℕ) \to A \in dom vol$
12		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
13	12	ffvelcdmi	$⊢ A \in dom vol \to vol (A) \in [0, +∞]$
14	11 13	syl	$⊢ (\forall n \in ℕ A \in dom vol \land n \in ℕ) \to vol (A) \in [0, +∞]$
15	3	fvmpt2	$⊢ (n \in ℕ \land vol (A) \in [0, +∞]) \to (n \in ℕ ⟼ vol (A)) (n) = vol (A)$
16	10 14 15	syl2anc	$⊢ (\forall n \in ℕ A \in dom vol \land n \in ℕ) \to (n \in ℕ ⟼ vol (A)) (n) = vol (A)$
17	16	adantlr	$⊢ ((\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \land n \in ℕ) \to (n \in ℕ ⟼ vol (A)) (n) = vol (A)$
18	17	ex	$⊢ (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \to (n \in ℕ \to (n \in ℕ ⟼ vol (A)) (n) = vol (A))$
19	9 18	ralrimi	$⊢ (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \to \forall n \in ℕ (n \in ℕ ⟼ vol (A)) (n) = vol (A)$
20	9 19	esumeq2d	$⊢ (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \to \underset{n \in ℕ}{\sum^{}} (n \in ℕ ⟼ vol (A)) (n) = \underset{n \in ℕ}{\sum^{}} vol (A)$
21		simpr	$⊢ (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \to \forall n \in ℕ vol (A) \in ℝ$
22	21	r19.21bi	$⊢ ((\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \land n \in ℕ) \to vol (A) \in ℝ$
23	14	adantlr	$⊢ ((\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \land n \in ℕ) \to vol (A) \in [0, +∞]$
24		0xr	$⊢ 0 \in ℝ^{*}$
25		pnfxr	$⊢ +∞ \in ℝ^{*}$
26		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (vol (A) \in [0, +∞] \leftrightarrow (vol (A) \in ℝ^{*} \land 0 \leq vol (A) \land vol (A) \leq +∞))$
27	24 25 26	mp2an	$⊢ vol (A) \in [0, +∞] \leftrightarrow (vol (A) \in ℝ^{*} \land 0 \leq vol (A) \land vol (A) \leq +∞)$
28	27	simp2bi	$⊢ vol (A) \in [0, +∞] \to 0 \leq vol (A)$
29	23 28	syl	$⊢ ((\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \land n \in ℕ) \to 0 \leq vol (A)$
30		ltpnf	$⊢ vol (A) \in ℝ \to vol (A) < +∞$
31	22 30	syl	$⊢ ((\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \land n \in ℕ) \to vol (A) < +∞$
32		0re	$⊢ 0 \in ℝ$
33		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (vol (A) \in [0, +∞) \leftrightarrow (vol (A) \in ℝ \land 0 \leq vol (A) \land vol (A) < +∞))$
34	32 25 33	mp2an	$⊢ vol (A) \in [0, +∞) \leftrightarrow (vol (A) \in ℝ \land 0 \leq vol (A) \land vol (A) < +∞)$
35	22 29 31 34	syl3anbrc	$⊢ ((\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \land n \in ℕ) \to vol (A) \in [0, +∞)$
36	9 35 3	fmptdf	$⊢ (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \to (n \in ℕ ⟼ vol (A)) : ℕ ⟶ [0, +∞)$
37		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ vol (A))$
38	37	esumfsupre	$⊢ (n \in ℕ ⟼ vol (A)) : ℕ ⟶ [0, +∞) \to \underset{n \in ℕ}{\sum^{}} (n \in ℕ ⟼ vol (A)) (n) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (A))) ℝ^{} <)$
39	36 38	syl	$⊢ (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \to \underset{n \in ℕ}{\sum^{}} (n \in ℕ ⟼ vol (A)) (n) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (A))) ℝ^{} <)$
40	20 39	eqtr3d	$⊢ (\forall n \in ℕ A \in dom vol \land \forall n \in ℕ vol (A) \in ℝ) \to \underset{n \in ℕ}{\sum^{}} vol (A) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (A))) ℝ^{} <)$
41	40	adantlr	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \forall n \in ℕ vol (A) \in ℝ) \to \underset{n \in ℕ}{\sum^{}} vol (A) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol (A))) ℝ^{} <)$
42	6 41	eqtr4d	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \forall n \in ℕ vol (A) \in ℝ) \to vol (⋃_{n \in ℕ} A) = \underset{n \in ℕ}{\sum^{*}} vol (A)$
43		nfv	$⊢ Ⅎ k vol (A) = +∞$
44		nfcv	$⊢ \underline{Ⅎ} n vol$
45		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ k / n ⦌ A$
46	44 45	nffv	$⊢ \underline{Ⅎ} n vol (⦋ k / n ⦌ A)$
47	46	nfeq1	$⊢ Ⅎ n vol (⦋ k / n ⦌ A) = +∞$
48		csbeq1a	$⊢ n = k \to A = ⦋ k / n ⦌ A$
49	48	fveqeq2d	$⊢ n = k \to (vol (A) = +∞ \leftrightarrow vol (⦋ k / n ⦌ A) = +∞)$
50	43 47 49	cbvrexw	$⊢ \exists n \in ℕ vol (A) = +∞ \leftrightarrow \exists k \in ℕ vol (⦋ k / n ⦌ A) = +∞$
51	50	bilani	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to \exists k \in ℕ vol (⦋ k / n ⦌ A) = +∞$
52	45	nfel1	$⊢ Ⅎ n ⦋ k / n ⦌ A \in dom vol$
53	48	eleq1d	$⊢ n = k \to (A \in dom vol \leftrightarrow ⦋ k / n ⦌ A \in dom vol)$
54	52 53	rspc	$⊢ k \in ℕ \to (\forall n \in ℕ A \in dom vol \to ⦋ k / n ⦌ A \in dom vol)$
55	54	impcom	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⦋ k / n ⦌ A \in dom vol$
56		iunmbl	$⊢ \forall n \in ℕ A \in dom vol \to ⋃_{n \in ℕ} A \in dom vol$
57	56	adantr	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⋃_{n \in ℕ} A \in dom vol$
58		nfcv	$⊢ \underline{Ⅎ} n ℕ$
59		nfcv	$⊢ \underline{Ⅎ} n k$
60	58 59 45 48	ssiun2sf	$⊢ k \in ℕ \to ⦋ k / n ⦌ A \subseteq ⋃_{n \in ℕ} A$
61	60	adantl	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⦋ k / n ⦌ A \subseteq ⋃_{n \in ℕ} A$
62		volss	$⊢ (⦋ k / n ⦌ A \in dom vol \land ⋃_{n \in ℕ} A \in dom vol \land ⦋ k / n ⦌ A \subseteq ⋃_{n \in ℕ} A) \to vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)$
63	55 57 61 62	syl3anc	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)$
64	63	adantlr	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land k \in ℕ) \to vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)$
65	64	adantlr	$⊢ (((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \land k \in ℕ) \to vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)$
66	65	ralrimiva	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to \forall k \in ℕ vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)$
67		r19.29r	$⊢ (\exists k \in ℕ vol (⦋ k / n ⦌ A) = +∞ \land \forall k \in ℕ vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)) \to \exists k \in ℕ (vol (⦋ k / n ⦌ A) = +∞ \land vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A))$
68	51 66 67	syl2anc	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to \exists k \in ℕ (vol (⦋ k / n ⦌ A) = +∞ \land vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A))$
69		breq1	$⊢ vol (⦋ k / n ⦌ A) = +∞ \to (vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A) \leftrightarrow +∞ \leq vol (⋃_{n \in ℕ} A))$
70	69	biimpa	$⊢ (vol (⦋ k / n ⦌ A) = +∞ \land vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)) \to +∞ \leq vol (⋃_{n \in ℕ} A)$
71	70	reximi	$⊢ \exists k \in ℕ (vol (⦋ k / n ⦌ A) = +∞ \land vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)) \to \exists k \in ℕ +∞ \leq vol (⋃_{n \in ℕ} A)$
72	68 71	syl	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to \exists k \in ℕ +∞ \leq vol (⋃_{n \in ℕ} A)$
73		1nn	$⊢ 1 \in ℕ$
74		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
75		r19.9rzv	$⊢ ℕ \neq \emptyset \to (+∞ \leq vol (⋃_{n \in ℕ} A) \leftrightarrow \exists k \in ℕ +∞ \leq vol (⋃_{n \in ℕ} A))$
76	73 74 75	mp2b	$⊢ +∞ \leq vol (⋃_{n \in ℕ} A) \leftrightarrow \exists k \in ℕ +∞ \leq vol (⋃_{n \in ℕ} A)$
77	72 76	sylibr	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to +∞ \leq vol (⋃_{n \in ℕ} A)$
78		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
79	12	ffvelcdmi	$⊢ ⋃_{n \in ℕ} A \in dom vol \to vol (⋃_{n \in ℕ} A) \in [0, +∞]$
80	78 79	sselid	$⊢ ⋃_{n \in ℕ} A \in dom vol \to vol (⋃_{n \in ℕ} A) \in ℝ^{*}$
81	56 80	syl	$⊢ \forall n \in ℕ A \in dom vol \to vol (⋃_{n \in ℕ} A) \in ℝ^{*}$
82	81	ad2antrr	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to vol (⋃_{n \in ℕ} A) \in ℝ^{*}$
83		xgepnf	$⊢ vol (⋃_{n \in ℕ} A) \in ℝ^{*} \to (+∞ \leq vol (⋃_{n \in ℕ} A) \leftrightarrow vol (⋃_{n \in ℕ} A) = +∞)$
84	82 83	syl	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to (+∞ \leq vol (⋃_{n \in ℕ} A) \leftrightarrow vol (⋃_{n \in ℕ} A) = +∞)$
85	77 84	mpbid	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to vol (⋃_{n \in ℕ} A) = +∞$
86		nfdisj1	$⊢ Ⅎ n \underset{n \in ℕ}{Disj} A$
87	7 86	nfan	$⊢ Ⅎ n (\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A)$
88		nfre1	$⊢ Ⅎ n \exists n \in ℕ vol (A) = +∞$
89	87 88	nfan	$⊢ Ⅎ n ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞)$
90		nnex	$⊢ ℕ \in V$
91	90	a1i	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to ℕ \in V$
92	14	3ad2antr3	$⊢ (\forall n \in ℕ A \in dom vol \land (\underset{n \in ℕ}{Disj} A \land \exists n \in ℕ vol (A) = +∞ \land n \in ℕ)) \to vol (A) \in [0, +∞]$
93	92	3anassrs	$⊢ (((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \land n \in ℕ) \to vol (A) \in [0, +∞]$
94		simpr	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to \exists n \in ℕ vol (A) = +∞$
95	89 91 93 94	esumpinfval	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to \underset{n \in ℕ}{\sum^{*}} vol (A) = +∞$
96	85 95	eqtr4d	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to vol (⋃_{n \in ℕ} A) = \underset{n \in ℕ}{\sum^{*}} vol (A)$
97		exmid	$⊢ (\forall n \in ℕ vol (A) \in ℝ \lor \neg \forall n \in ℕ vol (A) \in ℝ)$
98		rexnal	$⊢ \exists n \in ℕ \neg vol (A) \in ℝ \leftrightarrow \neg \forall n \in ℕ vol (A) \in ℝ$
99	98	orbi2i	$⊢ (\forall n \in ℕ vol (A) \in ℝ \lor \exists n \in ℕ \neg vol (A) \in ℝ) \leftrightarrow (\forall n \in ℕ vol (A) \in ℝ \lor \neg \forall n \in ℕ vol (A) \in ℝ)$
100	97 99	mpbir	$⊢ (\forall n \in ℕ vol (A) \in ℝ \lor \exists n \in ℕ \neg vol (A) \in ℝ)$
101		r19.29	$⊢ (\forall n \in ℕ A \in dom vol \land \exists n \in ℕ \neg vol (A) \in ℝ) \to \exists n \in ℕ (A \in dom vol \land \neg vol (A) \in ℝ)$
102		xrge0nre	$⊢ (vol (A) \in [0, +∞] \land \neg vol (A) \in ℝ) \to vol (A) = +∞$
103	13 102	sylan	$⊢ (A \in dom vol \land \neg vol (A) \in ℝ) \to vol (A) = +∞$
104	103	reximi	$⊢ \exists n \in ℕ (A \in dom vol \land \neg vol (A) \in ℝ) \to \exists n \in ℕ vol (A) = +∞$
105	101 104	syl	$⊢ (\forall n \in ℕ A \in dom vol \land \exists n \in ℕ \neg vol (A) \in ℝ) \to \exists n \in ℕ vol (A) = +∞$
106	105	ex	$⊢ \forall n \in ℕ A \in dom vol \to (\exists n \in ℕ \neg vol (A) \in ℝ \to \exists n \in ℕ vol (A) = +∞)$
107	106	orim2d	$⊢ \forall n \in ℕ A \in dom vol \to ((\forall n \in ℕ vol (A) \in ℝ \lor \exists n \in ℕ \neg vol (A) \in ℝ) \to (\forall n \in ℕ vol (A) \in ℝ \lor \exists n \in ℕ vol (A) = +∞))$
108	100 107	mpi	$⊢ \forall n \in ℕ A \in dom vol \to (\forall n \in ℕ vol (A) \in ℝ \lor \exists n \in ℕ vol (A) = +∞)$
109	108	adantr	$⊢ (\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \to (\forall n \in ℕ vol (A) \in ℝ \lor \exists n \in ℕ vol (A) = +∞)$
110	42 96 109	mpjaodan	$⊢ (\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \to vol (⋃_{n \in ℕ} A) = \underset{n \in ℕ}{\sum^{*}} vol (A)$

Metamath Proof Explorer

Theorem voliune

Proof