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

Theorem fsumrecl 14261
Description: Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
Hypotheses
Ref Expression
fsumcl.1 (𝜑𝐴 ∈ Fin)
fsumrecl.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℝ)
Assertion
Ref Expression
fsumrecl (𝜑 → Σ𝑘𝐴 𝐵 ∈ ℝ)
Distinct variable groups:   𝐴,𝑘   𝜑,𝑘
Allowed substitution hint:   𝐵(𝑘)

Proof of Theorem fsumrecl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-resscn 9850 . . 3 ℝ ⊆ ℂ
21a1i 11 . 2 (𝜑 → ℝ ⊆ ℂ)
3 readdcl 9876 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
43adantl 480 . 2 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
5 fsumcl.1 . 2 (𝜑𝐴 ∈ Fin)
6 fsumrecl.2 . 2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℝ)
7 0red 9898 . 2 (𝜑 → 0 ∈ ℝ)
82, 4, 5, 6, 7fsumcllem 14259 1 (𝜑 → Σ𝑘𝐴 𝐵 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wss 3539  (class class class)co 6527  Fincfn 7819  cc 9791  cr 9792   + caddc 9796  Σcsu 14213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-oadd 7429  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-sup 8209  df-oi 8276  df-card 8626  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-n0 11143  df-z 11214  df-uz 11523  df-rp 11668  df-fz 12156  df-fzo 12293  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-sum 14214
This theorem is referenced by:  fsumless  14318  fsumle  14321  fsumlt  14322  fsumabs  14323  o1fsum  14335  isumltss  14368  climcndslem1  14369  climcndslem2  14370  mertenslem1  14404  rpnnen2lem10  14740  prmreclem4  15410  prmreclem5  15411  lebnumlem1  22516  csbren  22935  trirn  22936  rrxmet  22944  rrxdstprj1  22945  ovolfiniun  23021  ovoliunlem1  23022  ovolscalem1  23033  ovolicc2lem4  23040  volfiniun  23067  uniioombllem3a  23103  uniioombllem4  23105  i1fd  23199  itg1cl  23203  i1fadd  23213  i1fmul  23214  dvfsumge  23534  dvfsumabs  23535  dvfsumrlimf  23537  dvfsumlem2  23539  dvfsumlem3  23540  dvfsumlem4  23541  dvfsum2  23546  aaliou3lem5  23851  mtest  23907  mtestbdd  23908  abelthlem7  23941  abelthlem8  23942  log2ublem2  24419  log2ub  24421  birthdaylem3  24425  emcllem1  24467  emcllem2  24468  emcllem3  24469  harmoniclbnd  24480  harmonicubnd  24481  harmonicbnd4  24482  fsumharmonic  24483  ftalem1  24544  ftalem4  24547  ftalem5  24548  chtf  24579  chpf  24594  chpub  24690  logfaclbnd  24692  logexprlim  24695  chtppilimlem1  24907  vmadivsum  24916  vmadivsumb  24917  rplogsumlem1  24918  rplogsumlem2  24919  rpvmasumlem  24921  dchrisumlem2  24924  dchrmusum2  24928  dchrvmasumlem2  24932  dchrvmasumlem3  24933  dchrvmasumiflem1  24935  dchrisum0ff  24941  dchrisum0flblem1  24942  dchrisum0fno1  24945  dchrisum0re  24947  dchrisum0lem1  24950  dchrisum0lem2a  24951  rplogsum  24961  dirith2  24962  mudivsum  24964  mulogsumlem  24965  mulog2sumlem1  24968  mulog2sumlem2  24969  vmalogdivsum2  24972  vmalogdivsum  24973  2vmadivsumlem  24974  logsqvma2  24977  log2sumbnd  24978  selberglem2  24980  selberg  24982  selbergb  24983  selberg2b  24986  chpdifbndlem1  24987  logdivbnd  24990  selberg3lem1  24991  selberg3lem2  24992  selberg3  24993  selberg4lem1  24994  selberg4  24995  pntrsumo1  24999  pntrsumbnd  25000  pntrsumbnd2  25001  selberg3r  25003  selberg4r  25004  selberg34r  25005  pntsf  25007  pntsval2  25010  pntrlog2bndlem1  25011  pntrlog2bndlem2  25012  pntrlog2bndlem3  25013  pntrlog2bndlem4  25014  pntrlog2bndlem5  25015  pntrlog2bndlem6  25017  pntrlog2bnd  25018  pntpbnd1  25020  pntpbnd2  25021  pntlemj  25037  pntlemf  25039  pntlemk  25040  pntlemo  25041  axsegconlem2  25544  ax5seglem3  25557  ax5seg  25564  esumpcvgval  29301  esumcvg  29309  sibfof  29563  knoppndvlem5  31511  knoppndvlem11  31517  knoppndvlem14  31520  mettrifi  32547  geomcau  32549  rrnmet  32622  rrndstprj1  32623  rrndstprj2  32624  refsumcn  38036  fsumge0cl  38464  fsumreclf  38467  stoweidlem11  38728  stoweidlem17  38734  stoweidlem20  38737  stoweidlem26  38743  stoweidlem30  38747  stoweidlem32  38749  stoweidlem38  38755  stoweidlem44  38761  stirlinglem12  38802  dirkeritg  38819  fourierdlem73  38896  fourierdlem83  38906  fourierdlem112  38935  etransclem23  38974  etransclem35  38986  etransclem48  38999  sge0rnre  39081  sge0cl  39098  sge0fsum  39104  sge0ltfirp  39117  sge0le  39124  sge0split  39126  sge0iunmptlemfi  39130  sge0iunmptlemre  39132  sge0xaddlem1  39150  sge0xaddlem2  39151  sge0seq  39163  omeiunltfirp  39233  carageniuncllem2  39236  hoidmvlelem2  39310  hoidmvlelem3  39311  hoiqssbllem2  39337  fsummsndifre  40241  fsummmodsndifre  40243
  Copyright terms: Public domain W3C validator