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

Theorem remulcld 9926
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 9877 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6527  cr 9791   · cmul 9797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9855
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  mulge0  10395  msqge0  10398  redivcl  10593  prodgt0  10717  prodge0  10719  ltmul1a  10721  ltmul1  10722  ltmuldiv  10745  lt2msq1  10756  lt2msq  10757  le2msq  10772  msq11  10773  supmul1  10839  supmullem2  10841  supmul  10842  div4p1lem1div2  11134  mul2lt0rlt0  11764  mul2lt0bi  11768  qbtwnre  11863  xmulneg1  11928  xmulf  11931  lincmb01cmp  12142  iccf1o  12143  flmulnn0  12445  flhalf  12448  modcl  12489  mod0  12492  modge0  12495  modmulnn  12505  mulp1mod1  12528  2txmodxeq0  12547  modaddmulmod  12554  moddi  12555  modsubdir  12556  modirr  12558  addmodlteq  12562  bernneq  12807  bernneq3  12809  expnbnd  12810  expmulnbnd  12813  discr1  12817  discr  12818  faclbnd  12894  faclbnd6  12903  remullem  13662  sqrlem7  13783  sqrtmul  13794  abstri  13864  sqreulem  13893  mulcn2  14120  reccn2  14121  o1rlimmul  14143  lo1mul  14152  iseraltlem2  14207  iseraltlem3  14208  iseralt  14209  o1fsum  14332  cvgcmpce  14337  climcndslem1  14366  climcndslem2  14367  climcnds  14368  geomulcvg  14392  cvgrat  14400  mertenslem1  14401  fprodge1  14511  eftlub  14624  sin02gt0  14707  eirrlem  14717  bitsp1o  14939  isprm5  15203  modprm0  15294  prmreclem3  15406  prmreclem4  15407  prmreclem5  15408  2expltfac  15583  metss2lem  22067  nlmvscnlem2  22232  nrginvrcnlem  22238  nmoco  22283  nmotri  22285  nghmcn  22291  icopnfhmeo  22481  nmoleub2lem3  22654  ipcau2  22762  tchcphlem1  22763  ipcnlem2  22769  rrxcph  22905  csbren  22907  trirn  22908  pjthlem1  22933  opnmbllem  23092  vitalilem4  23103  itg1val2  23174  itg1cl  23175  itg1ge0  23176  itg1addlem4  23189  itg1mulc  23194  itg1ge0a  23201  itg1climres  23204  mbfi1fseqlem1  23205  mbfi1fseqlem3  23207  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  mbfi1fseqlem6  23210  itg2const2  23231  itg2mulclem  23236  itg2mulc  23237  itg2monolem1  23240  itg2monolem3  23242  itg2cnlem2  23252  iblconst  23307  iblmulc2  23320  itgmulc2lem1  23321  itgmulc2lem2  23322  bddmulibl  23328  dveflem  23463  cmvth  23475  dvlip  23477  dvlipcn  23478  dvivthlem1  23492  lhop1lem  23497  dvcvx  23504  dvfsumlem2  23511  dvfsumlem3  23512  dvfsumlem4  23513  dvfsum2  23518  ftc1lem4  23523  plyeq0lem  23687  aalioulem3  23810  aalioulem4  23811  aaliou3lem9  23826  ulmdvlem1  23875  itgulm  23883  radcnvlem1  23888  radcnvlem2  23889  dvradcnv  23896  abelthlem2  23907  abelthlem7  23913  tangtx  23978  tanregt0  24006  logdivlti  24087  logcnlem3  24107  logcnlem4  24108  logccv  24126  recxpcl  24138  cxpmul  24151  cxplt  24157  cxple2  24160  abscxpbnd  24211  lawcoslem1  24262  heron  24282  atans2  24375  efrlim  24413  o1cxp  24418  scvxcvx  24429  jensenlem2  24431  amgmlem  24433  fsumharmonic  24455  lgamgulmlem2  24473  lgamgulmlem3  24474  lgamgulmlem4  24475  lgamgulmlem5  24476  lgamgulmlem6  24477  relgamcl  24505  ftalem1  24516  ftalem2  24517  ftalem5  24520  basellem3  24526  basellem8  24531  chpub  24662  logfacubnd  24663  logfaclbnd  24664  logfacbnd3  24665  logexprlim  24667  perfectlem2  24672  bclbnd  24722  efexple  24723  bposlem1  24726  bposlem2  24727  bposlem6  24731  bposlem9  24734  lgsdilem  24766  gausslemma2dlem0c  24800  gausslemma2dlem2  24809  gausslemma2dlem3  24810  gausslemma2dlem6  24814  lgseisenlem4  24820  lgseisen  24821  lgsquadlem1  24822  lgsquadlem2  24823  2lgslem1a1  24831  chebbnd1lem1  24875  chebbnd1lem3  24877  chtppilimlem1  24879  chpchtlim  24885  vmadivsum  24888  rplogsumlem1  24890  rpvmasumlem  24893  dchrisumlem2  24896  dchrisumlem3  24897  dchrmusum2  24900  dchrvmasumlem2  24904  dchrvmasumiflem1  24907  dchrisum0re  24919  dchrisum0lem1  24922  dirith2  24934  mulogsumlem  24937  mulogsum  24938  mulog2sumlem2  24941  vmalogdivsum2  24944  vmalogdivsum  24945  2vmadivsumlem  24946  logsqvma  24948  logsqvma2  24949  log2sumbnd  24950  selberglem2  24952  selberg  24954  selbergb  24955  selberg2lem  24956  selberg2b  24958  chpdifbndlem1  24959  chpdifbndlem2  24960  selberg3lem1  24963  selberg3lem2  24964  selberg3  24965  selberg4lem1  24966  selberg4  24967  pntrsumbnd2  24973  selberg3r  24975  selberg4r  24976  selberg34r  24977  pntsf  24979  pntsval2  24982  pntrlog2bndlem1  24983  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bndlem6  24989  pntrlog2bnd  24990  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntibndlem2a  24996  pntibndlem2  24997  pntlemb  25003  pntlemr  25008  pntlemj  25009  pntlemf  25011  pntlemk  25012  pntlemo  25013  pntlem3  25015  ostth2lem1  25024  ostth2lem2  25040  ostth2lem3  25041  ostth2lem4  25042  ostth3  25044  ttgcontlem1  25483  brbtwn2  25503  colinearalglem4  25507  axsegconlem8  25522  axsegconlem9  25523  axsegconlem10  25524  ax5seglem3  25529  axpaschlem  25538  axpasch  25539  axeuclidlem  25560  numclwwlk5  26405  numclwwlk7  26407  smcnlem  26737  ubthlem2  26917  htthlem  26964  pjhthlem1  27440  cnlnadjlem7  28122  nmopcoadji  28150  branmfn  28154  leopnmid  28187  bhmafibid1  28781  2sqmod  28785  rmulccn  29108  xrge0iifhom  29117  nexple  29205  dya2icoseg  29472  eulerpartlems  29555  eulerpartlemgc  29557  eulerpartlemb  29563  plymulx0  29756  signsvtp  29792  rescon  30288  knoppcnlem2  31460  knoppcnlem4  31462  knoppcnlem10  31468  unbdqndv2lem1  31476  unbdqndv2lem2  31477  knoppndvlem1  31479  knoppndvlem11  31489  knoppndvlem12  31490  knoppndvlem14  31492  knoppndvlem15  31493  knoppndvlem17  31495  knoppndvlem18  31496  knoppndvlem19  31497  knoppndvlem20  31498  knoppndvlem21  31499  opnmbllem0  32411  itg2addnclem2  32428  itg2addnclem3  32429  iblmulc2nc  32441  itgmulc2nclem1  32442  bddiblnc  32446  ftc1cnnclem  32449  ftc1anclem3  32453  areacirclem4  32469  geomcau  32521  equivbnd  32555  bfplem1  32587  bfplem2  32588  bfp  32589  rrnequiv  32600  rrntotbnd  32601  irrapxlem1  36200  irrapxlem2  36201  irrapxlem3  36202  irrapxlem4  36203  irrapxlem5  36204  pellexlem2  36208  pellexlem6  36212  pell14qrgt0  36237  pell1qrge1  36248  pell1qrgaplem  36251  pellqrexplicit  36255  pellqrex  36257  rmspecsqrtnq  36284  rmxycomplete  36296  rmxypos  36328  ltrmynn0  36329  ltrmxnn0  36330  jm2.24nn  36340  jm2.17a  36341  jm2.17b  36342  jm2.17c  36343  jm2.27c  36388  jm3.1lem2  36399  areaquad  36617  imo72b2lem0  37283  cvgdvgrat  37330  nzprmdif  37336  lt3addmuld  38252  fperiodmullem  38254  fperiodmul  38255  lt4addmuld  38257  xralrple2  38308  xralrple3  38328  ltmulneg  38353  fmul01  38444  fmuldfeqlem1  38446  fmul01lt1lem1  38448  sumnnodd  38494  ltmod  38502  0ellimcdiv  38513  limclner  38515  dvdivbd  38610  dvbdfbdioolem2  38616  dvbdfbdioo  38617  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  stoweidlem1  38691  stoweidlem11  38701  stoweidlem13  38703  stoweidlem14  38704  stoweidlem16  38706  stoweidlem17  38707  stoweidlem22  38712  stoweidlem24  38714  stoweidlem25  38715  stoweidlem26  38716  stoweidlem30  38720  stoweidlem34  38724  stoweidlem36  38726  stoweidlem49  38739  stoweidlem59  38749  stoweidlem60  38750  wallispilem4  38758  wallispilem5  38759  wallispi  38760  wallispi2lem1  38761  wallispi2  38763  stirlinglem1  38764  stirlinglem3  38766  stirlinglem5  38768  stirlinglem6  38769  stirlinglem7  38770  stirlinglem10  38773  stirlinglem11  38774  stirlinglem12  38775  stirlinglem15  38778  stirlingr  38780  dirker2re  38782  dirkerval2  38784  dirkerre  38785  dirkertrigeqlem1  38788  dirkertrigeqlem2  38789  dirkeritg  38792  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem4  38801  fourierdlem5  38802  fourierdlem6  38803  fourierdlem7  38804  fourierdlem16  38813  fourierdlem18  38815  fourierdlem19  38816  fourierdlem21  38818  fourierdlem22  38819  fourierdlem26  38823  fourierdlem35  38832  fourierdlem39  38836  fourierdlem41  38838  fourierdlem42  38839  fourierdlem43  38840  fourierdlem48  38844  fourierdlem49  38845  fourierdlem51  38847  fourierdlem55  38851  fourierdlem56  38852  fourierdlem57  38853  fourierdlem58  38854  fourierdlem62  38858  fourierdlem63  38859  fourierdlem64  38860  fourierdlem65  38861  fourierdlem66  38862  fourierdlem67  38863  fourierdlem68  38864  fourierdlem71  38867  fourierdlem72  38868  fourierdlem73  38869  fourierdlem76  38872  fourierdlem77  38873  fourierdlem78  38874  fourierdlem83  38879  fourierdlem84  38880  fourierdlem87  38883  fourierdlem88  38884  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem94  38890  fourierdlem95  38891  fourierdlem97  38893  fourierdlem103  38899  fourierdlem104  38900  fourierdlem112  38908  fourierdlem113  38909  sqwvfoura  38918  sqwvfourb  38919  fouriersw  38921  etransclem23  38947  etransclem48  38972  rrndistlt  38983  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem4  39285  smfmullem1  39473  smfmullem2  39474  smfmullem3  39475  smfmul  39477  fmtno4prmfac  39820  lighneallem4a  39861  perfectALTVlem2  39963  av-numclwwlk5  41537  av-numclwwlk7  41540  ply1mulgsumlem2  41964  digvalnn0  42186  dignn0fr  42188  dig2nn0  42198  amgmwlem  42313
  Copyright terms: Public domain W3C validator