Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  vonicclem1 Structured version   Visualization version   GIF version

Theorem vonicclem1 43716
 Description: The sequence of the measures of the half-open intervals converges to the measure of their intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypotheses
Ref Expression
vonicclem1.x (𝜑𝑋 ∈ Fin)
vonicclem1.a (𝜑𝐴:𝑋⟶ℝ)
vonicclem1.b (𝜑𝐵:𝑋⟶ℝ)
vonicclem1.u (𝜑𝑋 ≠ ∅)
vonicclem1.t ((𝜑𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
vonicclem1.c 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
vonicclem1.d 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘)))
vonicclem1.s 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷𝑛)))
Assertion
Ref Expression
vonicclem1 (𝜑𝑆 ⇝ ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
Distinct variable groups:   𝐴,𝑘,𝑛   𝐵,𝑛   𝐶,𝑘   𝑘,𝑋,𝑛   𝜑,𝑘,𝑛
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑛)   𝐷(𝑘,𝑛)   𝑆(𝑘,𝑛)

Proof of Theorem vonicclem1
StepHypRef Expression
1 vonicclem1.s . . . 4 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷𝑛)))
21a1i 11 . . 3 (𝜑𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷𝑛))))
3 simpr 488 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
4 vonicclem1.d . . . . . . . . . 10 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘)))
54a1i 11 . . . . . . . . 9 (𝜑𝐷 = (𝑛 ∈ ℕ ↦ X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))))
6 vonicclem1.x . . . . . . . . . . . 12 (𝜑𝑋 ∈ Fin)
76adantr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ Fin)
8 eqid 2758 . . . . . . . . . . 11 dom (voln‘𝑋) = dom (voln‘𝑋)
9 vonicclem1.a . . . . . . . . . . . 12 (𝜑𝐴:𝑋⟶ℝ)
109adantr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐴:𝑋⟶ℝ)
11 vonicclem1.b . . . . . . . . . . . . . . . 16 (𝜑𝐵:𝑋⟶ℝ)
1211ffvelrnda 6847 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
1312adantlr 714 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
14 nnrecre 11721 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
1514ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (1 / 𝑛) ∈ ℝ)
1613, 15readdcld 10713 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐵𝑘) + (1 / 𝑛)) ∈ ℝ)
1716fmpttd 6875 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))):𝑋⟶ℝ)
18 vonicclem1.c . . . . . . . . . . . . . . 15 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
1918a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = (𝑛 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛)))))
206mptexd 6983 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))) ∈ V)
2120adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))) ∈ V)
2219, 21fvmpt2d 6776 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐶𝑛) = (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
2322feq1d 6487 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝐶𝑛):𝑋⟶ℝ ↔ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))):𝑋⟶ℝ))
2417, 23mpbird 260 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐶𝑛):𝑋⟶ℝ)
257, 8, 10, 24hoimbl 43664 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘)) ∈ dom (voln‘𝑋))
2625elexd 3430 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘)) ∈ V)
275, 26fvmpt2d 6776 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐷𝑛) = X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘)))
283, 27syldan 594 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐷𝑛) = X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘)))
2928fveq2d 6666 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln‘𝑋)‘(𝐷𝑛)) = ((voln‘𝑋)‘X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))))
30 vonicclem1.u . . . . . . . 8 (𝜑𝑋 ≠ ∅)
3130adantr 484 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑋 ≠ ∅)
323, 24syldan 594 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐶𝑛):𝑋⟶ℝ)
33 eqid 2758 . . . . . . 7 X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘)) = X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))
347, 31, 10, 32, 33vonn0hoi 43703 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln‘𝑋)‘X𝑘𝑋 ((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))))
3510ffvelrnda 6847 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐴𝑘) ∈ ℝ)
363, 35syldanl 604 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐴𝑘) ∈ ℝ)
3732ffvelrnda 6847 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑛)‘𝑘) ∈ ℝ)
38 volico 43019 . . . . . . . . 9 (((𝐴𝑘) ∈ ℝ ∧ ((𝐶𝑛)‘𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))) = if((𝐴𝑘) < ((𝐶𝑛)‘𝑘), (((𝐶𝑛)‘𝑘) − (𝐴𝑘)), 0))
3936, 37, 38syl2anc 587 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))) = if((𝐴𝑘) < ((𝐶𝑛)‘𝑘), (((𝐶𝑛)‘𝑘) − (𝐴𝑘)), 0))
403, 13syldanl 604 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
41 vonicclem1.t . . . . . . . . . . 11 ((𝜑𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
4241adantlr 714 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
43 nnrp 12446 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
4443rpreccld 12487 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
4544ad2antlr 726 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (1 / 𝑛) ∈ ℝ+)
4640, 45ltaddrpd 12510 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐵𝑘) < ((𝐵𝑘) + (1 / 𝑛)))
4716elexd 3430 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐵𝑘) + (1 / 𝑛)) ∈ V)
4822, 47fvmpt2d 6776 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑛)‘𝑘) = ((𝐵𝑘) + (1 / 𝑛)))
493, 48syldanl 604 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑛)‘𝑘) = ((𝐵𝑘) + (1 / 𝑛)))
5046, 49breqtrrd 5063 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐵𝑘) < ((𝐶𝑛)‘𝑘))
5136, 40, 37, 42, 50lelttrd 10841 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐴𝑘) < ((𝐶𝑛)‘𝑘))
5251iftrued 4431 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → if((𝐴𝑘) < ((𝐶𝑛)‘𝑘), (((𝐶𝑛)‘𝑘) − (𝐴𝑘)), 0) = (((𝐶𝑛)‘𝑘) − (𝐴𝑘)))
5339, 52eqtrd 2793 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))) = (((𝐶𝑛)‘𝑘) − (𝐴𝑘)))
5453prodeq2dv 15330 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)((𝐶𝑛)‘𝑘))) = ∏𝑘𝑋 (((𝐶𝑛)‘𝑘) − (𝐴𝑘)))
5529, 34, 543eqtrd 2797 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((voln‘𝑋)‘(𝐷𝑛)) = ∏𝑘𝑋 (((𝐶𝑛)‘𝑘) − (𝐴𝑘)))
5648oveq1d 7170 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐶𝑛)‘𝑘) − (𝐴𝑘)) = (((𝐵𝑘) + (1 / 𝑛)) − (𝐴𝑘)))
5713recnd 10712 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐵𝑘) ∈ ℂ)
5815recnd 10712 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (1 / 𝑛) ∈ ℂ)
5935recnd 10712 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (𝐴𝑘) ∈ ℂ)
6057, 58, 59addsubd 11061 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐵𝑘) + (1 / 𝑛)) − (𝐴𝑘)) = (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛)))
6156, 60eqtrd 2793 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐶𝑛)‘𝑘) − (𝐴𝑘)) = (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛)))
6261prodeq2dv 15330 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ∏𝑘𝑋 (((𝐶𝑛)‘𝑘) − (𝐴𝑘)) = ∏𝑘𝑋 (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛)))
6355, 62eqtrd 2793 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((voln‘𝑋)‘(𝐷𝑛)) = ∏𝑘𝑋 (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛)))
6463mpteq2dva 5130 . . 3 (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷𝑛))) = (𝑛 ∈ ℕ ↦ ∏𝑘𝑋 (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛))))
652, 64eqtrd 2793 . 2 (𝜑𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘𝑋 (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛))))
66 nfv 1915 . . 3 𝑘𝜑
679ffvelrnda 6847 . . . . 5 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ)
6812, 67resubcld 11111 . . . 4 ((𝜑𝑘𝑋) → ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ)
6968recnd 10712 . . 3 ((𝜑𝑘𝑋) → ((𝐵𝑘) − (𝐴𝑘)) ∈ ℂ)
70 eqid 2758 . . 3 (𝑛 ∈ ℕ ↦ ∏𝑘𝑋 (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ ∏𝑘𝑋 (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛)))
7166, 6, 69, 70fprodaddrecnncnv 42946 . 2 (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘𝑋 (((𝐵𝑘) − (𝐴𝑘)) + (1 / 𝑛))) ⇝ ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
7265, 71eqbrtrd 5057 1 (𝜑𝑆 ⇝ ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  Vcvv 3409  ∅c0 4227  ifcif 4423   class class class wbr 5035   ↦ cmpt 5115  dom cdm 5527  ⟶wf 6335  ‘cfv 6339  (class class class)co 7155  Xcixp 8484  Fincfn 8532  ℝcr 10579  0cc0 10580  1c1 10581   + caddc 10583   < clt 10718   ≤ cle 10719   − cmin 10913   / cdiv 11340  ℕcn 11679  ℝ+crp 12435  [,)cico 12786   ⇝ cli 14894  ∏cprod 15312  volcvol 24168  volncvoln 43571 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-inf2 9142  ax-cc 9900  ax-ac2 9928  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657  ax-pre-sup 10658  ax-addf 10659  ax-mulf 10660 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-disj 5001  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-se 5487  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-of 7410  df-om 7585  df-1st 7698  df-2nd 7699  df-supp 7841  df-tpos 7907  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-1o 8117  df-2o 8118  df-oadd 8121  df-omul 8122  df-er 8304  df-map 8423  df-pm 8424  df-ixp 8485  df-en 8533  df-dom 8534  df-sdom 8535  df-fin 8536  df-fsupp 8872  df-fi 8913  df-sup 8944  df-inf 8945  df-oi 9012  df-dju 9368  df-card 9406  df-acn 9409  df-ac 9581  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-div 11341  df-nn 11680  df-2 11742  df-3 11743  df-4 11744  df-5 11745  df-6 11746  df-7 11747  df-8 11748  df-9 11749  df-n0 11940  df-z 12026  df-dec 12143  df-uz 12288  df-q 12394  df-rp 12436  df-xneg 12553  df-xadd 12554  df-xmul 12555  df-ioo 12788  df-ico 12790  df-icc 12791  df-fz 12945  df-fzo 13088  df-fl 13216  df-seq 13424  df-exp 13485  df-hash 13746  df-cj 14511  df-re 14512  df-im 14513  df-sqrt 14647  df-abs 14648  df-clim 14898  df-rlim 14899  df-sum 15096  df-prod 15313  df-struct 16548  df-ndx 16549  df-slot 16550  df-base 16552  df-sets 16553  df-ress 16554  df-plusg 16641  df-mulr 16642  df-starv 16643  df-sca 16644  df-vsca 16645  df-ip 16646  df-tset 16647  df-ple 16648  df-ds 16650  df-unif 16651  df-hom 16652  df-cco 16653  df-rest 16759  df-topn 16760  df-0g 16778  df-gsum 16779  df-topgen 16780  df-pt 16781  df-prds 16784  df-xrs 16838  df-qtop 16843  df-imas 16844  df-xps 16846  df-mre 16920  df-mrc 16921  df-acs 16923  df-mgm 17923  df-sgrp 17972  df-mnd 17983  df-submnd 18028  df-grp 18177  df-minusg 18178  df-mulg 18297  df-subg 18348  df-cntz 18519  df-cmn 18980  df-abl 18981  df-mgp 19313  df-ur 19325  df-ring 19372  df-cring 19373  df-oppr 19449  df-dvdsr 19467  df-unit 19468  df-invr 19498  df-dvr 19509  df-drng 19577  df-psmet 20163  df-xmet 20164  df-met 20165  df-bl 20166  df-mopn 20167  df-cnfld 20172  df-top 21599  df-topon 21616  df-topsp 21638  df-bases 21651  df-cn 21932  df-cnp 21933  df-cmp 22092  df-tx 22267  df-hmeo 22460  df-xms 23027  df-ms 23028  df-tms 23029  df-cncf 23584  df-ovol 24169  df-vol 24170  df-salg 43345  df-sumge0 43396  df-mea 43483  df-ome 43523  df-caragen 43525  df-ovoln 43570  df-voln 43572 This theorem is referenced by:  vonicclem2  43717
 Copyright terms: Public domain W3C validator