Theorem readdcld 11287

Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
readdcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
readdcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		readdcl 11235	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151   + caddc 11155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11213

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  ltadd2  11362  readdcan  11432  addrid  11438  leadd1  11728  le2add  11742  lesub2  11755  lesub3d  11878  supaddc  12232  supadd  12233  cju  12259  nnne0  12297  div4p1lem1div2  12518  difgtsumgt  12576  eluzmn  12882  rpnnen1lem5  13020  addlelt  13146  xralrple  13243  xov1plusxeqvd  13534  zltaddlt1le  13541  elincfzoext  13758  fladdz  13861  2tnp1ge0ge0  13865  flhalf  13866  fldiv  13896  modaddmodup  13971  modaddmodlo  13972  addmodlteq  13983  discr1  14274  discr  14275  ccatalpha  14627  2cshw  14847  remim  15152  remullem  15163  01sqrexlem7  15283  absrele  15343  abstri  15365  abs3lem  15373  amgm2  15404  bhmafibid1  15500  mulcn2  15628  o1add  15646  o1sub  15648  lo1add  15659  caucvgrlem  15705  iseraltlem2  15715  iseraltlem3  15716  fsumabs  15833  o1fsum  15845  climcndslem2  15882  tanhlt1  16192  eirrlem  16236  ruclem1  16263  ruclem2  16264  ruclem3  16265  ltoddhalfle  16394  bitscmp  16471  sadcaddlem  16490  sadasslem  16503  smuval2  16515  iserodd  16868  prmreclem4  16952  4sqlem5  16975  4sqlem6  16976  4sqlem12  16989  4sqlem15  16992  4sqlem16  16993  prmgaplem7  17090  prmgaplem8  17091  2expltfac  17126  cshwshashlem2  17130  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulgsum  22885  prdsxmetlem  24393  xblss2ps  24426  metustexhalf  24584  nrmmetd  24602  ngptgp  24664  nlmvscnlem2  24721  nlmvscnlem1  24722  nmotri  24775  nghmplusg  24776  blcvx  24833  iccntr  24856  icccmplem2  24858  reconnlem2  24862  metdcnlem  24871  metnrmlem3  24896  cnllycmp  25001  lebnumii  25011  tcphcphlem1  25282  ipcnlem2  25291  ipcnlem1  25292  csbren  25446  trirn  25447  minveclem2  25473  minveclem3b  25475  minveclem4  25479  ivthlem2  25500  ovolgelb  25528  ovollb2lem  25536  ovolunlem1a  25544  ovolunlem1  25545  ovolfiniun  25549  ovoliunlem1  25550  ovoliunlem2  25551  ovolshftlem1  25557  ovolscalem1  25561  ovolicopnf  25572  ismbl2  25575  nulmbl2  25584  unmbl  25585  voliunlem2  25599  ioombl1lem2  25607  ioombl1lem4  25609  ioombl1  25610  ioorcl2  25620  uniioombllem1  25629  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombl  25637  opnmbllem  25649  volcn  25654  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1fseqlem4  25767  mbfi1fseqlem6  25769  itg2splitlem  25797  itg2split  25798  itg2monolem3  25801  itg2addlem  25807  ibladdlem  25869  itgaddlem1  25872  itgaddlem2  25873  iblabslem  25877  iblabs  25878  dvferm1lem  26036  dvferm2lem  26038  dvlip2  26048  lhop1lem  26066  lhop1  26067  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  dvcvx  26073  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  ftc1lem4  26094  coemullem  26303  ulmbdd  26455  ulmcn  26456  ulmdvlem1  26457  radcnvle  26477  pserdvlem1  26485  pserdv  26487  abelthlem7  26496  pilem2  26510  pilem3  26511  cosordlem  26586  abslogle  26674  logccv  26719  cxpaddle  26809  ang180lem2  26867  heron  26895  atanlogaddlem  26970  atans2  26988  cxp2limlem  27033  scvxcvx  27043  jensenlem2  27045  amgmlem  27047  logdiflbnd  27052  harmonicbnd4  27068  fsumharmonic  27069  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  lgambdd  27094  lgamucov  27095  regamcl  27118  ftalem5  27134  efnnfsumcl  27160  efchtdvds  27216  chtublem  27269  chtub  27270  logfaclbnd  27280  perfectlem2  27288  bposlem7  27348  bposlem9  27350  lgsdirprm  27389  gausslemma2dlem1a  27423  2sqlem8  27484  chpchtlim  27537  vmadivsumb  27541  rplogsumlem1  27542  dchrisumlem2  27548  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0re  27571  dchrisum0lem1b  27573  mulog2sumlem1  27592  mulog2sumlem2  27593  logsqvma2  27601  log2sumbnd  27602  selberglem2  27604  selbergb  27607  selberg2b  27610  chpdifbndlem1  27611  chpdifbndlem2  27612  selberg3lem2  27616  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrsumbnd2  27625  selberg3r  27627  selberg34r  27629  pntsf  27631  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem2a  27648  pntibndlem2  27649  pntibndlem3  27650  pntlemg  27656  pntlemr  27660  pntlemk  27664  pntlemo  27665  pntlem3  27667  abvcxp  27673  padicabv  27688  ostth2lem2  27692  ostth3  27696  brbtwn2  28934  axsegconlem8  28953  axsegconlem10  28955  axpaschlem  28969  axpasch  28970  axeuclidlem  28991  axcontlem2  28994  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  vacn  30722  smcnlem  30725  ubthlem2  30899  minvecolem2  30903  minvecolem3  30904  minvecolem4  30908  minvecolem5  30909  nmoptrii  32122  hstle  32258  staddi  32274  stadd3i  32276  lt2addrd  32761  nndiffz1  32794  wrdt2ind  32922  cshwrnid  32930  fsumrp0cl  33008  pmtrto1cl  33101  fzto1st  33105  psgnfzto1st  33107  1smat1  33764  sqsscirc1  33868  cnre2csqlem  33870  tpr2rico  33872  nexple  33989  dya2iocress  34255  dya2iocbrsiga  34256  dya2icobrsiga  34257  dya2icoseg  34258  dya2iocucvr  34265  sxbrsigalem2  34267  omssubaddlem  34280  fibp1  34382  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemsgt1  34491  ballotlemsel1i  34493  plymulx0  34540  breprexplemc  34625  breprexp  34626  logdivsqrle  34643  resconn  35230  faclim  35725  dnizphlfeqhlf  36458  dnibndlem4  36463  dnibndlem6  36465  dnibndlem8  36467  dnibndlem9  36468  dnibndlem10  36469  dnibndlem11  36470  dnibndlem13  36472  dnibnd  36473  knoppcnlem4  36478  unblimceq0lem  36488  unblimceq0  36489  unbdqndv2lem1  36491  poimirlem29  37635  heicant  37641  opnmbllem0  37642  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  mbfposadd  37653  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  ibladdnclem  37662  itgaddnclem1  37664  itgaddnclem2  37665  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  ftc1cnnclem  37677  ftc1anclem4  37682  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirclem5  37698  mettrifi  37743  isbnd3  37770  ssbnd  37774  cntotbnd  37782  heibor1lem  37795  bfplem2  37809  rrnequiv  37821  iccbnd  37826  lcmineqlem18  42027  lcmineqlem20  42029  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  posbezout  42081  aks6d1c1  42097  aks6d1c2  42111  2np3bcnp1  42125  2ap1caineq  42126  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  bcle2d  42160  aks6d1c7lem1  42161  metakunt29  42214  2xp3dxp2ge1d  42222  factwoffsmonot  42223  readdridaddlidd  42277  resubeulem1  42381  resubeulem2  42382  resubeu  42383  readdsub  42390  reladdrsub  42391  resubidaddlidlem  42400  renegid2  42419  sn-it0e0  42421  sn-0tie0  42445  sn-addlt0d  42452  sn-addgt0d  42453  cnreeu  42476  dffltz  42620  fltnltalem  42648  fltnlta  42649  3cubeslem1  42671  pellexlem2  42817  pell1qrge1  42857  pell14qrgapw  42863  pellqrexplicit  42864  pellqrex  42866  pellfundge  42869  pellfundgt1  42870  rmspecfund  42896  rmxycomplete  42905  ltrmynn0  42936  jm2.24nn  42947  jm2.24  42951  fzmaxdif  42969  jm2.26lem3  42989  jm3.1lem2  43006  areaquad  43204  sqrtcvallem4  43628  sqrtcvallem5  43629  sqrtcval  43630  imo72b2lem0  44154  hashnzfzclim  44317  binomcxplemnotnn0  44351  zltlesub  45235  lt3addmuld  45251  absnpncan2d  45252  fperiodmullem  45253  lt4addmuld  45256  absnpncan3d  45257  leadd12dd  45266  supxrgelem  45286  supxrge  45287  ltadd12dd  45292  xralrple2  45303  infxr  45316  infleinflem2  45320  xralrple4  45322  xralrple3  45323  xrralrecnnle  45332  eliooshift  45458  iccshift  45470  iooshift  45474  iooiinicc  45494  iooiinioc  45508  fsumnncl  45527  climinf  45561  climsuselem1  45562  sumnnodd  45585  lptre2pt  45595  addlimc  45603  0ellimcdiv  45604  limclner  45606  climleltrp  45631  liminfltlem  45759  fperdvper  45874  dvdivbd  45878  dvbdfbdioolem2  45884  dvbdfbdioo  45885  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvxpaek  45895  dvnmul  45898  iblsplit  45921  iblspltprt  45928  itgspltprt  45934  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem1  45956  stoweidlem11  45966  stoweidlem13  45968  stoweidlem14  45969  stoweidlem20  45975  stoweidlem21  45976  stoweidlem26  45981  stoweidlem44  45999  stoweidlem60  46015  wallispilem3  46022  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem1  46029  stirlinglem3  46031  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  dirker2re  46047  dirkerval2  46049  dirkerre  46050  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkeritg  46057  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem4  46066  fourierdlem5  46067  fourierdlem6  46068  fourierdlem7  46069  fourierdlem9  46071  fourierdlem10  46072  fourierdlem18  46080  fourierdlem19  46081  fourierdlem20  46082  fourierdlem26  46088  fourierdlem28  46090  fourierdlem30  46092  fourierdlem35  46097  fourierdlem40  46102  fourierdlem41  46103  fourierdlem42  46104  fourierdlem47  46108  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem53  46114  fourierdlem57  46118  fourierdlem59  46120  fourierdlem60  46121  fourierdlem61  46122  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem66  46127  fourierdlem68  46129  fourierdlem71  46132  fourierdlem72  46133  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem80  46141  fourierdlem81  46142  fourierdlem82  46143  fourierdlem83  46144  fourierdlem84  46145  fourierdlem87  46148  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem94  46155  fourierdlem95  46156  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  qndenserrnbllem  46249  ioorrnopnlem  46259  ioorrnopnxrlem  46261  sge0xaddlem1  46388  sge0xaddlem2  46389  omeiunltfirp  46474  carageniuncllem2  46477  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoiqssbllem1  46577  hoiqssbllem2  46578  hoiqssbllem3  46579  hspmbllem2  46582  hspmbllem3  46583  ovolval5lem1  46607  iinhoiicclem  46628  iinhoiicc  46629  iunhoiioolem  46630  iccvonmbllem  46633  vonioolem1  46635  vonioolem2  46636  vonicclem1  46638  vonicclem2  46639  preimaleiinlt  46676  salpreimaltle  46681  smfaddlem1  46718  smfadd  46720  smflimlem3  46728  smflimlem4  46729  smflimlem6  46731  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  zm1nn  47251  requad01  47545  requad1  47546  requad2  47547  perfectALTVlem2  47646  nnsum4primesevenALTV  47725  bgoldbtbndlem2  47730  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  dignn0flhalflem1  48464  affinecomb1  48551  resum2sqcl  48555  2sphere  48598  line2  48601  itsclc0lem1  48605  itscnhlc0yqe  48608  itsclquadb  48625  2itscp  48630  itscnhlinecirc02plem1  48631  itscnhlinecirc02plem3  48633  itscnhlinecirc02p  48634  inlinecirc02plem  48635  amgmwlem  49032