Theorem fsumrecl 15691

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 11090	. . 3 ⊢ ℝ ⊆ ℂ
2	1	a1i 11	. 2 ⊢ (𝜑 → ℝ ⊆ ℂ)
3		readdcl 11116	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
5		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
6		fsumrecl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
7		0red 11142	. 2 ⊢ (𝜑 → 0 ∈ ℝ)
8	2, 4, 5, 6, 7	fsumcllem 15689	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3890  (class class class)co 7362  Fincfn 8888  ℂcc 11031  ℝcr 11032   + caddc 11036  Σcsu 15643

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-inf2 9557  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110  ax-pre-sup 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-se 5580  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-isom 6503  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7813  df-1st 7937  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-1o 8400  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-fin 8892  df-sup 9350  df-oi 9420  df-card 9858  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803  df-nn 12170  df-2 12239  df-3 12240  df-n0 12433  df-z 12520  df-uz 12784  df-rp 12938  df-fz 13457  df-fzo 13604  df-seq 13959  df-exp 14019  df-hash 14288  df-cj 15056  df-re 15057  df-im 15058  df-sqrt 15192  df-abs 15193  df-clim 15445  df-sum 15644

This theorem is referenced by:  fsumless  15754  fsumle  15757  fsumlt  15758  fsumabs  15759  o1fsum  15771  isumltss  15808  climcndslem1  15809  climcndslem2  15810  mertenslem1  15844  rpnnen2lem10  16185  prmreclem4  16885  prmreclem5  16886  lebnumlem1  24942  csbren  25380  trirn  25381  rrxmet  25389  rrxdstprj1  25390  ovolfiniun  25482  ovoliunlem1  25483  ovolscalem1  25494  ovolicc2lem4  25501  volfiniun  25528  uniioombllem3a  25565  uniioombllem4  25567  i1fd  25662  itg1cl  25666  i1fadd  25676  i1fmul  25677  dvfsumge  26003  dvfsumabs  26004  dvfsumrlimf  26006  dvfsumlem2  26008  dvfsumlem3  26009  dvfsumlem4  26010  dvfsum2  26015  aaliou3lem5  26328  mtest  26386  mtestbdd  26387  abelthlem7  26420  abelthlem8  26421  log2ublem2  26928  log2ub  26930  birthdaylem3  26934  emcllem1  26977  emcllem2  26978  emcllem3  26979  harmoniclbnd  26990  harmonicubnd  26991  harmonicbnd4  26992  fsumharmonic  26993  ftalem1  27054  ftalem4  27057  ftalem5  27058  chtf  27089  chpf  27104  chpub  27201  logfaclbnd  27203  logexprlim  27206  chtppilimlem1  27454  vmadivsum  27463  vmadivsumb  27464  rplogsumlem1  27465  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrisum0ff  27488  dchrisum0flblem1  27489  dchrisum0fno1  27492  dchrisum0re  27494  dchrisum0lem1  27497  dchrisum0lem2a  27498  rplogsum  27508  dirith2  27509  mudivsum  27511  mulogsumlem  27512  mulog2sumlem1  27515  mulog2sumlem2  27516  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  logsqvma2  27524  log2sumbnd  27525  selberglem2  27527  selberg  27529  selbergb  27530  selberg2b  27533  chpdifbndlem1  27534  logdivbnd  27537  selberg3lem1  27538  selberg3lem2  27539  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrsumo1  27546  pntrsumbnd  27547  pntrsumbnd2  27548  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntsf  27554  pntsval2  27557  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1  27567  pntpbnd2  27568  pntlemj  27584  pntlemf  27586  pntlemk  27587  pntlemo  27588  axsegconlem2  29005  ax5seglem3  29018  ax5seg  29025  esumpcvgval  34242  esumcvg  34250  sibfof  34504  reprlt  34783  reprgt  34785  reprinfz1  34786  hgt750lemd  34812  hgt750lemb  34820  hgt750lema  34821  hgt750leme  34822  tgoldbachgtde  34824  knoppndvlem5  36796  knoppndvlem11  36802  knoppndvlem14  36805  mettrifi  38098  geomcau  38100  rrnmet  38170  rrndstprj1  38171  rrndstprj2  38172  aks4d1p1p2  42529  sticksstones6  42610  unitscyglem4  42657  sumcubes  42765  fltnltalem  43115  refsumcn  45485  fsumge0cl  46027  fsumreclf  46030  stoweidlem11  46463  stoweidlem17  46469  stoweidlem20  46472  stoweidlem26  46478  stoweidlem30  46482  stoweidlem32  46484  stoweidlem38  46490  stoweidlem44  46496  stirlinglem12  46537  dirkeritg  46554  fourierdlem73  46631  fourierdlem83  46641  fourierdlem112  46670  etransclem23  46709  etransclem35  46721  etransclem48  46734  sge0rnre  46816  sge0cl  46833  sge0fsum  46839  sge0ltfirp  46852  sge0le  46859  sge0split  46861  sge0iunmptlemfi  46865  sge0iunmptlemre  46867  sge0xaddlem1  46885  sge0xaddlem2  46886  sge0seq  46898  omeiunltfirp  46971  carageniuncllem2  46974  hoidmvlelem2  47048  hoidmvlelem3  47049  hoiqssbllem2  47075  fsummsndifre  47846  fsummmodsndifre  47848