Theorem readdcld 11172

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7363  ℝcr 11035   + caddc 11039

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  ltadd2  11248  readdcan  11318  addrid  11324  leadd1  11616  le2add  11630  lesub2  11643  lesub3d  11766  le2addd  11767  supaddc  12121  supadd  12122  cju  12153  nnne0  12209  div4p1lem1div2  12430  difgtsumgt  12488  eluzmn  12793  rpnnen1lem5  12929  addlelt  13056  xralrple  13155  xov1plusxeqvd  13449  zltaddlt1le  13456  elincfzoext  13676  fladdz  13782  2tnp1ge0ge0  13786  flhalf  13787  fldiv  13817  modaddb  13866  modaddmodup  13894  modaddmodlo  13895  addmodlteq  13906  discr1  14199  discr  14200  ccatalpha  14554  2cshw  14773  remim  15077  remullem  15088  01sqrexlem7  15208  absrele  15268  abstri  15291  abs3lem  15299  amgm2  15330  bhmafibid1  15428  mulcn2  15556  o1add  15574  o1sub  15576  lo1add  15587  caucvgrlem  15633  iseraltlem2  15643  iseraltlem3  15644  fsumabs  15762  o1fsum  15774  climcndslem2  15813  tanhlt1  16125  eirrlem  16169  ruclem1  16196  ruclem2  16197  ruclem3  16198  ltoddhalfle  16328  bitscmp  16405  sadcaddlem  16424  sadasslem  16437  smuval2  16449  iserodd  16804  prmreclem4  16888  4sqlem5  16911  4sqlem6  16912  4sqlem12  16925  4sqlem15  16928  4sqlem16  16929  prmgaplem7  17026  prmgaplem8  17027  2expltfac  17061  cshwshashlem2  17065  chfacfscmul0  22848  chfacfscmulgsum  22850  chfacfpmmul0  22852  chfacfpmmulgsum  22854  prdsxmetlem  24358  xblss2ps  24391  metustexhalf  24546  nrmmetd  24564  ngptgp  24626  nlmvscnlem2  24675  nlmvscnlem1  24676  nmotri  24729  nghmplusg  24730  blcvx  24788  iccntr  24812  icccmplem2  24814  reconnlem2  24818  metdcnlem  24827  metnrmlem3  24852  cnllycmp  24948  lebnumii  24958  tcphcphlem1  25227  ipcnlem2  25236  ipcnlem1  25237  csbren  25391  trirn  25392  minveclem2  25418  minveclem3b  25420  minveclem4  25424  ivthlem2  25444  ovolgelb  25472  ovollb2lem  25480  ovolunlem1a  25488  ovolunlem1  25489  ovolfiniun  25493  ovoliunlem1  25494  ovoliunlem2  25495  ovolshftlem1  25501  ovolscalem1  25505  ovolicopnf  25516  ismbl2  25519  nulmbl2  25528  unmbl  25529  voliunlem2  25543  ioombl1lem2  25551  ioombl1lem4  25553  ioombl1  25554  ioorcl2  25564  uniioombllem1  25573  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  uniioombl  25581  opnmbllem  25593  volcn  25598  itg1addlem4  25691  mbfi1fseqlem4  25710  mbfi1fseqlem6  25712  itg2splitlem  25740  itg2split  25741  itg2monolem3  25744  itg2addlem  25750  ibladdlem  25812  itgaddlem1  25815  itgaddlem2  25816  iblabslem  25820  iblabs  25821  dvferm1lem  25976  dvferm2lem  25978  dvlip2  25987  lhop1lem  26005  lhop1  26006  lhop  26008  dvcnvrelem1  26009  dvcnvrelem2  26010  dvcnvre  26011  dvcvx  26012  dvfsumlem3  26020  dvfsumlem4  26021  dvfsum2  26026  ftc1lem4  26031  coemullem  26240  ulmbdd  26388  ulmcn  26389  ulmdvlem1  26390  radcnvle  26410  pserdvlem1  26417  pserdv  26419  abelthlem7  26428  pilem2  26442  pilem3  26443  cosordlem  26519  abslogle  26607  logccv  26652  cxpaddle  26741  ang180lem2  26799  heron  26827  atanlogaddlem  26902  atans2  26920  cxp2limlem  26964  scvxcvx  26974  jensenlem2  26976  amgmlem  26978  logdiflbnd  26983  harmonicbnd4  26999  fsumharmonic  27000  lgamgulmlem3  27019  lgamgulmlem4  27020  lgamgulmlem5  27021  lgamgulmlem6  27022  lgambdd  27025  lgamucov  27026  regamcl  27049  ftalem5  27065  efnnfsumcl  27091  efchtdvds  27147  chtublem  27199  chtub  27200  logfaclbnd  27210  perfectlem2  27218  bposlem7  27278  bposlem9  27280  lgsdirprm  27319  gausslemma2dlem1a  27353  2sqlem8  27414  chpchtlim  27467  vmadivsumb  27471  rplogsumlem1  27472  dchrisumlem2  27478  dchrvmasumlem2  27486  dchrvmasumiflem1  27489  dchrisum0re  27501  dchrisum0lem1b  27503  mulog2sumlem1  27522  mulog2sumlem2  27523  logsqvma2  27531  log2sumbnd  27532  selberglem2  27534  selbergb  27537  selberg2b  27540  chpdifbndlem1  27541  chpdifbndlem2  27542  selberg3lem2  27546  selberg3  27547  selberg4lem1  27548  selberg4  27549  pntrsumbnd2  27555  selberg3r  27557  selberg34r  27559  pntsf  27561  pntrlog2bndlem1  27565  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntrlog2bndlem6  27571  pntrlog2bnd  27572  pntpbnd1a  27573  pntpbnd2  27575  pntibndlem2a  27578  pntibndlem2  27579  pntibndlem3  27580  pntlemg  27586  pntlemr  27590  pntlemk  27594  pntlemo  27595  pntlem3  27597  abvcxp  27603  padicabv  27618  ostth2lem2  27622  ostth3  27626  brbtwn2  28999  axsegconlem8  29018  axsegconlem10  29020  axpaschlem  29034  axpasch  29035  axeuclidlem  29056  axcontlem2  29059  crctcshwlkn0lem3  29905  crctcshwlkn0lem5  29907  vacn  30790  smcnlem  30793  ubthlem2  30967  minvecolem2  30971  minvecolem3  30972  minvecolem4  30976  minvecolem5  30977  nmoptrii  32190  hstle  32326  staddi  32342  stadd3i  32344  lt2addrd  32849  nndiffz1  32885  nexple  32943  wrdt2ind  33039  cshwrnid  33047  fsumrp0cl  33107  pmtrto1cl  33187  fzto1st  33191  psgnfzto1st  33193  constrresqrtcl  33968  cos9thpiminplylem1  33973  1smat1  33995  sqsscirc1  34099  cnre2csqlem  34101  tpr2rico  34103  dya2iocress  34465  dya2iocbrsiga  34466  dya2icobrsiga  34467  dya2icoseg  34468  dya2iocucvr  34475  sxbrsigalem2  34477  omssubaddlem  34490  fibp1  34592  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemsgt1  34702  ballotlemsel1i  34704  plymulx0  34738  breprexplemc  34823  breprexp  34824  logdivsqrle  34841  resconn  35481  faclim  35981  dnizphlfeqhlf  36789  dnibndlem4  36794  dnibndlem6  36796  dnibndlem8  36798  dnibndlem9  36799  dnibndlem10  36800  dnibndlem11  36801  dnibndlem13  36803  dnibnd  36804  knoppcnlem4  36809  unblimceq0lem  36819  unblimceq0  36820  unbdqndv2lem1  36822  poimirlem29  38023  heicant  38029  opnmbllem0  38030  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  mbfposadd  38041  itg2addnclem  38045  itg2addnclem3  38047  itg2addnc  38048  itg2gt0cn  38049  ibladdnclem  38050  itgaddnclem1  38052  itgaddnclem2  38053  iblabsnclem  38057  iblabsnc  38058  iblmulc2nc  38059  ftc1cnnclem  38065  ftc1anclem4  38070  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  areacirclem5  38086  mettrifi  38131  isbnd3  38158  ssbnd  38162  cntotbnd  38170  heibor1lem  38183  bfplem2  38197  rrnequiv  38209  iccbnd  38214  lcmineqlem18  42538  lcmineqlem20  42540  aks4d1p1p3  42561  aks4d1p1p2  42562  aks4d1p1p4  42563  aks4d1p1p6  42565  aks4d1p1p7  42566  aks4d1p1p5  42567  aks4d1p1  42568  posbezout  42592  aks6d1c1  42608  aks6d1c2  42622  2np3bcnp1  42636  2ap1caineq  42637  sticksstones6  42643  sticksstones7  42644  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  sticksstones22  42660  bcle2d  42671  aks6d1c7lem1  42672  readdridaddlidd  42748  resubeulem1  42859  resubeulem2  42860  resubeu  42861  readdsub  42868  reladdrsub  42869  resubidaddlidlem  42878  renegid2  42898  sn-it0e0  42900  redivdird  42946  sn-0tie0  42948  sn-addlt0d  42955  sn-addgt0d  42956  cnreeu  42987  dffltz  43091  fltnltalem  43119  fltnlta  43120  3cubeslem1  43140  pellexlem2  43282  pell1qrge1  43322  pell14qrgapw  43328  pellqrexplicit  43329  pellqrex  43331  pellfundge  43334  pellfundgt1  43335  rmspecfund  43361  rmxycomplete  43369  ltrmynn0  43400  jm2.24nn  43411  jm2.24  43415  fzmaxdif  43433  jm2.26lem3  43453  jm3.1lem2  43470  areaquad  43668  sqrtcvallem4  44090  sqrtcvallem5  44091  sqrtcval  44092  imo72b2lem0  44616  hashnzfzclim  44773  binomcxplemnotnn0  44807  zltlesub  45740  lt3addmuld  45756  absnpncan2d  45757  fperiodmullem  45758  lt4addmuld  45761  absnpncan3d  45762  supxrgelem  45789  supxrge  45790  ltadd12dd  45795  xralrple2  45806  infxr  45818  infleinflem2  45822  xralrple4  45824  xralrple3  45825  xrralrecnnle  45834  eliooshift  45958  iccshift  45970  iooshift  45974  iooiinicc  45994  iooiinioc  46008  fsumnncl  46024  climinf  46058  climsuselem1  46059  sumnnodd  46082  lptre2pt  46090  addlimc  46098  0ellimcdiv  46099  limclner  46101  climleltrp  46126  liminfltlem  46254  fperdvper  46369  dvdivbd  46373  dvbdfbdioolem2  46379  dvbdfbdioo  46380  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvxpaek  46390  dvnmul  46393  iblsplit  46416  iblspltprt  46423  itgspltprt  46429  itgiccshift  46430  itgperiod  46431  itgsbtaddcnst  46432  stoweidlem1  46451  stoweidlem11  46461  stoweidlem13  46463  stoweidlem14  46464  stoweidlem20  46470  stoweidlem21  46471  stoweidlem26  46476  stoweidlem44  46494  stoweidlem60  46510  wallispilem3  46517  wallispilem4  46518  wallispilem5  46519  wallispi  46520  wallispi2lem1  46521  wallispi2lem2  46522  stirlinglem1  46524  stirlinglem3  46526  stirlinglem5  46528  stirlinglem6  46529  stirlinglem7  46530  stirlinglem10  46533  stirlinglem11  46534  stirlinglem12  46535  dirker2re  46542  dirkerval2  46544  dirkerre  46545  dirkerper  46546  dirkertrigeqlem1  46548  dirkertrigeqlem2  46549  dirkeritg  46552  dirkercncflem1  46553  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem4  46561  fourierdlem5  46562  fourierdlem6  46563  fourierdlem7  46564  fourierdlem9  46566  fourierdlem10  46567  fourierdlem18  46575  fourierdlem19  46576  fourierdlem20  46577  fourierdlem26  46583  fourierdlem28  46585  fourierdlem30  46587  fourierdlem35  46592  fourierdlem40  46597  fourierdlem41  46598  fourierdlem42  46599  fourierdlem47  46603  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem51  46607  fourierdlem53  46609  fourierdlem57  46613  fourierdlem59  46615  fourierdlem60  46616  fourierdlem61  46617  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem66  46622  fourierdlem68  46624  fourierdlem71  46627  fourierdlem72  46628  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem78  46634  fourierdlem79  46635  fourierdlem80  46636  fourierdlem81  46637  fourierdlem82  46638  fourierdlem83  46639  fourierdlem84  46640  fourierdlem87  46643  fourierdlem88  46644  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem93  46649  fourierdlem94  46650  fourierdlem95  46651  fourierdlem97  46653  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  qndenserrnbllem  46744  ioorrnopnlem  46754  ioorrnopnxrlem  46756  sge0xaddlem1  46883  sge0xaddlem2  46884  omeiunltfirp  46969  carageniuncllem2  46972  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hoiqssbllem1  47072  hoiqssbllem2  47073  hoiqssbllem3  47074  hspmbllem2  47077  hspmbllem3  47078  ovolval5lem1  47102  iinhoiicclem  47123  iinhoiicc  47124  iunhoiioolem  47125  iccvonmbllem  47128  vonioolem1  47130  vonioolem2  47131  vonicclem1  47133  vonicclem2  47134  preimaleiinlt  47171  salpreimaltle  47176  smfaddlem1  47213  smfadd  47215  smflimlem3  47223  smflimlem4  47224  smflimlem6  47226  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243  ormkglobd  47327  zm1nn  47772  requad01  48119  requad1  48120  requad2  48121  perfectALTVlem2  48220  nnsum4primesevenALTV  48299  bgoldbtbndlem2  48304  gpgvtxedg0  48561  gpgvtxedg1  48562  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx13starlem2  48570  dignn0flhalflem1  49113  affinecomb1  49200  resum2sqcl  49204  2sphere  49247  line2  49250  itsclc0lem1  49254  itscnhlc0yqe  49257  itsclquadb  49274  2itscp  49279  itscnhlinecirc02plem1  49280  itscnhlinecirc02plem3  49282  itscnhlinecirc02p  49283  inlinecirc02plem  49284  amgmwlem  50299