Theorem fsumrecl 15759

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2100   ⊆ wss 3959  (class class class)co 7430  Fincfn 8982  ℂcc 11163  ℝcr 11164   + caddc 11168  Σcsu 15711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-rep 5293  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-inf2 9691  ax-cnex 11221  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242  ax-pre-sup 11243

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rmo 3373  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-int 4960  df-iun 5008  df-br 5157  df-opab 5219  df-mpt 5240  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-se 5642  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-pred 6317  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7386  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7885  df-1st 8011  df-2nd 8012  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-fin 8986  df-sup 9492  df-oi 9560  df-card 9989  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-div 11929  df-nn 12275  df-2 12337  df-3 12338  df-n0 12535  df-z 12621  df-uz 12885  df-rp 13039  df-fz 13549  df-fzo 13692  df-seq 14033  df-exp 14093  df-hash 14360  df-cj 15125  df-re 15126  df-im 15127  df-sqrt 15261  df-abs 15262  df-clim 15511  df-sum 15712

This theorem is referenced by:  fsumless  15821  fsumle  15824  fsumlt  15825  fsumabs  15826  o1fsum  15838  isumltss  15873  climcndslem1  15874  climcndslem2  15875  mertenslem1  15909  rpnnen2lem10  16246  prmreclem4  16942  prmreclem5  16943  lebnumlem1  25001  csbren  25441  trirn  25442  rrxmet  25450  rrxdstprj1  25451  ovolfiniun  25544  ovoliunlem1  25545  ovolscalem1  25556  ovolicc2lem4  25563  volfiniun  25590  uniioombllem3a  25627  uniioombllem4  25629  i1fd  25724  itg1cl  25728  i1fadd  25738  i1fmul  25739  dvfsumge  26070  dvfsumabs  26071  dvfsumrlimf  26073  dvfsumlem2  26075  dvfsumlem2OLD  26076  dvfsumlem3  26077  dvfsumlem4  26078  dvfsum2  26083  aaliou3lem5  26398  mtest  26456  mtestbdd  26457  abelthlem7  26491  abelthlem8  26492  log2ublem2  26998  log2ub  27000  birthdaylem3  27004  emcllem1  27047  emcllem2  27048  emcllem3  27049  harmoniclbnd  27060  harmonicubnd  27061  harmonicbnd4  27062  fsumharmonic  27063  ftalem1  27124  ftalem4  27127  ftalem5  27128  chtf  27159  chpf  27174  chpub  27272  logfaclbnd  27274  logexprlim  27277  chtppilimlem1  27525  vmadivsum  27534  vmadivsumb  27535  rplogsumlem1  27536  rplogsumlem2  27537  rpvmasumlem  27539  dchrisumlem2  27542  dchrmusum2  27546  dchrvmasumlem2  27550  dchrvmasumlem3  27551  dchrvmasumiflem1  27553  dchrisum0ff  27559  dchrisum0flblem1  27560  dchrisum0fno1  27563  dchrisum0re  27565  dchrisum0lem1  27568  dchrisum0lem2a  27569  rplogsum  27579  dirith2  27580  mudivsum  27582  mulogsumlem  27583  mulog2sumlem1  27586  mulog2sumlem2  27587  vmalogdivsum2  27590  vmalogdivsum  27591  2vmadivsumlem  27592  logsqvma2  27595  log2sumbnd  27596  selberglem2  27598  selberg  27600  selbergb  27601  selberg2b  27604  chpdifbndlem1  27605  logdivbnd  27608  selberg3lem1  27609  selberg3lem2  27610  selberg3  27611  selberg4lem1  27612  selberg4  27613  pntrsumo1  27617  pntrsumbnd  27618  pntrsumbnd2  27619  selberg3r  27621  selberg4r  27622  selberg34r  27623  pntsf  27625  pntsval2  27628  pntrlog2bndlem1  27629  pntrlog2bndlem2  27630  pntrlog2bndlem3  27631  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  pntrlog2bndlem6  27635  pntrlog2bnd  27636  pntpbnd1  27638  pntpbnd2  27639  pntlemj  27655  pntlemf  27657  pntlemk  27658  pntlemo  27659  axsegconlem2  28875  ax5seglem3  28888  ax5seg  28895  esumpcvgval  33949  esumcvg  33957  sibfof  34212  reprlt  34503  reprgt  34505  reprinfz1  34506  hgt750lemd  34532  hgt750lemb  34540  hgt750lema  34541  hgt750leme  34542  tgoldbachgtde  34544  knoppndvlem5  36267  knoppndvlem11  36273  knoppndvlem14  36276  mettrifi  37505  geomcau  37507  rrnmet  37577  rrndstprj1  37578  rrndstprj2  37579  aks4d1p1p2  41816  sticksstones6  41897  unitscyglem4  41944  sumcubes  42074  fltnltalem  42386  refsumcn  44700  fsumge0cl  45264  fsumreclf  45267  stoweidlem11  45702  stoweidlem17  45708  stoweidlem20  45711  stoweidlem26  45717  stoweidlem30  45721  stoweidlem32  45723  stoweidlem38  45729  stoweidlem44  45735  stirlinglem12  45776  dirkeritg  45793  fourierdlem73  45870  fourierdlem83  45880  fourierdlem112  45909  etransclem23  45948  etransclem35  45960  etransclem48  45973  sge0rnre  46055  sge0cl  46072  sge0fsum  46078  sge0ltfirp  46091  sge0le  46098  sge0split  46100  sge0iunmptlemfi  46104  sge0iunmptlemre  46106  sge0xaddlem1  46124  sge0xaddlem2  46125  sge0seq  46137  omeiunltfirp  46210  carageniuncllem2  46213  hoidmvlelem2  46287  hoidmvlelem3  46288  hoiqssbllem2  46314  fsummsndifre  47014  fsummmodsndifre  47016