MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  readdcld Structured version   Visualization version   GIF version

Theorem readdcld 10664
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
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 readdcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 readdcl 10614 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  (class class class)co 7146  cr 10530   + caddc 10534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10592
This theorem depends on definitions:  df-bi 210  df-an 400
This theorem is referenced by:  ltadd2  10738  readdcan  10808  addid1  10814  leadd1  11102  le2add  11116  lesub2  11129  lesub3d  11252  supaddc  11602  supadd  11603  cju  11628  nnne0  11666  div4p1lem1div2  11887  difgtsumgt  11945  eluzmn  12245  rpnnen1lem5  12375  addlelt  12498  xralrple  12593  xov1plusxeqvd  12883  zltaddlt1le  12890  elincfzoext  13097  fladdz  13197  2tnp1ge0ge0  13201  flhalf  13202  fldiv  13230  modaddmodup  13304  modaddmodlo  13305  addmodlteq  13316  discr1  13603  discr  13604  ccatalpha  13945  2cshw  14173  remim  14474  remullem  14485  sqrlem7  14606  absrele  14666  abstri  14688  abs3lem  14696  amgm2  14727  bhmafibid1  14823  mulcn2  14950  o1add  14968  o1sub  14970  lo1add  14981  caucvgrlem  15027  iseraltlem2  15037  iseraltlem3  15038  fsumabs  15154  o1fsum  15166  climcndslem2  15203  tanhlt1  15511  eirrlem  15555  ruclem1  15582  ruclem2  15583  ruclem3  15584  ltoddhalfle  15708  bitscmp  15783  sadcaddlem  15802  sadasslem  15815  smuval2  15827  iserodd  16168  prmreclem4  16251  4sqlem5  16274  4sqlem6  16275  4sqlem12  16288  4sqlem15  16291  4sqlem16  16292  prmgaplem7  16389  prmgaplem8  16390  2expltfac  16424  cshwshashlem2  16428  chfacfscmul0  21461  chfacfscmulgsum  21463  chfacfpmmul0  21465  chfacfpmmulgsum  21467  prdsxmetlem  22973  xblss2ps  23006  metustexhalf  23161  nrmmetd  23179  ngptgp  23240  nlmvscnlem2  23289  nlmvscnlem1  23290  nmotri  23343  nghmplusg  23344  blcvx  23401  iccntr  23424  icccmplem2  23426  reconnlem2  23430  metdcnlem  23439  metnrmlem3  23464  cnllycmp  23559  lebnumii  23569  tcphcphlem1  23837  ipcnlem2  23846  ipcnlem1  23847  csbren  24001  trirn  24002  minveclem2  24028  minveclem3b  24030  minveclem4  24034  ivthlem2  24054  ovolgelb  24082  ovollb2lem  24090  ovolunlem1a  24098  ovolunlem1  24099  ovolfiniun  24103  ovoliunlem1  24104  ovoliunlem2  24105  ovolshftlem1  24111  ovolscalem1  24115  ovolicopnf  24126  ismbl2  24129  nulmbl2  24138  unmbl  24139  voliunlem2  24153  ioombl1lem2  24161  ioombl1lem4  24163  ioombl1  24164  ioorcl2  24174  uniioombllem1  24183  uniioombllem3  24187  uniioombllem4  24188  uniioombllem5  24189  uniioombl  24191  opnmbllem  24203  volcn  24208  itg1addlem4  24301  mbfi1fseqlem4  24320  mbfi1fseqlem6  24322  itg2splitlem  24350  itg2split  24351  itg2monolem3  24354  itg2addlem  24360  ibladdlem  24421  itgaddlem1  24424  itgaddlem2  24425  iblabslem  24429  iblabs  24430  dvferm1lem  24585  dvferm2lem  24587  dvlip2  24596  lhop1lem  24614  lhop1  24615  lhop  24617  dvcnvrelem1  24618  dvcnvrelem2  24619  dvcnvre  24620  dvcvx  24621  dvfsumlem3  24629  dvfsumlem4  24630  dvfsum2  24635  ftc1lem4  24640  coemullem  24845  ulmbdd  24991  ulmcn  24992  ulmdvlem1  24993  radcnvle  25013  pserdvlem1  25020  pserdv  25022  abelthlem7  25031  pilem2  25045  pilem3  25046  cosordlem  25120  abslogle  25207  logccv  25252  cxpaddle  25339  ang180lem2  25394  heron  25422  atanlogaddlem  25497  atans2  25515  cxp2limlem  25559  scvxcvx  25569  jensenlem2  25571  amgmlem  25573  logdiflbnd  25578  harmonicbnd4  25594  fsumharmonic  25595  lgamgulmlem3  25614  lgamgulmlem4  25615  lgamgulmlem5  25616  lgamgulmlem6  25617  lgambdd  25620  lgamucov  25621  regamcl  25644  ftalem5  25660  efnnfsumcl  25686  efchtdvds  25742  chtublem  25793  chtub  25794  logfaclbnd  25804  perfectlem2  25812  bposlem7  25872  bposlem9  25874  lgsdirprm  25913  gausslemma2dlem1a  25947  2sqlem8  26008  chpchtlim  26061  vmadivsumb  26065  rplogsumlem1  26066  dchrisumlem2  26072  dchrvmasumlem2  26080  dchrvmasumiflem1  26083  dchrisum0re  26095  dchrisum0lem1b  26097  mulog2sumlem1  26116  mulog2sumlem2  26117  logsqvma2  26125  log2sumbnd  26126  selberglem2  26128  selbergb  26131  selberg2b  26134  chpdifbndlem1  26135  chpdifbndlem2  26136  selberg3lem2  26140  selberg3  26141  selberg4lem1  26142  selberg4  26143  pntrsumbnd2  26149  selberg3r  26151  selberg34r  26153  pntsf  26155  pntrlog2bndlem1  26159  pntrlog2bndlem2  26160  pntrlog2bndlem4  26162  pntrlog2bndlem5  26163  pntrlog2bndlem6  26165  pntrlog2bnd  26166  pntpbnd1a  26167  pntpbnd2  26169  pntibndlem2a  26172  pntibndlem2  26173  pntibndlem3  26174  pntlemg  26180  pntlemr  26184  pntlemk  26188  pntlemo  26189  pntlem3  26191  abvcxp  26197  padicabv  26212  ostth2lem2  26216  ostth3  26220  brbtwn2  26697  axsegconlem8  26716  axsegconlem10  26718  axpaschlem  26732  axpasch  26733  axeuclidlem  26754  axcontlem2  26757  crctcshwlkn0lem3  27596  crctcshwlkn0lem5  27598  vacn  28475  smcnlem  28478  ubthlem2  28652  minvecolem2  28656  minvecolem3  28657  minvecolem4  28661  minvecolem5  28662  nmoptrii  29875  hstle  30011  staddi  30027  stadd3i  30029  lt2addrd  30481  nndiffz1  30515  wrdt2ind  30633  cshwrnid  30641  fsumrp0cl  30709  pmtrto1cl  30768  fzto1st  30772  psgnfzto1st  30774  1smat1  31099  sqsscirc1  31178  cnre2csqlem  31180  tpr2rico  31182  nexple  31295  dya2iocress  31559  dya2iocbrsiga  31560  dya2icobrsiga  31561  dya2icoseg  31562  dya2iocucvr  31569  sxbrsigalem2  31571  omssubaddlem  31584  fibp1  31686  ballotlemfc0  31777  ballotlemfcc  31778  ballotlemsgt1  31795  ballotlemsel1i  31797  plymulx0  31844  breprexplemc  31930  breprexp  31931  logdivsqrle  31948  resconn  32520  faclim  33005  dnizphlfeqhlf  33842  dnibndlem4  33847  dnibndlem6  33849  dnibndlem8  33851  dnibndlem9  33852  dnibndlem10  33853  dnibndlem11  33854  dnibndlem13  33856  dnibnd  33857  knoppcnlem4  33862  unblimceq0lem  33872  unblimceq0  33873  unbdqndv2lem1  33875  poimirlem29  34998  heicant  35004  opnmbllem0  35005  mblfinlem3  35008  mblfinlem4  35009  ismblfin  35010  mbfposadd  35016  itg2addnclem  35020  itg2addnclem3  35022  itg2addnc  35023  itg2gt0cn  35024  ibladdnclem  35025  itgaddnclem1  35027  itgaddnclem2  35028  iblabsnclem  35032  iblabsnc  35033  iblmulc2nc  35034  ftc1cnnclem  35040  ftc1anclem4  35045  ftc1anclem7  35048  ftc1anclem8  35049  ftc1anc  35050  areacirclem5  35061  mettrifi  35107  isbnd3  35134  ssbnd  35138  cntotbnd  35146  heibor1lem  35159  bfplem2  35173  rrnequiv  35185  iccbnd  35190  lcmineqlem18  39242  lcmineqlem20  39244  2xp3dxp2ge1d  39270  factwoffsmonot  39271  readdid1addid2d  39339  resubeulem1  39387  resubeulem2  39388  resubeu  39389  readdsub  39396  reladdrsub  39397  resubidaddid1lem  39406  renegid2  39425  sn-it0e0  39426  dffltz  39471  fltnltalem  39474  fltnlta  39475  3cubeslem1  39481  pellexlem2  39627  pell1qrge1  39667  pell14qrgapw  39673  pellqrexplicit  39674  pellqrex  39676  pellfundge  39679  pellfundgt1  39680  rmspecfund  39706  rmxycomplete  39714  ltrmynn0  39745  jm2.24nn  39756  jm2.24  39760  fzmaxdif  39778  jm2.26lem3  39798  jm3.1lem2  39815  areaquad  40022  sqrtcvallem4  40195  sqrtcvallem5  40196  sqrtcval  40197  imo72b2lem0  40728  hashnzfzclim  40886  binomcxplemnotnn0  40920  zltlesub  41782  lt3addmuld  41799  absnpncan2d  41800  fperiodmullem  41801  lt4addmuld  41804  absnpncan3d  41805  leadd12dd  41814  supxrgelem  41835  supxrge  41836  ltadd12dd  41841  xralrple2  41852  infxr  41865  infleinflem2  41869  xralrple4  41871  xralrple3  41872  xrralrecnnle  41883  eliooshift  42009  iccshift  42021  iooshift  42025  iooiinicc  42045  iooiinioc  42059  fsumnncl  42079  climinf  42114  climsuselem1  42115  sumnnodd  42138  lptre2pt  42148  addlimc  42156  0ellimcdiv  42157  limclner  42159  climleltrp  42184  liminfltlem  42312  fperdvper  42427  dvdivbd  42431  dvbdfbdioolem2  42437  dvbdfbdioo  42438  ioodvbdlimc1lem1  42439  ioodvbdlimc1lem2  42440  ioodvbdlimc2lem  42442  dvxpaek  42448  dvnmul  42451  iblsplit  42474  iblspltprt  42481  itgspltprt  42487  itgiccshift  42488  itgperiod  42489  itgsbtaddcnst  42490  stoweidlem1  42509  stoweidlem11  42519  stoweidlem13  42521  stoweidlem14  42522  stoweidlem20  42528  stoweidlem21  42529  stoweidlem26  42534  stoweidlem44  42552  stoweidlem60  42568  wallispilem3  42575  wallispilem4  42576  wallispilem5  42577  wallispi  42578  wallispi2lem1  42579  wallispi2lem2  42580  stirlinglem1  42582  stirlinglem3  42584  stirlinglem5  42586  stirlinglem6  42587  stirlinglem7  42588  stirlinglem10  42591  stirlinglem11  42592  stirlinglem12  42593  dirker2re  42600  dirkerval2  42602  dirkerre  42603  dirkerper  42604  dirkertrigeqlem1  42606  dirkertrigeqlem2  42607  dirkeritg  42610  dirkercncflem1  42611  dirkercncflem2  42612  dirkercncflem4  42614  fourierdlem4  42619  fourierdlem5  42620  fourierdlem6  42621  fourierdlem7  42622  fourierdlem9  42624  fourierdlem10  42625  fourierdlem18  42633  fourierdlem19  42634  fourierdlem20  42635  fourierdlem26  42641  fourierdlem28  42643  fourierdlem30  42645  fourierdlem35  42650  fourierdlem40  42655  fourierdlem41  42656  fourierdlem42  42657  fourierdlem47  42661  fourierdlem48  42662  fourierdlem49  42663  fourierdlem50  42664  fourierdlem51  42665  fourierdlem53  42667  fourierdlem57  42671  fourierdlem59  42673  fourierdlem60  42674  fourierdlem61  42675  fourierdlem63  42677  fourierdlem64  42678  fourierdlem65  42679  fourierdlem66  42680  fourierdlem68  42682  fourierdlem71  42685  fourierdlem72  42686  fourierdlem74  42688  fourierdlem75  42689  fourierdlem76  42690  fourierdlem78  42692  fourierdlem79  42693  fourierdlem80  42694  fourierdlem81  42695  fourierdlem82  42696  fourierdlem83  42697  fourierdlem84  42698  fourierdlem87  42701  fourierdlem88  42702  fourierdlem89  42703  fourierdlem90  42704  fourierdlem91  42705  fourierdlem92  42706  fourierdlem93  42707  fourierdlem94  42708  fourierdlem95  42709  fourierdlem97  42711  fourierdlem101  42715  fourierdlem103  42717  fourierdlem104  42718  fourierdlem111  42725  fourierdlem112  42726  fourierdlem113  42727  sqwvfoura  42736  sqwvfourb  42737  fouriersw  42739  qndenserrnbllem  42802  ioorrnopnlem  42812  ioorrnopnxrlem  42814  sge0xaddlem1  42938  sge0xaddlem2  42939  omeiunltfirp  43024  carageniuncllem2  43027  hoidmv1lelem1  43096  hoidmv1lelem2  43097  hoidmvlelem1  43100  hoidmvlelem2  43101  hoidmvlelem3  43102  hoidmvlelem4  43103  hoiqssbllem1  43127  hoiqssbllem2  43128  hoiqssbllem3  43129  hspmbllem2  43132  hspmbllem3  43133  ovolval5lem1  43157  iinhoiicclem  43178  iinhoiicc  43179  iunhoiioolem  43180  iccvonmbllem  43183  vonioolem1  43185  vonioolem2  43186  vonicclem1  43188  vonicclem2  43189  preimaleiinlt  43222  salpreimaltle  43226  smfaddlem1  43262  smfadd  43264  smflimlem3  43272  smflimlem4  43273  smflimlem6  43275  smfmullem1  43289  smfmullem2  43290  smfmullem3  43291  zm1nn  43725  requad01  44005  requad1  44006  requad2  44007  perfectALTVlem2  44106  nnsum4primesevenALTV  44185  bgoldbtbndlem2  44190  dignn0flhalflem1  44894  affinecomb1  44970  resum2sqcl  44974  2sphere  45017  line2  45020  itsclc0lem1  45024  itscnhlc0yqe  45027  itsclquadb  45044  2itscp  45049  itscnhlinecirc02plem1  45050  itscnhlinecirc02plem3  45052  itscnhlinecirc02p  45053  inlinecirc02plem  45054  amgmwlem  45184
  Copyright terms: Public domain W3C validator