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

Theorem fsumrecl 13849
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  |-  ( ph  ->  A  e.  Fin )
fsumrecl.2  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  RR )
Assertion
Ref Expression
fsumrecl  |-  ( ph  -> 
sum_ k  e.  A  B  e.  RR )
Distinct variable groups:    A, k    ph, k
Allowed substitution hint:    B( k)

Proof of Theorem fsumrecl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-resscn 9622 . . 3  |-  RR  C_  CC
21a1i 11 . 2  |-  ( ph  ->  RR  C_  CC )
3 readdcl 9648 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  +  y )  e.  RR )
43adantl 472 . 2  |-  ( (
ph  /\  ( x  e.  RR  /\  y  e.  RR ) )  -> 
( x  +  y )  e.  RR )
5 fsumcl.1 . 2  |-  ( ph  ->  A  e.  Fin )
6 fsumrecl.2 . 2  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  RR )
7 0red 9670 . 2  |-  ( ph  ->  0  e.  RR )
82, 4, 5, 6, 7fsumcllem 13847 1  |-  ( ph  -> 
sum_ k  e.  A  B  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898    C_ wss 3416  (class class class)co 6315   Fincfn 7595   CCcc 9563   RRcr 9564    + caddc 9568   sum_csu 13801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-sup 7982  df-oi 8051  df-card 8399  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-n0 10899  df-z 10967  df-uz 11189  df-rp 11332  df-fz 11814  df-fzo 11947  df-seq 12246  df-exp 12305  df-hash 12548  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-clim 13601  df-sum 13802
This theorem is referenced by:  fsumless  13905  fsumle  13908  fsumlt  13909  fsumabs  13910  o1fsum  13922  isumltss  13955  climcndslem1  13956  climcndslem2  13957  mertenslem1  13989  rpnnen2lem10  14325  prmreclem4  14912  prmreclem5  14913  lebnumlem1  22038  lebnumlem1OLD  22041  csbren  22402  trirn  22403  rrxmet  22411  rrxdstprj1  22412  ovolfiniun  22503  ovoliunlem1  22504  ovolscalem1  22515  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  volfiniun  22549  uniioombllem3a  22591  uniioombllem4  22593  i1fd  22688  itg1cl  22692  i1fadd  22702  i1fmul  22703  dvfsumge  23023  dvfsumabs  23024  dvfsumrlimf  23026  dvfsumlem2  23028  dvfsumlem3  23029  dvfsumlem4  23030  dvfsum2  23035  aaliou3lem5  23352  mtest  23408  mtestbdd  23409  abelthlem7  23442  abelthlem8  23443  log2ublem2  23922  log2ub  23924  birthdaylem3  23928  emcllem1  23970  emcllem2  23971  emcllem3  23972  harmoniclbnd  23983  harmonicubnd  23984  harmonicbnd4  23985  fsumharmonic  23986  ftalem1  24046  ftalem4  24049  ftalem5  24050  ftalem4OLD  24051  ftalem5OLD  24052  chtf  24084  chpf  24099  chpub  24197  logfaclbnd  24199  logexprlim  24202  chtppilimlem1  24360  vmadivsum  24369  vmadivsumb  24370  rplogsumlem1  24371  rplogsumlem2  24372  rpvmasumlem  24374  dchrisumlem2  24377  dchrmusum2  24381  dchrvmasumlem2  24385  dchrvmasumlem3  24386  dchrvmasumiflem1  24388  dchrisum0ff  24394  dchrisum0flblem1  24395  dchrisum0fno1  24398  dchrisum0re  24400  dchrisum0lem1  24403  dchrisum0lem2a  24404  rplogsum  24414  dirith2  24415  mudivsum  24417  mulogsumlem  24418  mulog2sumlem1  24421  mulog2sumlem2  24422  vmalogdivsum2  24425  vmalogdivsum  24426  2vmadivsumlem  24427  logsqvma2  24430  log2sumbnd  24431  selberglem2  24433  selberg  24435  selbergb  24436  selberg2b  24439  chpdifbndlem1  24440  logdivbnd  24443  selberg3lem1  24444  selberg3lem2  24445  selberg3  24446  selberg4lem1  24447  selberg4  24448  pntrsumo1  24452  pntrsumbnd  24453  pntrsumbnd2  24454  selberg3r  24456  selberg4r  24457  selberg34r  24458  pntsf  24460  pntsval2  24463  pntrlog2bndlem1  24464  pntrlog2bndlem2  24465  pntrlog2bndlem3  24466  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  pntrlog2bndlem6  24470  pntrlog2bnd  24471  pntpbnd1  24473  pntpbnd2  24474  pntlemj  24490  pntlemf  24492  pntlemk  24493  pntlemo  24494  axsegconlem2  24997  ax5seglem3  25010  ax5seg  25017  esumpcvgval  28948  esumcvg  28956  sibfof  29222  mettrifi  32131  geomcau  32133  rrnmet  32206  rrndstprj1  32207  rrndstprj2  32208  refsumcn  37391  fsumge0cl  37690  fsumreclf  37693  stoweidlem11  37909  stoweidlem17  37915  stoweidlem20  37918  stoweidlem26  37924  stoweidlem30  37929  stoweidlem32  37931  stoweidlem38  37937  stoweidlem44  37943  stirlinglem12  37985  dirkeritg  38002  fourierdlem73  38081  fourierdlem83  38091  fourierdlem112  38120  etransclem23  38160  etransclem35  38172  etransclem48OLD  38185  etransclem48  38186  sge0rnre  38244  sge0cl  38261  sge0fsum  38267  sge0ltfirp  38280  sge0le  38287  sge0split  38289  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0xaddlem1  38313  sge0xaddlem2  38314  omeiunltfirp  38378  carageniuncllem2  38381  hoidmvlelem2  38456  hoidmvlelem3  38457  hoiqssbllem2  38483  fsummsndifre  39137  fsummmodsndifre  39139
  Copyright terms: Public domain W3C validator