Theorem fsumrecl 15677

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.

Step	Hyp	Ref	Expression
1		ax-resscn 11164	. . 3 ⊢ ℝ ⊆ ℂ
2	1	a1i 11	. 2 ⊢ (𝜑 → ℝ ⊆ ℂ)
3		readdcl 11190	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
4	3	adantl 483	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
5		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
6		fsumrecl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
7		0red 11214	. 2 ⊢ (𝜑 → 0 ∈ ℝ)
8	2, 4, 5, 6, 7	fsumcllem 15675	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ⊆ wss 3948  (class class class)co 7406  Fincfn 8936  ℂcc 11105  ℝcr 11106   + caddc 11110  Σcsu 15629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-fz 13482  df-fzo 13625  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630

This theorem is referenced by:  fsumless  15739  fsumle  15742  fsumlt  15743  fsumabs  15744  o1fsum  15756  isumltss  15791  climcndslem1  15792  climcndslem2  15793  mertenslem1  15827  rpnnen2lem10  16163  prmreclem4  16849  prmreclem5  16850  lebnumlem1  24469  csbren  24908  trirn  24909  rrxmet  24917  rrxdstprj1  24918  ovolfiniun  25010  ovoliunlem1  25011  ovolscalem1  25022  ovolicc2lem4  25029  volfiniun  25056  uniioombllem3a  25093  uniioombllem4  25095  i1fd  25190  itg1cl  25194  i1fadd  25204  i1fmul  25205  dvfsumge  25531  dvfsumabs  25532  dvfsumrlimf  25534  dvfsumlem2  25536  dvfsumlem3  25537  dvfsumlem4  25538  dvfsum2  25543  aaliou3lem5  25852  mtest  25908  mtestbdd  25909  abelthlem7  25942  abelthlem8  25943  log2ublem2  26442  log2ub  26444  birthdaylem3  26448  emcllem1  26490  emcllem2  26491  emcllem3  26492  harmoniclbnd  26503  harmonicubnd  26504  harmonicbnd4  26505  fsumharmonic  26506  ftalem1  26567  ftalem4  26570  ftalem5  26571  chtf  26602  chpf  26617  chpub  26713  logfaclbnd  26715  logexprlim  26718  chtppilimlem1  26966  vmadivsum  26975  vmadivsumb  26976  rplogsumlem1  26977  rplogsumlem2  26978  rpvmasumlem  26980  dchrisumlem2  26983  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrisum0ff  27000  dchrisum0flblem1  27001  dchrisum0fno1  27004  dchrisum0re  27006  dchrisum0lem1  27009  dchrisum0lem2a  27010  rplogsum  27020  dirith2  27021  mudivsum  27023  mulogsumlem  27024  mulog2sumlem1  27027  mulog2sumlem2  27028  vmalogdivsum2  27031  vmalogdivsum  27032  2vmadivsumlem  27033  logsqvma2  27036  log2sumbnd  27037  selberglem2  27039  selberg  27041  selbergb  27042  selberg2b  27045  chpdifbndlem1  27046  logdivbnd  27049  selberg3lem1  27050  selberg3lem2  27051  selberg3  27052  selberg4lem1  27053  selberg4  27054  pntrsumo1  27058  pntrsumbnd  27059  pntrsumbnd2  27060  selberg3r  27062  selberg4r  27063  selberg34r  27064  pntsf  27066  pntsval2  27069  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntpbnd1  27079  pntpbnd2  27080  pntlemj  27096  pntlemf  27098  pntlemk  27099  pntlemo  27100  axsegconlem2  28166  ax5seglem3  28179  ax5seg  28186  esumpcvgval  33065  esumcvg  33073  sibfof  33328  reprlt  33620  reprgt  33622  reprinfz1  33623  hgt750lemd  33649  hgt750lemb  33657  hgt750lema  33658  hgt750leme  33659  tgoldbachgtde  33661  gg-dvfsumlem2  35172  knoppndvlem5  35381  knoppndvlem11  35387  knoppndvlem14  35390  mettrifi  36614  geomcau  36616  rrnmet  36686  rrndstprj1  36687  rrndstprj2  36688  aks4d1p1p2  40924  sticksstones6  40956  sumcubes  41207  fltnltalem  41401  refsumcn  43700  fsumge0cl  44276  fsumreclf  44279  stoweidlem11  44714  stoweidlem17  44720  stoweidlem20  44723  stoweidlem26  44729  stoweidlem30  44733  stoweidlem32  44735  stoweidlem38  44741  stoweidlem44  44747  stirlinglem12  44788  dirkeritg  44805  fourierdlem73  44882  fourierdlem83  44892  fourierdlem112  44921  etransclem23  44960  etransclem35  44972  etransclem48  44985  sge0rnre  45067  sge0cl  45084  sge0fsum  45090  sge0ltfirp  45103  sge0le  45110  sge0split  45112  sge0iunmptlemfi  45116  sge0iunmptlemre  45118  sge0xaddlem1  45136  sge0xaddlem2  45137  sge0seq  45149  omeiunltfirp  45222  carageniuncllem2  45225  hoidmvlelem2  45299  hoidmvlelem3  45300  hoiqssbllem2  45326  fsummsndifre  46027  fsummmodsndifre  46029