Theorem measiun

Description: A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016) (Proof shortened by Thierry Arnoux, 7-Feb-2017)

	Ref	Expression
Hypotheses	measiun.1	⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ 𝑆 ) )
	measiun.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	measiun.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ 𝑆 )
	measiun.4	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐵 )
Assertion	measiun	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		measiun.1	⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ 𝑆 ) )
2		measiun.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
3		measiun.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ 𝑆 )
4		measiun.4	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐵 )
5		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
6		measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
7	1 2 6	syl2anc	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
8	5 7	sselid	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
9		measbase	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
10	1 9	syl	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
11	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ 𝐵 ∈ 𝑆 )
12		sigaclcu2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑛 ∈ ℕ 𝐵 ∈ 𝑆 ) → ∪ 𝑛 ∈ ℕ 𝐵 ∈ 𝑆 )
13	10 11 12	syl2anc	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ 𝐵 ∈ 𝑆 )
14		measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∪ 𝑛 ∈ ℕ 𝐵 ∈ 𝑆 ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ 𝐵 ) ∈ ( 0 [,] +∞ ) )
15	1 13 14	syl2anc	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ 𝐵 ) ∈ ( 0 [,] +∞ ) )
16	5 15	sselid	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ 𝐵 ) ∈ ℝ* )
17		nnex	⊢ ℕ ∈ V
18	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
19		measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
20	18 3 19	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
21	20	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
22		nfcv	⊢ Ⅎ 𝑛 ℕ
23	22	esumcl	⊢ ( ( ℕ ∈ V ∧ ∀ 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
24	17 21 23	sylancr	⊢ ( 𝜑 → Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
25	5 24	sselid	⊢ ( 𝜑 → Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) ∈ ℝ* )
26	1 2 13 4	measssd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ 𝐵 ) )
27		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐵
28		csbeq1a	⊢ ( 𝑛 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑛 ⦌ 𝐵 )
29		eqidd	⊢ ( 𝜑 → ℕ = ℕ )
30	29	orcd	⊢ ( 𝜑 → ( ℕ = ℕ ∨ ℕ = ( 1 ..^ 𝑚 ) ) )
31	27 28 30 1 3	measiuns	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ 𝐵 ) = Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ) )
32	17	a1i	⊢ ( 𝜑 → ℕ ∈ V )
33	10	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ∈ ∪ ran sigAlgebra )
34		nfv	⊢ Ⅎ 𝑛 𝜑
35		nfcv	⊢ Ⅎ 𝑛 𝑘
36	35	nfel1	⊢ Ⅎ 𝑛 𝑘 ∈ ℕ
37	27	nfel1	⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆
38	36 37	nfim	⊢ Ⅎ 𝑛 ( 𝑘 ∈ ℕ → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 )
39	34 38	nfim	⊢ Ⅎ 𝑛 ( 𝜑 → ( 𝑘 ∈ ℕ → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) )
40		eleq1w	⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ ℕ ↔ 𝑘 ∈ ℕ ) )
41	28	eleq1d	⊢ ( 𝑛 = 𝑘 → ( 𝐵 ∈ 𝑆 ↔ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) )
42	40 41	imbi12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 ∈ ℕ → 𝐵 ∈ 𝑆 ) ↔ ( 𝑘 ∈ ℕ → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) ) )
43	42	imbi2d	⊢ ( 𝑛 = 𝑘 → ( ( 𝜑 → ( 𝑛 ∈ ℕ → 𝐵 ∈ 𝑆 ) ) ↔ ( 𝜑 → ( 𝑘 ∈ ℕ → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) ) ) )
44	3	ex	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ → 𝐵 ∈ 𝑆 ) )
45	39 43 44	chvarfv	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) )
46	45	ralrimiv	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 )
47		fzossnn	⊢ ( 1 ..^ 𝑛 ) ⊆ ℕ
48		ssralv	⊢ ( ( 1 ..^ 𝑛 ) ⊆ ℕ → ( ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 → ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) )
49	47 48	ax-mp	⊢ ( ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 → ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 )
50		sigaclfu2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 )
51	49 50	sylan2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 )
52	10 46 51	syl2anc	⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 )
54		difelsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐵 ∈ 𝑆 ∧ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ∈ 𝑆 ) → ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ∈ 𝑆 )
55	33 3 53 54	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ∈ 𝑆 )
56		measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
57	18 55 56	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
58		difssd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ⊆ 𝐵 )
59	18 55 3 58	measssd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ) ≤ ( 𝑀 ‘ 𝐵 ) )
60	32 57 20 59	esumle	⊢ ( 𝜑 → Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ⦋ 𝑘 / 𝑛 ⦌ 𝐵 ) ) ≤ Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) )
61	31 60	eqbrtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ 𝐵 ) ≤ Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) )
62	8 16 25 26 61	xrletrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ 𝐵 ) )