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

Theorem readdcld 9612
Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
readdcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
readdcld  |-  ( ph  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 readdcl 9564 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823  (class class class)co 6270   RRcr 9480    + caddc 9484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9542
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  ltadd2  9677  readdcan  9743  addid1  9749  leadd1  10016  le2add  10030  lesub2  10043  cju  10527  rpnnen1lem5  11213  xralrple  11407  xov1plusxeqvd  11669  elincfzoext  11855  fladdz  11940  flhalf  11944  fldiv  11969  modaddmodup  12032  modaddmodlo  12033  discr1  12284  discr  12285  2cshw  12772  remim  13032  remullem  13043  sqrlem7  13164  absrele  13223  abstri  13245  abs3lem  13253  amgm2  13284  mulcn2  13500  o1add  13518  o1sub  13520  lo1add  13531  caucvgrlem  13577  iseraltlem2  13587  iseraltlem3  13588  fsumabs  13697  o1fsum  13709  climcndslem2  13744  tanhlt1  13977  eirrlem  14019  ruclem1  14048  ruclem2  14049  ruclem3  14050  bitscmp  14172  sadcaddlem  14191  sadasslem  14204  smuval2  14216  prmreclem4  14521  4sqlem5  14544  4sqlem6  14545  4sqlem12  14558  4sqlem15  14561  4sqlem16  14562  2expltfac  14661  cshwshashlem2  14665  chfacfscmul0  19526  chfacfscmulgsum  19528  chfacfpmmul0  19530  chfacfpmmulgsum  19532  prdsxmetlem  21037  xblss2ps  21070  metustexhalfOLD  21232  metustexhalf  21233  nrmmetd  21261  ngptgp  21316  nlmvscnlem2  21360  nlmvscnlem1  21361  nmotri  21412  nghmplusg  21413  blcvx  21469  iccntr  21492  icccmplem2  21494  reconnlem2  21498  metdcnlem  21507  metnrmlem3  21531  cnllycmp  21622  lebnumii  21632  tchcphlem1  21844  ipcnlem2  21850  ipcnlem1  21851  csbren  21992  trirn  21993  minveclem2  22007  minveclem3b  22009  minveclem4  22013  ivthlem2  22030  ovolgelb  22057  ovollb2lem  22065  ovolunlem1a  22073  ovolunlem1  22074  ovolfiniun  22078  ovoliunlem1  22079  ovoliunlem2  22080  ovolshftlem1  22086  ovolscalem1  22090  ovolicopnf  22101  ismbl2  22104  nulmbl2  22113  unmbl  22114  voliunlem2  22127  ioombl1lem2  22135  ioombl1lem4  22137  ioombl1  22138  ioorcl2  22147  uniioombllem1  22156  uniioombllem3  22160  uniioombllem4  22161  uniioombllem5  22162  uniioombl  22164  opnmbllem  22176  volcn  22181  itg1addlem4  22272  mbfi1fseqlem4  22291  mbfi1fseqlem6  22293  itg2splitlem  22321  itg2split  22322  itg2monolem3  22325  itg2addlem  22331  ibladdlem  22392  itgaddlem1  22395  itgaddlem2  22396  iblabslem  22400  iblabs  22401  dvferm1lem  22551  dvferm2lem  22553  dvlip2  22562  lhop1lem  22580  lhop1  22581  lhop  22583  dvcnvrelem1  22584  dvcnvrelem2  22585  dvcnvre  22586  dvcvx  22587  dvfsumlem3  22595  dvfsumlem4  22596  dvfsum2  22601  ftc1lem4  22606  coemullem  22813  ulmbdd  22959  ulmcn  22960  ulmdvlem1  22961  radcnvle  22981  pserdvlem1  22988  pserdv  22990  abelthlem7  22999  pilem2  23013  pilem3  23014  cosordlem  23084  abslogle  23171  logccv  23212  cxpaddle  23294  ang180lem2  23341  heron  23366  atanlogaddlem  23441  atans2  23459  cxp2limlem  23503  scvxcvx  23513  jensenlem2  23515  amgmlem  23517  logdiflbnd  23522  harmonicbnd4  23538  fsumharmonic  23539  ftalem5  23548  efnnfsumcl  23574  efchtdvds  23631  chtublem  23684  chtub  23685  logfaclbnd  23695  perfectlem2  23703  bcmono  23750  bposlem7  23763  bposlem9  23765  lgsdirprm  23802  2sqlem8  23845  chpchtlim  23862  vmadivsumb  23866  rplogsumlem1  23867  dchrisumlem2  23873  dchrvmasumlem2  23881  dchrvmasumiflem1  23884  dchrisum0re  23896  dchrisum0lem1b  23898  mulog2sumlem1  23917  mulog2sumlem2  23918  logsqvma2  23926  log2sumbnd  23927  selberglem2  23929  selbergb  23932  selberg2b  23935  chpdifbndlem1  23936  chpdifbndlem2  23937  selberg3lem2  23941  selberg3  23942  selberg4lem1  23943  selberg4  23944  pntrsumbnd2  23950  selberg3r  23952  selberg34r  23954  pntsf  23956  pntrlog2bndlem1  23960  pntrlog2bndlem2  23961  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntrlog2bndlem6  23966  pntrlog2bnd  23967  pntpbnd1a  23968  pntpbnd2  23970  pntibndlem2a  23973  pntibndlem2  23974  pntibndlem3  23975  pntlemg  23981  pntlemr  23985  pntlemk  23989  pntlemo  23990  pntlem3  23992  abvcxp  23998  padicabv  24013  ostth2lem2  24017  ostth3  24021  brbtwn2  24410  axsegconlem8  24429  axsegconlem10  24431  axpaschlem  24445  axpasch  24446  axeuclidlem  24467  axcontlem2  24470  vacn  25802  smcnlem  25805  ubthlem2  25985  minvecolem2  25989  minvecolem3  25990  minvecolem4  25994  minvecolem5  25995  nmoptrii  27211  hstle  27347  staddi  27363  stadd3i  27365  lt2addrd  27794  nndiffz1  27830  bhmafibid1  27866  fsumrp0cl  27919  sqsscirc1  28125  cnre2csqlem  28127  tpr2rico  28129  nexple  28239  dya2iocress  28482  dya2iocbrsiga  28483  dya2icobrsiga  28484  dya2icoseg  28485  dya2iocucvr  28492  sxbrsigalem2  28494  omssubaddlem  28507  fibp1  28604  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemsgt1  28713  ballotlemsel1i  28715  eluzmn  28755  plymulx0  28768  lgamgulmlem3  28837  lgamgulmlem4  28838  lgamgulmlem5  28839  lgamgulmlem6  28840  lgambdd  28843  lgamucov  28844  regamcl  28867  rescon  28955  faclim  29412  supaddc  30281  supadd  30282  heicant  30289  opnmbllem0  30290  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  mbfposadd  30302  itg2addnclem  30306  itg2addnclem3  30308  itg2addnc  30309  itg2gt0cn  30310  ibladdnclem  30311  itgaddnclem1  30313  itgaddnclem2  30314  iblabsnclem  30318  iblabsnc  30319  iblmulc2nc  30320  ftc1cnnclem  30328  ftc1anclem4  30333  ftc1anclem7  30336  ftc1anclem8  30337  ftc1anc  30338  areacirclem5  30351  mettrifi  30490  isbnd3  30520  ssbnd  30524  cntotbnd  30532  heibor1lem  30545  bfplem2  30559  rrnequiv  30571  iccbnd  30576  pellexlem2  31005  pell1qrge1  31045  pell14qrgapw  31051  pellqrexplicit  31052  pellqrex  31054  pellfundge  31057  pellfundgt1  31058  rmspecfund  31084  rmxycomplete  31092  ltrmynn0  31125  jm2.24nn  31136  jm2.24  31140  fzmaxdif  31158  jm2.26lem3  31182  jm3.1lem2  31199  areaquad  31425  hashnzfzclim  31468  binomcxplemnotnn0  31502  zltlesub  31708  lt3addmuld  31740  absnpncan2d  31741  fperiodmullem  31742  lt4addmuld  31745  absnpncan3d  31746  leadd12dd  31760  eliooshift  31780  iccshift  31797  iooshift  31801  fsumnncl  31811  climinf  31851  climsuselem1  31852  sumnnodd  31875  lptre2pt  31885  addlimc  31893  0ellimcdiv  31894  limclner  31896  fperdvper  31954  dvdivbd  31959  dvbdfbdioolem2  31965  dvbdfbdioo  31966  ioodvbdlimc1lem1  31967  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvxpaek  31976  dvnmul  31979  iblsplit  32004  iblspltprt  32011  itgspltprt  32017  itgiccshift  32018  itgperiod  32019  itgsbtaddcnst  32020  stoweidlem1  32022  stoweidlem11  32032  stoweidlem13  32034  stoweidlem14  32035  stoweidlem20  32041  stoweidlem21  32042  stoweidlem26  32047  stoweidlem44  32065  stoweidlem60  32081  wallispilem3  32088  wallispilem4  32089  wallispilem5  32090  wallispi  32091  wallispi2lem1  32092  wallispi2lem2  32093  stirlinglem1  32095  stirlinglem3  32097  stirlinglem5  32099  stirlinglem6  32100  stirlinglem7  32101  stirlinglem10  32104  stirlinglem11  32105  stirlinglem12  32106  dirker2re  32113  dirkerval2  32115  dirkerre  32116  dirkerper  32117  dirkertrigeqlem1  32119  dirkertrigeqlem2  32120  dirkeritg  32123  dirkercncflem1  32124  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem4  32132  fourierdlem5  32133  fourierdlem6  32134  fourierdlem7  32135  fourierdlem9  32137  fourierdlem10  32138  fourierdlem18  32146  fourierdlem19  32147  fourierdlem20  32148  fourierdlem26  32154  fourierdlem28  32156  fourierdlem30  32158  fourierdlem35  32163  fourierdlem40  32168  fourierdlem41  32169  fourierdlem42  32170  fourierdlem47  32175  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem53  32181  fourierdlem57  32185  fourierdlem59  32187  fourierdlem60  32188  fourierdlem61  32189  fourierdlem63  32191  fourierdlem64  32192  fourierdlem65  32193  fourierdlem66  32194  fourierdlem68  32196  fourierdlem71  32199  fourierdlem72  32200  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem78  32206  fourierdlem79  32207  fourierdlem80  32208  fourierdlem81  32209  fourierdlem82  32210  fourierdlem83  32211  fourierdlem84  32212  fourierdlem87  32215  fourierdlem88  32216  fourierdlem89  32217  fourierdlem90  32218  fourierdlem91  32219  fourierdlem92  32220  fourierdlem93  32221  fourierdlem94  32222  fourierdlem95  32223  fourierdlem97  32225  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  fourierdlem112  32240  fourierdlem113  32241  sqwvfoura  32250  sqwvfourb  32251  fouriersw  32253  zm1nn  32699  dignn0flhalflem1  33490  imo72b2lem0  38434
  Copyright terms: Public domain W3C validator