MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovoliun Structured version   Visualization version   GIF version

Theorem ovoliun 24407
Description: The Lebesgue outer measure function is countably sub-additive. (Many books allow +∞ as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss 24387, so we need not consider this case here, although we do allow the sum itself to be infinite.) (Contributed by Mario Carneiro, 12-Jun-2014.)
Hypotheses
Ref Expression
ovoliun.t 𝑇 = seq1( + , 𝐺)
ovoliun.g 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))
ovoliun.a ((𝜑𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)
ovoliun.v ((𝜑𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
Assertion
Ref Expression
ovoliun (𝜑 → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
Distinct variable group:   𝜑,𝑛
Allowed substitution hints:   𝐴(𝑛)   𝑇(𝑛)   𝐺(𝑛)

Proof of Theorem ovoliun
Dummy variables 𝑘 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mnfxr 10895 . . . . . 6 -∞ ∈ ℝ*
21a1i 11 . . . . 5 (𝜑 → -∞ ∈ ℝ*)
3 nnuz 12482 . . . . . . . . 9 ℕ = (ℤ‘1)
4 1zzd 12213 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
5 ovoliun.v . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
6 ovoliun.g . . . . . . . . . . 11 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))
75, 6fmptd 6936 . . . . . . . . . 10 (𝜑𝐺:ℕ⟶ℝ)
87ffvelrnda 6909 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
93, 4, 8serfre 13610 . . . . . . . 8 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
10 ovoliun.t . . . . . . . . 9 𝑇 = seq1( + , 𝐺)
1110feq1i 6541 . . . . . . . 8 (𝑇:ℕ⟶ℝ ↔ seq1( + , 𝐺):ℕ⟶ℝ)
129, 11sylibr 237 . . . . . . 7 (𝜑𝑇:ℕ⟶ℝ)
13 1nn 11846 . . . . . . 7 1 ∈ ℕ
14 ffvelrn 6907 . . . . . . 7 ((𝑇:ℕ⟶ℝ ∧ 1 ∈ ℕ) → (𝑇‘1) ∈ ℝ)
1512, 13, 14sylancl 589 . . . . . 6 (𝜑 → (𝑇‘1) ∈ ℝ)
1615rexrd 10888 . . . . 5 (𝜑 → (𝑇‘1) ∈ ℝ*)
1712frnd 6558 . . . . . . 7 (𝜑 → ran 𝑇 ⊆ ℝ)
18 ressxr 10882 . . . . . . 7 ℝ ⊆ ℝ*
1917, 18sstrdi 3918 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ*)
20 supxrcl 12910 . . . . . 6 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
2119, 20syl 17 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
2215mnfltd 12721 . . . . 5 (𝜑 → -∞ < (𝑇‘1))
2312ffnd 6551 . . . . . . 7 (𝜑𝑇 Fn ℕ)
24 fnfvelrn 6906 . . . . . . 7 ((𝑇 Fn ℕ ∧ 1 ∈ ℕ) → (𝑇‘1) ∈ ran 𝑇)
2523, 13, 24sylancl 589 . . . . . 6 (𝜑 → (𝑇‘1) ∈ ran 𝑇)
26 supxrub 12919 . . . . . 6 ((ran 𝑇 ⊆ ℝ* ∧ (𝑇‘1) ∈ ran 𝑇) → (𝑇‘1) ≤ sup(ran 𝑇, ℝ*, < ))
2719, 25, 26syl2anc 587 . . . . 5 (𝜑 → (𝑇‘1) ≤ sup(ran 𝑇, ℝ*, < ))
282, 16, 21, 22, 27xrltletrd 12756 . . . 4 (𝜑 → -∞ < sup(ran 𝑇, ℝ*, < ))
29 xrrebnd 12763 . . . . 5 (sup(ran 𝑇, ℝ*, < ) ∈ ℝ* → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) < +∞)))
3021, 29syl 17 . . . 4 (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) < +∞)))
3128, 30mpbirand 707 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ ↔ sup(ran 𝑇, ℝ*, < ) < +∞))
32 nfcv 2904 . . . . . . . . 9 𝑚𝐴
33 nfcsb1v 3841 . . . . . . . . 9 𝑛𝑚 / 𝑛𝐴
34 csbeq1a 3830 . . . . . . . . 9 (𝑛 = 𝑚𝐴 = 𝑚 / 𝑛𝐴)
3532, 33, 34cbviun 4950 . . . . . . . 8 𝑛 ∈ ℕ 𝐴 = 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴
3635fveq2i 6725 . . . . . . 7 (vol*‘ 𝑛 ∈ ℕ 𝐴) = (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴)
37 nfcv 2904 . . . . . . . . . 10 𝑚(vol*‘𝐴)
38 nfcv 2904 . . . . . . . . . . 11 𝑛vol*
3938, 33nffv 6732 . . . . . . . . . 10 𝑛(vol*‘𝑚 / 𝑛𝐴)
4034fveq2d 6726 . . . . . . . . . 10 (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘𝑚 / 𝑛𝐴))
4137, 39, 40cbvmpt 5161 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) = (𝑚 ∈ ℕ ↦ (vol*‘𝑚 / 𝑛𝐴))
426, 41eqtri 2765 . . . . . . . 8 𝐺 = (𝑚 ∈ ℕ ↦ (vol*‘𝑚 / 𝑛𝐴))
43 ovoliun.a . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)
4443ralrimiva 3105 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ)
45 nfv 1922 . . . . . . . . . . . 12 𝑚 𝐴 ⊆ ℝ
46 nfcv 2904 . . . . . . . . . . . . 13 𝑛
4733, 46nfss 3897 . . . . . . . . . . . 12 𝑛𝑚 / 𝑛𝐴 ⊆ ℝ
4834sseq1d 3937 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ 𝑚 / 𝑛𝐴 ⊆ ℝ))
4945, 47, 48cbvralw 3354 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀𝑚 ∈ ℕ 𝑚 / 𝑛𝐴 ⊆ ℝ)
5044, 49sylib 221 . . . . . . . . . 10 (𝜑 → ∀𝑚 ∈ ℕ 𝑚 / 𝑛𝐴 ⊆ ℝ)
5150ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ∀𝑚 ∈ ℕ 𝑚 / 𝑛𝐴 ⊆ ℝ)
5251r19.21bi 3130 . . . . . . . 8 ((((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → 𝑚 / 𝑛𝐴 ⊆ ℝ)
535ralrimiva 3105 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ)
5437nfel1 2920 . . . . . . . . . . . 12 𝑚(vol*‘𝐴) ∈ ℝ
5539nfel1 2920 . . . . . . . . . . . 12 𝑛(vol*‘𝑚 / 𝑛𝐴) ∈ ℝ
5640eleq1d 2822 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔ (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ))
5754, 55, 56cbvralw 3354 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ ↔ ∀𝑚 ∈ ℕ (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
5853, 57sylib 221 . . . . . . . . . 10 (𝜑 → ∀𝑚 ∈ ℕ (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
5958ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ∀𝑚 ∈ ℕ (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
6059r19.21bi 3130 . . . . . . . 8 ((((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
61 simplr 769 . . . . . . . 8 (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
62 simpr 488 . . . . . . . 8 (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
6310, 42, 52, 60, 61, 62ovoliunlem3 24406 . . . . . . 7 (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝑥))
6436, 63eqbrtrid 5093 . . . . . 6 (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝑥))
6564ralrimiva 3105 . . . . 5 ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) → ∀𝑥 ∈ ℝ+ (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝑥))
66 iunss 4959 . . . . . . . 8 ( 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ)
6744, 66sylibr 237 . . . . . . 7 (𝜑 𝑛 ∈ ℕ 𝐴 ⊆ ℝ)
68 ovolcl 24380 . . . . . . 7 ( 𝑛 ∈ ℕ 𝐴 ⊆ ℝ → (vol*‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ*)
6967, 68syl 17 . . . . . 6 (𝜑 → (vol*‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ*)
70 xralrple 12800 . . . . . 6 (((vol*‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) → ((vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔ ∀𝑥 ∈ ℝ+ (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝑥)))
7169, 70sylan 583 . . . . 5 ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) → ((vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔ ∀𝑥 ∈ ℝ+ (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝑥)))
7265, 71mpbird 260 . . . 4 ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ) → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
7372ex 416 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < )))
7431, 73sylbird 263 . 2 (𝜑 → (sup(ran 𝑇, ℝ*, < ) < +∞ → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < )))
75 nltpnft 12759 . . . 4 (sup(ran 𝑇, ℝ*, < ) ∈ ℝ* → (sup(ran 𝑇, ℝ*, < ) = +∞ ↔ ¬ sup(ran 𝑇, ℝ*, < ) < +∞))
7621, 75syl 17 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) = +∞ ↔ ¬ sup(ran 𝑇, ℝ*, < ) < +∞))
77 pnfge 12727 . . . . 5 ((vol*‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ +∞)
7869, 77syl 17 . . . 4 (𝜑 → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ +∞)
79 breq2 5062 . . . 4 (sup(ran 𝑇, ℝ*, < ) = +∞ → ((vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔ (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ +∞))
8078, 79syl5ibrcom 250 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) = +∞ → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < )))
8176, 80sylbird 263 . 2 (𝜑 → (¬ sup(ran 𝑇, ℝ*, < ) < +∞ → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < )))
8274, 81pm2.61d 182 1 (𝜑 → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2110  wral 3061  csb 3816  wss 3871   ciun 4909   class class class wbr 5058  cmpt 5140  ran crn 5557   Fn wfn 6380  wf 6381  cfv 6385  (class class class)co 7218  supcsup 9061  cr 10733  1c1 10735   + caddc 10737  +∞cpnf 10869  -∞cmnf 10870  *cxr 10871   < clt 10872  cle 10873  cn 11835  +crp 12591  seqcseq 13579  vol*covol 24364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-inf2 9261  ax-cc 10054  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811  ax-pre-sup 10812
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-se 5515  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-isom 6394  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-er 8396  df-map 8515  df-pm 8516  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-sup 9063  df-inf 9064  df-oi 9131  df-card 9560  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-div 11495  df-nn 11836  df-2 11898  df-3 11899  df-n0 12096  df-z 12182  df-uz 12444  df-q 12550  df-rp 12592  df-ioo 12944  df-ico 12946  df-fz 13101  df-fzo 13244  df-fl 13372  df-seq 13580  df-exp 13641  df-hash 13902  df-cj 14667  df-re 14668  df-im 14669  df-sqrt 14803  df-abs 14804  df-clim 15054  df-rlim 15055  df-sum 15255  df-ovol 24366
This theorem is referenced by:  ovoliun2  24408  voliunlem2  24453  voliunlem3  24454  ex-ovoliunnfl  35562
  Copyright terms: Public domain W3C validator