ovoliun2

Description: The Lebesgue outer measure function is countably sub-additive. (This version is a little easier to read, but does not allow infinite values like ovoliun .) (Contributed by Mario Carneiro, 12-Jun-2014)

	Ref	Expression
Hypotheses	ovoliun.t	$⊢ T = seq 1 (+ G)$
	ovoliun.g	$⊢ G = (n \in ℕ ⟼ {vol}^{*} (A))$
	ovoliun.a	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
	ovoliun.v	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
	ovoliun2.t	$⊢ φ \to T \in dom ⇝$
Assertion	ovoliun2	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \leq \sum_{n \in ℕ} {vol}^{} (A)$

Proof

Step	Hyp	Ref	Expression
1		ovoliun.t	$⊢ T = seq 1 (+ G)$
2		ovoliun.g	$⊢ G = (n \in ℕ ⟼ {vol}^{*} (A))$
3		ovoliun.a	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
4		ovoliun.v	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
5		ovoliun2.t	$⊢ φ \to T \in dom ⇝$
6	1 2 3 4	ovoliun	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \leq sup (ran T ℝ^{} <)$
7		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
8		1zzd	$⊢ φ \to 1 \in ℤ$
9		fvex	$⊢ {vol}^{*} (⦋ m / n ⦌ A) \in V$
10		nfcv	$⊢ \underline{Ⅎ} m {vol}^{*} (A)$
11		nfcv	$⊢ \underline{Ⅎ} n {vol}^{*}$
12		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ m / n ⦌ A$
13	11 12	nffv	$⊢ \underline{Ⅎ} n {vol}^{*} (⦋ m / n ⦌ A)$
14		csbeq1a	$⊢ n = m \to A = ⦋ m / n ⦌ A$
15	14	fveq2d	$⊢ n = m \to {vol}^{} (A) = {vol}^{} (⦋ m / n ⦌ A)$
16	10 13 15	cbvmpt	$⊢ (n \in ℕ ⟼ {vol}^{} (A)) = (m \in ℕ ⟼ {vol}^{} (⦋ m / n ⦌ A))$
17	2 16	eqtri	$⊢ G = (m \in ℕ ⟼ {vol}^{*} (⦋ m / n ⦌ A))$
18	17	fvmpt2	$⊢ (m \in ℕ \land {vol}^{} (⦋ m / n ⦌ A) \in V) \to G (m) = {vol}^{} (⦋ m / n ⦌ A)$
19	9 18	mpan2	$⊢ m \in ℕ \to G (m) = {vol}^{*} (⦋ m / n ⦌ A)$
20	19	adantl	$⊢ (φ \land m \in ℕ) \to G (m) = {vol}^{*} (⦋ m / n ⦌ A)$
21	4	ralrimiva	$⊢ φ \to \forall n \in ℕ {vol}^{*} (A) \in ℝ$
22	10	nfel1	$⊢ Ⅎ m {vol}^{*} (A) \in ℝ$
23	13	nfel1	$⊢ Ⅎ n {vol}^{*} (⦋ m / n ⦌ A) \in ℝ$
24	15	eleq1d	$⊢ n = m \to ({vol}^{} (A) \in ℝ \leftrightarrow {vol}^{} (⦋ m / n ⦌ A) \in ℝ)$
25	22 23 24	cbvralw	$⊢ \forall n \in ℕ {vol}^{} (A) \in ℝ \leftrightarrow \forall m \in ℕ {vol}^{} (⦋ m / n ⦌ A) \in ℝ$
26	21 25	sylib	$⊢ φ \to \forall m \in ℕ {vol}^{*} (⦋ m / n ⦌ A) \in ℝ$
27	26	r19.21bi	$⊢ (φ \land m \in ℕ) \to {vol}^{*} (⦋ m / n ⦌ A) \in ℝ$
28	20 27	eqeltrd	$⊢ (φ \land m \in ℕ) \to G (m) \in ℝ$
29	7 8 28	serfre	$⊢ φ \to seq 1 (+ G) : ℕ ⟶ ℝ$
30	1	feq1i	$⊢ T : ℕ ⟶ ℝ \leftrightarrow seq 1 (+ G) : ℕ ⟶ ℝ$
31	29 30	sylibr	$⊢ φ \to T : ℕ ⟶ ℝ$
32	31	frnd	$⊢ φ \to ran T \subseteq ℝ$
33		1nn	$⊢ 1 \in ℕ$
34	31	fdmd	$⊢ φ \to dom T = ℕ$
35	33 34	eleqtrrid	$⊢ φ \to 1 \in dom T$
36	35	ne0d	$⊢ φ \to dom T \neq \emptyset$
37		dm0rn0	$⊢ dom T = \emptyset \leftrightarrow ran T = \emptyset$
38	37	necon3bii	$⊢ dom T \neq \emptyset \leftrightarrow ran T \neq \emptyset$
39	36 38	sylib	$⊢ φ \to ran T \neq \emptyset$
40	1 5	eqeltrrid	$⊢ φ \to seq 1 (+ G) \in dom ⇝$
41	7 8 20 27 40	isumrecl	$⊢ φ \to \sum_{m \in ℕ} {vol}^{*} (⦋ m / n ⦌ A) \in ℝ$
42		elfznn	$⊢ m \in (1 \dots k) \to m \in ℕ$
43	42	adantl	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to m \in ℕ$
44	43 19	syl	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to G (m) = {vol}^{*} (⦋ m / n ⦌ A)$
45		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
46	45 7	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
47		simpl	$⊢ (φ \land k \in ℕ) \to φ$
48	47 42 27	syl2an	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to {vol}^{*} (⦋ m / n ⦌ A) \in ℝ$
49	48	recnd	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to {vol}^{*} (⦋ m / n ⦌ A) \in ℂ$
50	44 46 49	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} {vol}^{*} (⦋ m / n ⦌ A) = seq 1 (+ G) (k)$
51	1	fveq1i	$⊢ T (k) = seq 1 (+ G) (k)$
52	50 51	eqtr4di	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} {vol}^{*} (⦋ m / n ⦌ A) = T (k)$
53		fzfid	$⊢ φ \to (1 \dots k) \in Fin$
54		fz1ssnn	$⊢ (1 \dots k) \subseteq ℕ$
55	54	a1i	$⊢ φ \to (1 \dots k) \subseteq ℕ$
56	3	ralrimiva	$⊢ φ \to \forall n \in ℕ A \subseteq ℝ$
57		nfv	$⊢ Ⅎ m A \subseteq ℝ$
58		nfcv	$⊢ \underline{Ⅎ} n ℝ$
59	12 58	nfss	$⊢ Ⅎ n ⦋ m / n ⦌ A \subseteq ℝ$
60	14	sseq1d	$⊢ n = m \to (A \subseteq ℝ \leftrightarrow ⦋ m / n ⦌ A \subseteq ℝ)$
61	57 59 60	cbvralw	$⊢ \forall n \in ℕ A \subseteq ℝ \leftrightarrow \forall m \in ℕ ⦋ m / n ⦌ A \subseteq ℝ$
62	56 61	sylib	$⊢ φ \to \forall m \in ℕ ⦋ m / n ⦌ A \subseteq ℝ$
63	62	r19.21bi	$⊢ (φ \land m \in ℕ) \to ⦋ m / n ⦌ A \subseteq ℝ$
64		ovolge0	$⊢ ⦋ m / n ⦌ A \subseteq ℝ \to 0 \leq {vol}^{*} (⦋ m / n ⦌ A)$
65	63 64	syl	$⊢ (φ \land m \in ℕ) \to 0 \leq {vol}^{*} (⦋ m / n ⦌ A)$
66	7 8 53 55 20 27 65 40	isumless	$⊢ φ \to \sum_{m = 1}^{k} {vol}^{} (⦋ m / n ⦌ A) \leq \sum_{m \in ℕ} {vol}^{} (⦋ m / n ⦌ A)$
67	66	adantr	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} {vol}^{} (⦋ m / n ⦌ A) \leq \sum_{m \in ℕ} {vol}^{} (⦋ m / n ⦌ A)$
68	52 67	eqbrtrrd	$⊢ (φ \land k \in ℕ) \to T (k) \leq \sum_{m \in ℕ} {vol}^{*} (⦋ m / n ⦌ A)$
69	68	ralrimiva	$⊢ φ \to \forall k \in ℕ T (k) \leq \sum_{m \in ℕ} {vol}^{*} (⦋ m / n ⦌ A)$
70		brralrspcev	$⊢ (\sum_{m \in ℕ} {vol}^{} (⦋ m / n ⦌ A) \in ℝ \land \forall k \in ℕ T (k) \leq \sum_{m \in ℕ} {vol}^{} (⦋ m / n ⦌ A)) \to \exists x \in ℝ \forall k \in ℕ T (k) \leq x$
71	41 69 70	syl2anc	$⊢ φ \to \exists x \in ℝ \forall k \in ℕ T (k) \leq x$
72	31	ffnd	$⊢ φ \to T Fn ℕ$
73		breq1	$⊢ z = T (k) \to (z \leq x \leftrightarrow T (k) \leq x)$
74	73	ralrn	$⊢ T Fn ℕ \to (\forall z \in ran T z \leq x \leftrightarrow \forall k \in ℕ T (k) \leq x)$
75	72 74	syl	$⊢ φ \to (\forall z \in ran T z \leq x \leftrightarrow \forall k \in ℕ T (k) \leq x)$
76	75	rexbidv	$⊢ φ \to (\exists x \in ℝ \forall z \in ran T z \leq x \leftrightarrow \exists x \in ℝ \forall k \in ℕ T (k) \leq x)$
77	71 76	mpbird	$⊢ φ \to \exists x \in ℝ \forall z \in ran T z \leq x$
78		supxrre	$⊢ (ran T \subseteq ℝ \land ran T \neq \emptyset \land \exists x \in ℝ \forall z \in ran T z \leq x) \to sup (ran T ℝ^{*} <) = sup (ran T ℝ <)$
79	32 39 77 78	syl3anc	$⊢ φ \to sup (ran T ℝ^{*} <) = sup (ran T ℝ <)$
80	7 1 8 20 27 65 71	isumsup	$⊢ φ \to \sum_{m \in ℕ} {vol}^{*} (⦋ m / n ⦌ A) = sup (ran T ℝ <)$
81	79 80	eqtr4d	$⊢ φ \to sup (ran T ℝ^{} <) = \sum_{m \in ℕ} {vol}^{} (⦋ m / n ⦌ A)$
82	10 13 15	cbvsumi	$⊢ \sum_{n \in ℕ} {vol}^{} (A) = \sum_{m \in ℕ} {vol}^{} (⦋ m / n ⦌ A)$
83	81 82	eqtr4di	$⊢ φ \to sup (ran T ℝ^{} <) = \sum_{n \in ℕ} {vol}^{} (A)$
84	6 83	breqtrd	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \leq \sum_{n \in ℕ} {vol}^{} (A)$

Metamath Proof Explorer

Theorem ovoliun2

Proof