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

Theorem remulcld 9645
Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1
readdcld.2
Assertion
Ref Expression
remulcld

Proof of Theorem remulcld
StepHypRef Expression
1 recnd.1 . 2
2 readdcld.2 . 2
3 remulcl 9598 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  (class class class)co 6296   cr 9512   cmul 9518
This theorem is referenced by:  mulge0  10095  msqge0  10099  redivcl  10288  prodgt0  10412  prodge0  10414  ltmul1a  10416  ltmul1  10417  ltmuldiv  10440  lt2msq1  10453  lt2msq  10454  le2msq  10470  msq11  10471  supmul1  10533  supmullem2  10535  supmul  10536  qbtwnre  11427  xmulneg1  11490  xmulf  11493  lincmb01cmp  11692  iccf1o  11693  flmulnn0  11960  flhalf  11962  modcl  12000  mod0  12003  modge0  12005  modmulnn  12013  2txmodxeq0  12047  modaddmulmod  12053  moddi  12054  modsubdir  12055  modirr  12057  bernneq  12292  bernneq3  12294  expnbnd  12295  expmulnbnd  12298  discr1  12302  discr  12303  faclbnd  12368  faclbnd6  12377  remullem  12961  sqrlem7  13082  sqrtmul  13093  abstri  13163  sqreulem  13192  mulcn2  13418  reccn2  13419  o1rlimmul  13441  lo1mul  13450  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  o1fsum  13627  cvgcmpce  13632  climcndslem1  13661  climcndslem2  13662  climcnds  13663  geomulcvg  13685  cvgrat  13692  mertenslem1  13693  eftlub  13844  sin02gt0  13927  eirrlem  13937  bitsp1o  14083  isprm5  14253  modprm0  14330  prmreclem3  14436  prmreclem4  14437  prmreclem5  14438  2expltfac  14577  metss2lem  21014  nlmvscnlem2  21194  nrginvrcnlem  21199  nmoco  21244  nmotri  21246  nghmcn  21252  icopnfhmeo  21443  nmoleub2lem3  21598  ipcau2  21677  tchcphlem1  21678  ipcnlem2  21684  rrxcph  21824  csbren  21826  trirn  21827  pjthlem1  21852  opnmbllem  22010  vitalilem4  22020  itg1val2  22091  itg1cl  22092  itg1ge0  22093  itg1addlem4  22106  itg1mulc  22111  itg1ge0a  22118  itg1climres  22121  mbfi1fseqlem1  22122  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  itg2const2  22148  itg2mulclem  22153  itg2mulc  22154  itg2monolem1  22157  itg2monolem3  22159  itg2cnlem2  22169  iblconst  22224  iblmulc2  22237  itgmulc2lem1  22238  itgmulc2lem2  22239  bddmulibl  22245  dveflem  22380  cmvth  22392  dvlip  22394  dvlipcn  22395  dvivthlem1  22409  lhop1lem  22414  dvcvx  22421  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsum2  22435  ftc1lem4  22440  plyeq0lem  22607  aalioulem3  22730  aalioulem4  22731  aaliou3lem9  22746  ulmdvlem1  22795  itgulm  22803  radcnvlem1  22808  radcnvlem2  22809  dvradcnv  22816  abelthlem2  22827  abelthlem7  22833  tangtx  22898  tanregt0  22926  logdivlti  23005  logcnlem3  23025  logcnlem4  23026  logccv  23044  recxpcl  23056  cxpmul  23069  cxplt  23075  cxple2  23078  abscxpbnd  23127  lawcoslem1  23147  heron  23169  atans2  23262  efrlim  23299  o1cxp  23304  scvxcvx  23315  jensenlem2  23317  amgmlem  23319  fsumharmonic  23341  ftalem1  23346  ftalem2  23347  ftalem5  23350  basellem3  23356  basellem8  23361  chpub  23495  logfacubnd  23496  logfaclbnd  23497  logfacbnd3  23498  logexprlim  23500  perfectlem2  23505  bclbnd  23555  efexple  23556  bposlem1  23559  bposlem2  23560  bposlem6  23564  bposlem9  23567  lgsdilem  23597  lgseisenlem4  23627  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  chebbnd1lem1  23654  chebbnd1lem3  23656  chtppilimlem1  23658  chpchtlim  23664  vmadivsum  23667  rplogsumlem1  23669  rpvmasumlem  23672  dchrisumlem2  23675  dchrisumlem3  23676  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  dchrisum0re  23698  dchrisum0lem1  23701  dirith2  23713  mulogsumlem  23716  mulogsum  23717  mulog2sumlem2  23720  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  logsqvma  23727  logsqvma2  23728  log2sumbnd  23729  selberglem2  23731  selberg  23733  selbergb  23734  selberg2lem  23735  selberg2b  23737  chpdifbndlem1  23738  chpdifbndlem2  23739  selberg3lem1  23742  selberg3lem2  23743  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrsumbnd2  23752  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntsf  23758  pntsval2  23761  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem2a  23775  pntibndlem2  23776  pntlemb  23782  pntlemr  23787  pntlemj  23788  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntlem3  23794  ostth2lem1  23803  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  ostth3  23823  ttgcontlem1  24188  brbtwn2  24208  colinearalglem4  24212  axsegconlem8  24227  axsegconlem9  24228  axsegconlem10  24229  ax5seglem3  24234  axpaschlem  24243  axpasch  24244  axeuclidlem  24265  numclwwlk5  25112  numclwwlk7  25114  smcnlem  25607  ubthlem2  25787  htthlem  25834  pjhthlem1  26309  cnlnadjlem7  26992  nmopcoadji  27020  branmfn  27024  leopnmid  27057  mul2lt0rlt0  27565  mul2lt0bi  27569  bhmafibid1  27632  2sqmod  27636  rmulccn  27910  xrge0iifhom  27919  nexple  28005  dya2icoseg  28248  eulerpartlems  28299  eulerpartlemgc  28301  eulerpartlemb  28307  plymulx0  28504  signsvtp  28540  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  relgamcl  28604  rescon  28691  opnmbllem0  30050  itg2addnclem2  30067  itg2addnclem3  30068  iblmulc2nc  30080  itgmulc2nclem1  30081  bddiblnc  30085  ftc1cnnclem  30088  ftc1anclem3  30092  areacirclem4  30110  geomcau  30252  equivbnd  30286  bfplem1  30318  bfplem2  30319  bfp  30320  rrnequiv  30331  rrntotbnd  30332  irrapxlem1  30758  irrapxlem2  30759  irrapxlem3  30760  irrapxlem4  30761  irrapxlem5  30762  pellexlem2  30766  pellexlem6  30770  pell14qrgt0  30795  pell1qrge1  30806  pell1qrgaplem  30809  pellqrexplicit  30813  pellqrex  30815  rmxycomplete  30853  rmxypos  30885  ltrmynn0  30886  ltrmxnn0  30887  jm2.24nn  30897  jm2.17a  30898  jm2.17b  30899  jm2.17c  30900  jm2.27c  30949  jm3.1lem2  30960  areaquad  31184  cvgdvgrat  31194  nzprmdif  31224  lt3addmuld  31501  fperiodmullem  31503  fperiodmul  31504  lt4addmuld  31506  fmul01  31574  fmuldfeqlem1  31576  fmul01lt1lem1  31578  fprodge1  31598  sumnnodd  31636  ltmod  31644  0ellimcdiv  31655  limclner  31657  dvdivbd  31720  dvbdfbdioolem2  31726  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem1  31783  stoweidlem11  31793  stoweidlem13  31795  stoweidlem14  31796  stoweidlem16  31798  stoweidlem17  31799  stoweidlem22  31804  stoweidlem24  31806  stoweidlem25  31807  stoweidlem26  31808  stoweidlem30  31812  stoweidlem34  31816  stoweidlem36  31818  stoweidlem49  31831  stoweidlem59  31841  stoweidlem60  31842  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  stirlinglem15  31870  stirlingr  31872  dirker2re  31874  dirkerval2  31876  dirkerre  31877  dirkertrigeqlem1  31880  dirkertrigeqlem2  31881  dirkeritg  31884  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem4  31893  fourierdlem5  31894  fourierdlem6  31895  fourierdlem7  31896  fourierdlem16  31905  fourierdlem18  31907  fourierdlem19  31908  fourierdlem21  31910  fourierdlem22  31911  fourierdlem26  31915  fourierdlem35  31924  fourierdlem39  31928  fourierdlem41  31930  fourierdlem42  31931  fourierdlem43  31932  fourierdlem48  31937  fourierdlem49  31938  fourierdlem51  31940  fourierdlem55  31944  fourierdlem56  31945  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem66  31955  fourierdlem67  31956  fourierdlem68  31957  fourierdlem71  31960  fourierdlem72  31961  fourierdlem73  31962  fourierdlem76  31965  fourierdlem77  31966  fourierdlem78  31967  fourierdlem83  31972  fourierdlem84  31973  fourierdlem87  31976  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem94  31983  fourierdlem95  31984  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  etransclem23  32040  etransclem48  32065  ply1mulgsumlem2  32987  imo72b2lem0  37982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9576
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator