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

Theorem remulcld 8863
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 8822 . 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 1684  (class class class)co 5858   RRcr 8736    x. cmul 8742
This theorem is referenced by:  mulge0  9291  msqge0  9295  redivcl  9479  prodgt0  9601  prodge0  9603  ltmul1a  9605  ltmul1  9606  ltmuldiv  9626  lt2msq1  9639  lt2msq  9640  le2msq  9656  msq11  9657  supmul1  9719  supmullem2  9721  supmul  9722  qbtwnre  10526  xmulneg1  10589  xmulf  10592  lincmb01cmp  10777  iccf1o  10778  flmulnn0  10952  flhalf  10954  modcl  10976  mod0  10978  modge0  10980  modmulnn  10988  moddi  11007  modsubdir  11008  modirr  11009  bernneq  11227  bernneq3  11229  expnbnd  11230  expmulnbnd  11233  discr1  11237  discr  11238  faclbnd  11303  faclbnd6  11312  remullem  11613  sqrlem7  11734  sqrmul  11745  abstri  11814  sqreulem  11843  mulcn2  12069  reccn2  12070  o1rlimmul  12092  lo1mul  12101  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  o1fsum  12271  cvgcmpce  12276  climcndslem1  12308  climcndslem2  12309  climcnds  12310  geomulcvg  12332  cvgrat  12339  mertenslem1  12340  eftlub  12389  sin02gt0  12472  eirrlem  12482  bitsp1o  12624  isprm5  12791  prmreclem3  12965  prmreclem4  12966  prmreclem5  12967  2expltfac  13105  metss2lem  18057  nlmvscnlem2  18196  nrginvrcnlem  18201  nmoco  18246  nmotri  18248  nghmcn  18254  icopnfhmeo  18441  nmoleub2lem3  18596  ipcau2  18664  tchcphlem1  18665  ipcnlem2  18671  pjthlem1  18801  opnmbllem  18956  vitalilem4  18966  itg1val2  19039  itg1cl  19040  itg1ge0  19041  itg1addlem4  19054  itg1mulc  19059  itg1ge0a  19066  itg1climres  19069  mbfi1fseqlem1  19070  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  itg2const2  19096  itg2mulclem  19101  itg2mulc  19102  itg2monolem1  19105  itg2monolem3  19107  itg2cnlem2  19117  iblconst  19172  iblmulc2  19185  itgmulc2lem1  19186  itgmulc2lem2  19187  bddmulibl  19193  dveflem  19326  cmvth  19338  dvlip  19340  dvlipcn  19341  dvivthlem1  19355  lhop1lem  19360  dvcvx  19367  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsum2  19381  ftc1lem4  19386  plyeq0lem  19592  aalioulem3  19714  aalioulem4  19715  aaliou3lem9  19730  ulmdvlem1  19777  itgulm  19784  radcnvlem1  19789  radcnvlem2  19790  dvradcnv  19797  abelthlem2  19808  abelthlem7  19814  tangtx  19873  tanregt0  19901  logdivlti  19971  logcnlem3  19991  logcnlem4  19992  logccv  20010  recxpcl  20022  cxpmul  20035  cxplt  20041  cxple2  20044  abscxpbnd  20093  lawcoslem1  20113  atans2  20227  efrlim  20264  o1cxp  20269  scvxcvx  20280  jensenlem2  20282  amgmlem  20284  fsumharmonic  20305  ftalem1  20310  ftalem2  20311  ftalem5  20314  basellem3  20320  basellem8  20325  chpub  20459  logfacubnd  20460  logfaclbnd  20461  logfacbnd3  20462  logexprlim  20464  perfectlem2  20469  bclbnd  20519  efexple  20520  bposlem1  20523  bposlem2  20524  bposlem6  20528  bposlem9  20531  lgsdilem  20561  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  chebbnd1lem1  20618  chebbnd1lem3  20620  chtppilimlem1  20622  chpchtlim  20628  vmadivsum  20631  rplogsumlem1  20633  rpvmasumlem  20636  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0re  20662  dchrisum0lem1  20665  dirith2  20677  mulogsumlem  20680  mulogsum  20681  mulog2sumlem2  20684  vmalogdivsum2  20687  vmalogdivsum  20688  2vmadivsumlem  20689  logsqvma  20691  logsqvma2  20692  log2sumbnd  20693  selberglem2  20695  selberg  20697  selbergb  20698  selberg2lem  20699  selberg2b  20701  chpdifbndlem1  20702  chpdifbndlem2  20703  selberg3lem1  20706  selberg3lem2  20707  selberg3  20708  selberg4lem1  20709  selberg4  20710  pntrsumbnd2  20716  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntsf  20722  pntsval2  20725  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2a  20739  pntibndlem2  20740  pntlemb  20746  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntlem3  20758  ostth2lem1  20767  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth3  20787  smcnlem  21270  ubthlem2  21450  htthlem  21497  pjhthlem1  21970  cnlnadjlem7  22653  nmopcoadji  22681  branmfn  22685  leopnmid  22718  rmulccn  23301  xrge0iifhom  23319  dya2iocseg  23579  rescon  23777  brbtwn2  24533  colinearalglem4  24537  axsegconlem8  24552  axsegconlem9  24553  axsegconlem10  24554  ax5seglem3  24559  axpaschlem  24568  axpasch  24569  axeuclidlem  24590  areacirclem5  24929  csbrn  26462  trirn  26463  geomcau  26475  bfplem1  26546  bfplem2  26547  bfp  26548  rrnequiv  26559  rrntotbnd  26560  irrapxlem1  26907  irrapxlem2  26908  irrapxlem3  26909  irrapxlem4  26910  irrapxlem5  26911  pellexlem2  26915  pellexlem6  26919  pell14qrgt0  26944  pell1qrge1  26955  pell1qrgaplem  26958  pellqrexplicit  26962  pellqrex  26964  rmxycomplete  27002  rmxypos  27034  ltrmynn0  27035  ltrmxnn0  27036  jm2.24nn  27046  jm2.17a  27047  jm2.17b  27048  jm2.17c  27049  jm2.27c  27100  jm3.1lem2  27111  stoweidlem30  27779  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem15  27837  stirlingr  27839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 8800
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator