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

Theorem fsumrecl 15087
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 10587 . . 3 ℝ ⊆ ℂ
21a1i 11 . 2 (𝜑 → ℝ ⊆ ℂ)
3 readdcl 10613 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
43adantl 485 . 2 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
5 fsumcl.1 . 2 (𝜑𝐴 ∈ Fin)
6 fsumrecl.2 . 2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℝ)
7 0red 10637 . 2 (𝜑 → 0 ∈ ℝ)
82, 4, 5, 6, 7fsumcllem 15085 1 (𝜑 → Σ𝑘𝐴 𝐵 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  wss 3884  (class class class)co 7139  Fincfn 8496  cc 10528  cr 10529   + caddc 10533  Σcsu 15038
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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608
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 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-sup 8894  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-sum 15039
This theorem is referenced by:  fsumless  15147  fsumle  15150  fsumlt  15151  fsumabs  15152  o1fsum  15164  isumltss  15199  climcndslem1  15200  climcndslem2  15201  mertenslem1  15236  rpnnen2lem10  15572  prmreclem4  16249  prmreclem5  16250  lebnumlem1  23570  csbren  24007  trirn  24008  rrxmet  24016  rrxdstprj1  24017  ovolfiniun  24109  ovoliunlem1  24110  ovolscalem1  24121  ovolicc2lem4  24128  volfiniun  24155  uniioombllem3a  24192  uniioombllem4  24194  i1fd  24289  itg1cl  24293  i1fadd  24303  i1fmul  24304  dvfsumge  24629  dvfsumabs  24630  dvfsumrlimf  24632  dvfsumlem2  24634  dvfsumlem3  24635  dvfsumlem4  24636  dvfsum2  24641  aaliou3lem5  24947  mtest  25003  mtestbdd  25004  abelthlem7  25037  abelthlem8  25038  log2ublem2  25537  log2ub  25539  birthdaylem3  25543  emcllem1  25585  emcllem2  25586  emcllem3  25587  harmoniclbnd  25598  harmonicubnd  25599  harmonicbnd4  25600  fsumharmonic  25601  ftalem1  25662  ftalem4  25665  ftalem5  25666  chtf  25697  chpf  25712  chpub  25808  logfaclbnd  25810  logexprlim  25813  chtppilimlem1  26061  vmadivsum  26070  vmadivsumb  26071  rplogsumlem1  26072  rplogsumlem2  26073  rpvmasumlem  26075  dchrisumlem2  26078  dchrmusum2  26082  dchrvmasumlem2  26086  dchrvmasumlem3  26087  dchrvmasumiflem1  26089  dchrisum0ff  26095  dchrisum0flblem1  26096  dchrisum0fno1  26099  dchrisum0re  26101  dchrisum0lem1  26104  dchrisum0lem2a  26105  rplogsum  26115  dirith2  26116  mudivsum  26118  mulogsumlem  26119  mulog2sumlem1  26122  mulog2sumlem2  26123  vmalogdivsum2  26126  vmalogdivsum  26127  2vmadivsumlem  26128  logsqvma2  26131  log2sumbnd  26132  selberglem2  26134  selberg  26136  selbergb  26137  selberg2b  26140  chpdifbndlem1  26141  logdivbnd  26144  selberg3lem1  26145  selberg3lem2  26146  selberg3  26147  selberg4lem1  26148  selberg4  26149  pntrsumo1  26153  pntrsumbnd  26154  pntrsumbnd2  26155  selberg3r  26157  selberg4r  26158  selberg34r  26159  pntsf  26161  pntsval2  26164  pntrlog2bndlem1  26165  pntrlog2bndlem2  26166  pntrlog2bndlem3  26167  pntrlog2bndlem4  26168  pntrlog2bndlem5  26169  pntrlog2bndlem6  26171  pntrlog2bnd  26172  pntpbnd1  26174  pntpbnd2  26175  pntlemj  26191  pntlemf  26193  pntlemk  26194  pntlemo  26195  axsegconlem2  26716  ax5seglem3  26729  ax5seg  26736  esumpcvgval  31451  esumcvg  31459  sibfof  31712  reprlt  32004  reprgt  32006  reprinfz1  32007  hgt750lemd  32033  hgt750lemb  32041  hgt750lema  32042  hgt750leme  32043  tgoldbachgtde  32045  knoppndvlem5  33969  knoppndvlem11  33975  knoppndvlem14  33978  mettrifi  35194  geomcau  35196  rrnmet  35266  rrndstprj1  35267  rrndstprj2  35268  fltnltalem  39611  refsumcn  41652  fsumge0cl  42208  fsumreclf  42211  stoweidlem11  42646  stoweidlem17  42652  stoweidlem20  42655  stoweidlem26  42661  stoweidlem30  42665  stoweidlem32  42667  stoweidlem38  42673  stoweidlem44  42679  stirlinglem12  42720  dirkeritg  42737  fourierdlem73  42814  fourierdlem83  42824  fourierdlem112  42853  etransclem23  42892  etransclem35  42904  etransclem48  42917  sge0rnre  42996  sge0cl  43013  sge0fsum  43019  sge0ltfirp  43032  sge0le  43039  sge0split  43041  sge0iunmptlemfi  43045  sge0iunmptlemre  43047  sge0xaddlem1  43065  sge0xaddlem2  43066  sge0seq  43078  omeiunltfirp  43151  carageniuncllem2  43154  hoidmvlelem2  43228  hoidmvlelem3  43229  hoiqssbllem2  43255  fsummsndifre  43882  fsummmodsndifre  43884
  Copyright terms: Public domain W3C validator