Theorem readdcld 11203

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 11151	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067   + caddc 11071

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

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

This theorem is referenced by:  ltadd2  11278  readdcan  11348  addrid  11354  leadd1  11646  le2add  11660  lesub2  11673  lesub3d  11796  le2addd  11797  supaddc  12150  supadd  12151  cju  12182  nnne0  12220  div4p1lem1div2  12437  difgtsumgt  12495  eluzmn  12800  rpnnen1lem5  12940  addlelt  13067  xralrple  13165  xov1plusxeqvd  13459  zltaddlt1le  13466  elincfzoext  13684  fladdz  13787  2tnp1ge0ge0  13791  flhalf  13792  fldiv  13822  modaddb  13871  modaddmodup  13899  modaddmodlo  13900  addmodlteq  13911  discr1  14204  discr  14205  ccatalpha  14558  2cshw  14778  remim  15083  remullem  15094  01sqrexlem7  15214  absrele  15274  abstri  15297  abs3lem  15305  amgm2  15336  bhmafibid1  15434  mulcn2  15562  o1add  15580  o1sub  15582  lo1add  15593  caucvgrlem  15639  iseraltlem2  15649  iseraltlem3  15650  fsumabs  15767  o1fsum  15779  climcndslem2  15816  tanhlt1  16128  eirrlem  16172  ruclem1  16199  ruclem2  16200  ruclem3  16201  ltoddhalfle  16331  bitscmp  16408  sadcaddlem  16427  sadasslem  16440  smuval2  16452  iserodd  16806  prmreclem4  16890  4sqlem5  16913  4sqlem6  16914  4sqlem12  16927  4sqlem15  16930  4sqlem16  16931  prmgaplem7  17028  prmgaplem8  17029  2expltfac  17063  cshwshashlem2  17067  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  prdsxmetlem  24256  xblss2ps  24289  metustexhalf  24444  nrmmetd  24462  ngptgp  24524  nlmvscnlem2  24573  nlmvscnlem1  24574  nmotri  24627  nghmplusg  24628  blcvx  24686  iccntr  24710  icccmplem2  24712  reconnlem2  24716  metdcnlem  24725  metnrmlem3  24750  cnllycmp  24855  lebnumii  24865  tcphcphlem1  25135  ipcnlem2  25144  ipcnlem1  25145  csbren  25299  trirn  25300  minveclem2  25326  minveclem3b  25328  minveclem4  25332  ivthlem2  25353  ovolgelb  25381  ovollb2lem  25389  ovolunlem1a  25397  ovolunlem1  25398  ovolfiniun  25402  ovoliunlem1  25403  ovoliunlem2  25404  ovolshftlem1  25410  ovolscalem1  25414  ovolicopnf  25425  ismbl2  25428  nulmbl2  25437  unmbl  25438  voliunlem2  25452  ioombl1lem2  25460  ioombl1lem4  25462  ioombl1  25463  ioorcl2  25473  uniioombllem1  25482  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombl  25490  opnmbllem  25502  volcn  25507  itg1addlem4  25600  mbfi1fseqlem4  25619  mbfi1fseqlem6  25621  itg2splitlem  25649  itg2split  25650  itg2monolem3  25653  itg2addlem  25659  ibladdlem  25721  itgaddlem1  25724  itgaddlem2  25725  iblabslem  25729  iblabs  25730  dvferm1lem  25888  dvferm2lem  25890  dvlip2  25900  lhop1lem  25918  lhop1  25919  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  dvcvx  25925  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  ftc1lem4  25946  coemullem  26155  ulmbdd  26307  ulmcn  26308  ulmdvlem1  26309  radcnvle  26329  pserdvlem1  26337  pserdv  26339  abelthlem7  26348  pilem2  26362  pilem3  26363  cosordlem  26439  abslogle  26527  logccv  26572  cxpaddle  26662  ang180lem2  26720  heron  26748  atanlogaddlem  26823  atans2  26841  cxp2limlem  26886  scvxcvx  26896  jensenlem2  26898  amgmlem  26900  logdiflbnd  26905  harmonicbnd4  26921  fsumharmonic  26922  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  lgambdd  26947  lgamucov  26948  regamcl  26971  ftalem5  26987  efnnfsumcl  27013  efchtdvds  27069  chtublem  27122  chtub  27123  logfaclbnd  27133  perfectlem2  27141  bposlem7  27201  bposlem9  27203  lgsdirprm  27242  gausslemma2dlem1a  27276  2sqlem8  27337  chpchtlim  27390  vmadivsumb  27394  rplogsumlem1  27395  dchrisumlem2  27401  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0re  27424  dchrisum0lem1b  27426  mulog2sumlem1  27445  mulog2sumlem2  27446  logsqvma2  27454  log2sumbnd  27455  selberglem2  27457  selbergb  27460  selberg2b  27463  chpdifbndlem1  27464  chpdifbndlem2  27465  selberg3lem2  27469  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrsumbnd2  27478  selberg3r  27480  selberg34r  27482  pntsf  27484  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem2a  27501  pntibndlem2  27502  pntibndlem3  27503  pntlemg  27509  pntlemr  27513  pntlemk  27517  pntlemo  27518  pntlem3  27520  abvcxp  27526  padicabv  27541  ostth2lem2  27545  ostth3  27549  brbtwn2  28832  axsegconlem8  28851  axsegconlem10  28853  axpaschlem  28867  axpasch  28868  axeuclidlem  28889  axcontlem2  28892  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  vacn  30623  smcnlem  30626  ubthlem2  30800  minvecolem2  30804  minvecolem3  30805  minvecolem4  30809  minvecolem5  30810  nmoptrii  32023  hstle  32159  staddi  32175  stadd3i  32177  lt2addrd  32674  nndiffz1  32709  nexple  32769  wrdt2ind  32875  cshwrnid  32883  fsumrp0cl  32962  pmtrto1cl  33056  fzto1st  33060  psgnfzto1st  33062  constrresqrtcl  33767  cos9thpiminplylem1  33772  1smat1  33794  sqsscirc1  33898  cnre2csqlem  33900  tpr2rico  33902  dya2iocress  34265  dya2iocbrsiga  34266  dya2icobrsiga  34267  dya2icoseg  34268  dya2iocucvr  34275  sxbrsigalem2  34277  omssubaddlem  34290  fibp1  34392  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsgt1  34502  ballotlemsel1i  34504  plymulx0  34538  breprexplemc  34623  breprexp  34624  logdivsqrle  34641  resconn  35233  faclim  35733  dnizphlfeqhlf  36464  dnibndlem4  36469  dnibndlem6  36471  dnibndlem8  36473  dnibndlem9  36474  dnibndlem10  36475  dnibndlem11  36476  dnibndlem13  36478  dnibnd  36479  knoppcnlem4  36484  unblimceq0lem  36494  unblimceq0  36495  unbdqndv2lem1  36497  poimirlem29  37643  heicant  37649  opnmbllem0  37650  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  mbfposadd  37661  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem1  37672  itgaddnclem2  37673  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  ftc1cnnclem  37685  ftc1anclem4  37690  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirclem5  37706  mettrifi  37751  isbnd3  37778  ssbnd  37782  cntotbnd  37790  heibor1lem  37803  bfplem2  37817  rrnequiv  37829  iccbnd  37834  lcmineqlem18  42034  lcmineqlem20  42036  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  posbezout  42088  aks6d1c1  42104  aks6d1c2  42118  2np3bcnp1  42132  2ap1caineq  42133  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  bcle2d  42167  aks6d1c7lem1  42168  readdridaddlidd  42246  resubeulem1  42363  resubeulem2  42364  resubeu  42365  readdsub  42372  reladdrsub  42373  resubidaddlidlem  42382  renegid2  42402  sn-it0e0  42404  sn-0tie0  42439  sn-addlt0d  42446  sn-addgt0d  42447  cnreeu  42478  dffltz  42622  fltnltalem  42650  fltnlta  42651  3cubeslem1  42672  pellexlem2  42818  pell1qrge1  42858  pell14qrgapw  42864  pellqrexplicit  42865  pellqrex  42867  pellfundge  42870  pellfundgt1  42871  rmspecfund  42897  rmxycomplete  42906  ltrmynn0  42937  jm2.24nn  42948  jm2.24  42952  fzmaxdif  42970  jm2.26lem3  42990  jm3.1lem2  43007  areaquad  43205  sqrtcvallem4  43628  sqrtcvallem5  43629  sqrtcval  43630  imo72b2lem0  44154  hashnzfzclim  44311  binomcxplemnotnn0  44345  zltlesub  45283  lt3addmuld  45299  absnpncan2d  45300  fperiodmullem  45301  lt4addmuld  45304  absnpncan3d  45305  supxrgelem  45333  supxrge  45334  ltadd12dd  45339  xralrple2  45350  infxr  45363  infleinflem2  45367  xralrple4  45369  xralrple3  45370  xrralrecnnle  45379  eliooshift  45504  iccshift  45516  iooshift  45520  iooiinicc  45540  iooiinioc  45554  fsumnncl  45570  climinf  45604  climsuselem1  45605  sumnnodd  45628  lptre2pt  45638  addlimc  45646  0ellimcdiv  45647  limclner  45649  climleltrp  45674  liminfltlem  45802  fperdvper  45917  dvdivbd  45921  dvbdfbdioolem2  45927  dvbdfbdioo  45928  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvxpaek  45938  dvnmul  45941  iblsplit  45964  iblspltprt  45971  itgspltprt  45977  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem1  45999  stoweidlem11  46009  stoweidlem13  46011  stoweidlem14  46012  stoweidlem20  46018  stoweidlem21  46019  stoweidlem26  46024  stoweidlem44  46042  stoweidlem60  46058  wallispilem3  46065  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem1  46072  stirlinglem3  46074  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  dirker2re  46090  dirkerval2  46092  dirkerre  46093  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkeritg  46100  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem4  46109  fourierdlem5  46110  fourierdlem6  46111  fourierdlem7  46112  fourierdlem9  46114  fourierdlem10  46115  fourierdlem18  46123  fourierdlem19  46124  fourierdlem20  46125  fourierdlem26  46131  fourierdlem28  46133  fourierdlem30  46135  fourierdlem35  46140  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem47  46151  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem53  46157  fourierdlem57  46161  fourierdlem59  46163  fourierdlem60  46164  fourierdlem61  46165  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem66  46170  fourierdlem68  46172  fourierdlem71  46175  fourierdlem72  46176  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem80  46184  fourierdlem81  46185  fourierdlem82  46186  fourierdlem83  46187  fourierdlem84  46188  fourierdlem87  46191  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem93  46197  fourierdlem94  46198  fourierdlem95  46199  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  qndenserrnbllem  46292  ioorrnopnlem  46302  ioorrnopnxrlem  46304  sge0xaddlem1  46431  sge0xaddlem2  46432  omeiunltfirp  46517  carageniuncllem2  46520  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoiqssbllem1  46620  hoiqssbllem2  46621  hoiqssbllem3  46622  hspmbllem2  46625  hspmbllem3  46626  ovolval5lem1  46650  iinhoiicclem  46671  iinhoiicc  46672  iunhoiioolem  46673  iccvonmbllem  46676  vonioolem1  46678  vonioolem2  46679  vonicclem1  46681  vonicclem2  46682  preimaleiinlt  46719  salpreimaltle  46724  smfaddlem1  46761  smfadd  46763  smflimlem3  46771  smflimlem4  46772  smflimlem6  46774  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  ormkglobd  46873  zm1nn  47303  requad01  47622  requad1  47623  requad2  47624  perfectALTVlem2  47723  nnsum4primesevenALTV  47802  bgoldbtbndlem2  47807  gpgvtxedg0  48054  gpgvtxedg1  48055  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  dignn0flhalflem1  48604  affinecomb1  48691  resum2sqcl  48695  2sphere  48738  line2  48741  itsclc0lem1  48745  itscnhlc0yqe  48748  itsclquadb  48765  2itscp  48770  itscnhlinecirc02plem1  48771  itscnhlinecirc02plem3  48773  itscnhlinecirc02p  48774  inlinecirc02plem  48775  amgmwlem  49791