Metamath Proof Explorer

Theorem 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 ⊢ 𝑇 = seq 1 ( + , 𝐺 )
ovoliun.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
ovoliun.a ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
ovoliun.v ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
ovoliun2.t ⊢ ( 𝜑 → 𝑇 ∈ dom ⇝ )
Assertion ovoliun2 ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ Σ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ovoliun.t ⊢ 𝑇 = seq 1 ( + , 𝐺 )
2 ovoliun.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
3 ovoliun.a ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
4 ovoliun.v ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
5 ovoliun2.t ⊢ ( 𝜑 → 𝑇 ∈ dom ⇝ )
6 1 2 3 4 ovoliun ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
7 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
8 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
9 fvex ⊢ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V
10 nfcv ⊢ Ⅎ 𝑚 ( vol* ‘ 𝐴 )
11 nfcv ⊢ Ⅎ 𝑛 vol*
12 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
13 11 12 nffv ⊢ Ⅎ 𝑛 ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
14 csbeq1a ⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
15 14 fveq2d ⊢ ( 𝑛 = 𝑚 → ( vol* ‘ 𝐴 ) = ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
16 10 13 15 cbvmpt ⊢ ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) ) = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
17 2 16 eqtri ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
18 17 fvmpt2 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V ) → ( 𝐺 ‘ 𝑚 ) = ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
19 9 18 mpan2 ⊢ ( 𝑚 ∈ ℕ → ( 𝐺 ‘ 𝑚 ) = ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) = ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
21 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) ∈ ℝ )
22 10 nfel1 ⊢ Ⅎ 𝑚 ( vol* ‘ 𝐴 ) ∈ ℝ
23 13 nfel1 ⊢ Ⅎ 𝑛 ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ
24 15 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( vol* ‘ 𝐴 ) ∈ ℝ ↔ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ ) )
25 22 23 24 cbvralw ⊢ ( ∀ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) ∈ ℝ ↔ ∀ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
26 21 25 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
27 26 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
28 20 27 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) ∈ ℝ )
29 7 8 28 serfre ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
30 1 feq1i ⊢ ( 𝑇 : ℕ ⟶ ℝ ↔ seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
31 29 30 sylibr ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ℝ )
32 31 frnd ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ )
33 1nn ⊢ 1 ∈ ℕ
34 31 fdmd ⊢ ( 𝜑 → dom 𝑇 = ℕ )
35 33 34 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑇 )
36 35 ne0d ⊢ ( 𝜑 → dom 𝑇 ≠ ∅ )
37 dm0rn0 ⊢ ( dom 𝑇 = ∅ ↔ ran 𝑇 = ∅ )
38 37 necon3bii ⊢ ( dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅ )
39 36 38 sylib ⊢ ( 𝜑 → ran 𝑇 ≠ ∅ )
40 1 5 eqeltrrid ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ∈ dom ⇝ )
41 7 8 20 27 40 isumrecl ⊢ ( 𝜑 → Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
42 elfznn ⊢ ( 𝑚 ∈ ( 1 ... 𝑘 ) → 𝑚 ∈ ℕ )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → 𝑚 ∈ ℕ )
44 43 19 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( 𝐺 ‘ 𝑚 ) = ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
45 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
46 45 7 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
47 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝜑 )
48 47 42 27 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
49 48 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
50 44 46 49 fsumser ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑘 ) )
51 1 fveq1i ⊢ ( 𝑇 ‘ 𝑘 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑘 )
52 50 51 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ( 𝑇 ‘ 𝑘 ) )
53 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑘 ) ∈ Fin )
54 fz1ssnn ⊢ ( 1 ... 𝑘 ) ⊆ ℕ
55 54 a1i ⊢ ( 𝜑 → ( 1 ... 𝑘 ) ⊆ ℕ )
56 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
57 nfv ⊢ Ⅎ 𝑚 𝐴 ⊆ ℝ
58 nfcv ⊢ Ⅎ 𝑛 ℝ
59 12 58 nfss ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ
60 14 sseq1d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ⊆ ℝ ↔ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ ) )
61 57 59 60 cbvralw ⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ )
62 56 61 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ )
63 62 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ )
64 ovolge0 ⊢ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ⊆ ℝ → 0 ≤ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
65 63 64 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
66 7 8 53 55 20 27 65 40 isumless ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ≤ Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
68 52 67 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ 𝑘 ) ≤ Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
69 68 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑇 ‘ 𝑘 ) ≤ Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
70 brralrspcev ⊢ ( ( Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( 𝑇 ‘ 𝑘 ) ≤ Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑇 ‘ 𝑘 ) ≤ 𝑥 )
71 41 69 70 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑇 ‘ 𝑘 ) ≤ 𝑥 )
72 31 ffnd ⊢ ( 𝜑 → 𝑇 Fn ℕ )
73 breq1 ⊢ ( 𝑧 = ( 𝑇 ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑇 ‘ 𝑘 ) ≤ 𝑥 ) )
74 73 ralrn ⊢ ( 𝑇 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑇 ‘ 𝑘 ) ≤ 𝑥 ) )
75 72 74 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑇 ‘ 𝑘 ) ≤ 𝑥 ) )
76 75 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑇 ‘ 𝑘 ) ≤ 𝑥 ) )
77 71 76 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 )
78 supxrre ⊢ ( ( ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ) → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) )
79 32 39 77 78 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) )
80 7 1 8 20 27 65 71 isumsup ⊢ ( 𝜑 → Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = sup ( ran 𝑇 , ℝ , < ) )
81 79 80 eqtr4d ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) = Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
82 10 13 15 cbvsumi ⊢ Σ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) = Σ 𝑚 ∈ ℕ ( vol* ‘ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
83 81 82 eqtr4di ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) = Σ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) )
84 6 83 breqtrd ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ Σ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) )