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		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) = +∞$
44		nfv	$⊢ Ⅎ k vol (A) = +∞$
45		nfcv	$⊢ \underline{Ⅎ} n vol$
46		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ k / n ⦌ A$
47	45 46	nffv	$⊢ \underline{Ⅎ} n vol (⦋ k / n ⦌ A)$
48	47	nfeq1	$⊢ Ⅎ n vol (⦋ k / n ⦌ A) = +∞$
49		csbeq1a	$⊢ n = k \to A = ⦋ k / n ⦌ A$
50	49	fveqeq2d	$⊢ n = k \to (vol (A) = +∞ \leftrightarrow vol (⦋ k / n ⦌ A) = +∞)$
51	44 48 50	cbvrexw	$⊢ \exists n \in ℕ vol (A) = +∞ \leftrightarrow \exists k \in ℕ vol (⦋ k / n ⦌ A) = +∞$
52	43 51	sylib	$⊢ ((\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) = +∞$
53	46	nfel1	$⊢ Ⅎ n ⦋ k / n ⦌ A \in dom vol$
54	49	eleq1d	$⊢ n = k \to (A \in dom vol \leftrightarrow ⦋ k / n ⦌ A \in dom vol)$
55	53 54	rspc	$⊢ k \in ℕ \to (\forall n \in ℕ A \in dom vol \to ⦋ k / n ⦌ A \in dom vol)$
56	55	impcom	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⦋ k / n ⦌ A \in dom vol$
57		iunmbl	$⊢ \forall n \in ℕ A \in dom vol \to ⋃_{n \in ℕ} A \in dom vol$
58	57	adantr	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⋃_{n \in ℕ} A \in dom vol$
59		nfcv	$⊢ \underline{Ⅎ} n ℕ$
60		nfcv	$⊢ \underline{Ⅎ} n k$
61	59 60 46 49	ssiun2sf	$⊢ k \in ℕ \to ⦋ k / n ⦌ A \subseteq ⋃_{n \in ℕ} A$
62	61	adantl	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⦋ k / n ⦌ A \subseteq ⋃_{n \in ℕ} A$
63		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)$
64	56 58 62 63	syl3anc	$⊢ (\forall n \in ℕ A \in dom vol \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 k \in ℕ) \to vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)$
66	65	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)$
67	66	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)$
68		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))$
69	52 67 68	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))$
70		breq1	$⊢ vol (⦋ k / n ⦌ A) = +∞ \to (vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A) \leftrightarrow +∞ \leq vol (⋃_{n \in ℕ} A))$
71	70	biimpa	$⊢ (vol (⦋ k / n ⦌ A) = +∞ \land vol (⦋ k / n ⦌ A) \leq vol (⋃_{n \in ℕ} A)) \to +∞ \leq vol (⋃_{n \in ℕ} A)$
72	71	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)$
73	69 72	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)$
74		1nn	$⊢ 1 \in ℕ$
75		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
76		r19.9rzv	$⊢ ℕ \neq \emptyset \to (+∞ \leq vol (⋃_{n \in ℕ} A) \leftrightarrow \exists k \in ℕ +∞ \leq vol (⋃_{n \in ℕ} A))$
77	74 75 76	mp2b	$⊢ +∞ \leq vol (⋃_{n \in ℕ} A) \leftrightarrow \exists k \in ℕ +∞ \leq vol (⋃_{n \in ℕ} A)$
78	73 77	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)$
79		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
80	12	ffvelcdmi	$⊢ ⋃_{n \in ℕ} A \in dom vol \to vol (⋃_{n \in ℕ} A) \in [0, +∞]$
81	79 80	sselid	$⊢ ⋃_{n \in ℕ} A \in dom vol \to vol (⋃_{n \in ℕ} A) \in ℝ^{*}$
82	57 81	syl	$⊢ \forall n \in ℕ A \in dom vol \to vol (⋃_{n \in ℕ} A) \in ℝ^{*}$
83	82	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 ℝ^{*}$
84		xgepnf	$⊢ vol (⋃_{n \in ℕ} A) \in ℝ^{*} \to (+∞ \leq vol (⋃_{n \in ℕ} A) \leftrightarrow vol (⋃_{n \in ℕ} A) = +∞)$
85	83 84	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) = +∞)$
86	78 85	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) = +∞$
87		nfdisj1	$⊢ Ⅎ n \underset{n \in ℕ}{Disj} A$
88	7 87	nfan	$⊢ Ⅎ n (\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A)$
89		nfre1	$⊢ Ⅎ n \exists n \in ℕ vol (A) = +∞$
90	88 89	nfan	$⊢ Ⅎ n ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞)$
91		nnex	$⊢ ℕ \in V$
92	91	a1i	$⊢ ((\forall n \in ℕ A \in dom vol \land \underset{n \in ℕ}{Disj} A) \land \exists n \in ℕ vol (A) = +∞) \to ℕ \in V$
93	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, +∞]$
94	93	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, +∞]$
95	90 92 94 43	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	86 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