Theorem fsumrecl 15722

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098   ⊆ wss 3949  (class class class)co 7426  Fincfn 8972  ℂcc 11146  ℝcr 11147   + caddc 11151  Σcsu 15674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-inf2 9674  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-1st 8001  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-er 8733  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-sup 9475  df-oi 9543  df-card 9972  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-n0 12513  df-z 12599  df-uz 12863  df-rp 13017  df-fz 13527  df-fzo 13670  df-seq 14009  df-exp 14069  df-hash 14332  df-cj 15088  df-re 15089  df-im 15090  df-sqrt 15224  df-abs 15225  df-clim 15474  df-sum 15675

This theorem is referenced by:  fsumless  15784  fsumle  15787  fsumlt  15788  fsumabs  15789  o1fsum  15801  isumltss  15836  climcndslem1  15837  climcndslem2  15838  mertenslem1  15872  rpnnen2lem10  16209  prmreclem4  16897  prmreclem5  16898  lebnumlem1  24915  csbren  25355  trirn  25356  rrxmet  25364  rrxdstprj1  25365  ovolfiniun  25458  ovoliunlem1  25459  ovolscalem1  25470  ovolicc2lem4  25477  volfiniun  25504  uniioombllem3a  25541  uniioombllem4  25543  i1fd  25638  itg1cl  25642  i1fadd  25652  i1fmul  25653  dvfsumge  25984  dvfsumabs  25985  dvfsumrlimf  25987  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsum2  25997  aaliou3lem5  26310  mtest  26368  mtestbdd  26369  abelthlem7  26403  abelthlem8  26404  log2ublem2  26907  log2ub  26909  birthdaylem3  26913  emcllem1  26956  emcllem2  26957  emcllem3  26958  harmoniclbnd  26969  harmonicubnd  26970  harmonicbnd4  26971  fsumharmonic  26972  ftalem1  27033  ftalem4  27036  ftalem5  27037  chtf  27068  chpf  27083  chpub  27181  logfaclbnd  27183  logexprlim  27186  chtppilimlem1  27434  vmadivsum  27443  vmadivsumb  27444  rplogsumlem1  27445  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlem2  27451  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrisum0ff  27468  dchrisum0flblem1  27469  dchrisum0fno1  27472  dchrisum0re  27474  dchrisum0lem1  27477  dchrisum0lem2a  27478  rplogsum  27488  dirith2  27489  mudivsum  27491  mulogsumlem  27492  mulog2sumlem1  27495  mulog2sumlem2  27496  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  logsqvma2  27504  log2sumbnd  27505  selberglem2  27507  selberg  27509  selbergb  27510  selberg2b  27513  chpdifbndlem1  27514  logdivbnd  27517  selberg3lem1  27518  selberg3lem2  27519  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrsumo1  27526  pntrsumbnd  27527  pntrsumbnd2  27528  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntsf  27534  pntsval2  27537  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1  27547  pntpbnd2  27548  pntlemj  27564  pntlemf  27566  pntlemk  27567  pntlemo  27568  axsegconlem2  28757  ax5seglem3  28770  ax5seg  28777  esumpcvgval  33738  esumcvg  33746  sibfof  34001  reprlt  34292  reprgt  34294  reprinfz1  34295  hgt750lemd  34321  hgt750lemb  34329  hgt750lema  34330  hgt750leme  34331  tgoldbachgtde  34333  knoppndvlem5  36032  knoppndvlem11  36038  knoppndvlem14  36041  mettrifi  37271  geomcau  37273  rrnmet  37343  rrndstprj1  37344  rrndstprj2  37345  aks4d1p1p2  41581  sticksstones6  41663  sumcubes  41922  fltnltalem  42135  refsumcn  44441  fsumge0cl  45008  fsumreclf  45011  stoweidlem11  45446  stoweidlem17  45452  stoweidlem20  45455  stoweidlem26  45461  stoweidlem30  45465  stoweidlem32  45467  stoweidlem38  45473  stoweidlem44  45479  stirlinglem12  45520  dirkeritg  45537  fourierdlem73  45614  fourierdlem83  45624  fourierdlem112  45653  etransclem23  45692  etransclem35  45704  etransclem48  45717  sge0rnre  45799  sge0cl  45816  sge0fsum  45822  sge0ltfirp  45835  sge0le  45842  sge0split  45844  sge0iunmptlemfi  45848  sge0iunmptlemre  45850  sge0xaddlem1  45868  sge0xaddlem2  45869  sge0seq  45881  omeiunltfirp  45954  carageniuncllem2  45957  hoidmvlelem2  46031  hoidmvlelem3  46032  hoiqssbllem2  46058  fsummsndifre  46759  fsummmodsndifre  46761