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

Theorem remulcld 8950
Description: Closure law for multiplication 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
remulcld  |-  ( ph  ->  ( A  x.  B
)  e.  RR )

Proof of Theorem remulcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 remulcl 8909 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710  (class class class)co 5942   RRcr 8823    x. cmul 8829
This theorem is referenced by:  mulge0  9378  msqge0  9382  redivcl  9566  prodgt0  9688  prodge0  9690  ltmul1a  9692  ltmul1  9693  ltmuldiv  9713  lt2msq1  9726  lt2msq  9727  le2msq  9743  msq11  9744  supmul1  9806  supmullem2  9808  supmul  9809  qbtwnre  10615  xmulneg1  10678  xmulf  10681  lincmb01cmp  10866  iccf1o  10867  flmulnn0  11041  flhalf  11043  modcl  11065  mod0  11067  modge0  11069  modmulnn  11077  moddi  11096  modsubdir  11097  modirr  11098  bernneq  11317  bernneq3  11319  expnbnd  11320  expmulnbnd  11323  discr1  11327  discr  11328  faclbnd  11393  faclbnd6  11402  remullem  11703  sqrlem7  11824  sqrmul  11835  abstri  11904  sqreulem  11933  mulcn2  12159  reccn2  12160  o1rlimmul  12182  lo1mul  12191  iseraltlem2  12246  iseraltlem3  12247  iseralt  12248  o1fsum  12362  cvgcmpce  12367  climcndslem1  12399  climcndslem2  12400  climcnds  12401  geomulcvg  12423  cvgrat  12430  mertenslem1  12431  eftlub  12480  sin02gt0  12563  eirrlem  12573  bitsp1o  12715  isprm5  12882  prmreclem3  13056  prmreclem4  13057  prmreclem5  13058  2expltfac  13196  metss2lem  18153  nlmvscnlem2  18292  nrginvrcnlem  18297  nmoco  18342  nmotri  18344  nghmcn  18350  icopnfhmeo  18539  nmoleub2lem3  18694  ipcau2  18762  tchcphlem1  18763  ipcnlem2  18769  pjthlem1  18899  opnmbllem  19054  vitalilem4  19064  itg1val2  19137  itg1cl  19138  itg1ge0  19139  itg1addlem4  19152  itg1mulc  19157  itg1ge0a  19164  itg1climres  19167  mbfi1fseqlem1  19168  mbfi1fseqlem3  19170  mbfi1fseqlem4  19171  mbfi1fseqlem5  19172  mbfi1fseqlem6  19173  itg2const2  19194  itg2mulclem  19199  itg2mulc  19200  itg2monolem1  19203  itg2monolem3  19205  itg2cnlem2  19215  iblconst  19270  iblmulc2  19283  itgmulc2lem1  19284  itgmulc2lem2  19285  bddmulibl  19291  dveflem  19424  cmvth  19436  dvlip  19438  dvlipcn  19439  dvivthlem1  19453  lhop1lem  19458  dvcvx  19465  dvfsumlem2  19472  dvfsumlem3  19473  dvfsumlem4  19474  dvfsum2  19479  ftc1lem4  19484  plyeq0lem  19690  aalioulem3  19812  aalioulem4  19813  aaliou3lem9  19828  ulmdvlem1  19877  itgulm  19885  radcnvlem1  19890  radcnvlem2  19891  dvradcnv  19898  abelthlem2  19909  abelthlem7  19915  tangtx  19974  tanregt0  20002  logdivlti  20076  logcnlem3  20096  logcnlem4  20097  logccv  20115  recxpcl  20127  cxpmul  20140  cxplt  20146  cxple2  20149  abscxpbnd  20198  lawcoslem1  20218  atans2  20332  efrlim  20369  o1cxp  20374  scvxcvx  20385  jensenlem2  20387  amgmlem  20389  fsumharmonic  20411  ftalem1  20416  ftalem2  20417  ftalem5  20420  basellem3  20426  basellem8  20431  chpub  20565  logfacubnd  20566  logfaclbnd  20567  logfacbnd3  20568  logexprlim  20570  perfectlem2  20575  bclbnd  20625  efexple  20626  bposlem1  20629  bposlem2  20630  bposlem6  20634  bposlem9  20637  lgsdilem  20667  lgseisenlem4  20697  lgseisen  20698  lgsquadlem1  20699  lgsquadlem2  20700  chebbnd1lem1  20724  chebbnd1lem3  20726  chtppilimlem1  20728  chpchtlim  20734  vmadivsum  20737  rplogsumlem1  20739  rpvmasumlem  20742  dchrisumlem2  20745  dchrisumlem3  20746  dchrmusum2  20749  dchrvmasumlem2  20753  dchrvmasumiflem1  20756  dchrisum0re  20768  dchrisum0lem1  20771  dirith2  20783  mulogsumlem  20786  mulogsum  20787  mulog2sumlem2  20790  vmalogdivsum2  20793  vmalogdivsum  20794  2vmadivsumlem  20795  logsqvma  20797  logsqvma2  20798  log2sumbnd  20799  selberglem2  20801  selberg  20803  selbergb  20804  selberg2lem  20805  selberg2b  20807  chpdifbndlem1  20808  chpdifbndlem2  20809  selberg3lem1  20812  selberg3lem2  20813  selberg3  20814  selberg4lem1  20815  selberg4  20816  pntrsumbnd2  20822  selberg3r  20824  selberg4r  20825  selberg34r  20826  pntsf  20828  pntsval2  20831  pntrlog2bndlem1  20832  pntrlog2bndlem2  20833  pntrlog2bndlem3  20834  pntrlog2bndlem4  20835  pntrlog2bndlem5  20836  pntrlog2bndlem6  20838  pntrlog2bnd  20839  pntpbnd1a  20840  pntpbnd1  20841  pntpbnd2  20842  pntibndlem2a  20845  pntibndlem2  20846  pntlemb  20852  pntlemr  20857  pntlemj  20858  pntlemf  20860  pntlemk  20861  pntlemo  20862  pntlem3  20864  ostth2lem1  20873  ostth2lem2  20889  ostth2lem3  20890  ostth2lem4  20891  ostth3  20893  smcnlem  21378  ubthlem2  21558  htthlem  21605  pjhthlem1  22078  cnlnadjlem7  22761  nmopcoadji  22789  branmfn  22793  leopnmid  22826  rmulccn  23470  xrge0iifhom  23479  dya2icoseg  23891  lgamgulmlem2  24063  lgamgulmlem3  24064  lgamgulmlem4  24065  lgamgulmlem5  24066  lgamgulmlem6  24067  relgamcl  24095  rescon  24181  brbtwn2  25092  colinearalglem4  25096  axsegconlem8  25111  axsegconlem9  25112  axsegconlem10  25113  ax5seglem3  25118  axpaschlem  25127  axpasch  25128  axeuclidlem  25149  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  iblmulc2nc  25505  itgmulc2nclem1  25506  bddiblnc  25510  ftc1cnnclem  25513  areacirclem5  25521  csbrn  25786  trirn  25787  geomcau  25799  bfplem1  25869  bfplem2  25870  bfp  25871  rrnequiv  25882  rrntotbnd  25883  irrapxlem1  26230  irrapxlem2  26231  irrapxlem3  26232  irrapxlem4  26233  irrapxlem5  26234  pellexlem2  26238  pellexlem6  26242  pell14qrgt0  26267  pell1qrge1  26278  pell1qrgaplem  26281  pellqrexplicit  26285  pellqrex  26287  rmxycomplete  26325  rmxypos  26357  ltrmynn0  26358  ltrmxnn0  26359  jm2.24nn  26369  jm2.17a  26370  jm2.17b  26371  jm2.17c  26372  jm2.27c  26423  jm3.1lem2  26434  stoweidlem30  27102  wallispilem4  27140  wallispilem5  27141  wallispi  27142  wallispi2lem1  27143  wallispi2  27145  stirlinglem1  27146  stirlinglem3  27148  stirlinglem5  27150  stirlinglem6  27151  stirlinglem7  27152  stirlinglem10  27155  stirlinglem11  27156  stirlinglem12  27157  stirlinglem15  27160  stirlingr  27162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 8887
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator