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

Theorem remulcld 10660
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 10611 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  cr 10525   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10589
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  mulge0  11147  msqge0  11150  redivcl  11348  prodgt0  11476  ltmul1a  11478  ltmul1  11479  ltmuldiv  11502  lt2msq1  11513  lt2msq  11514  le2msq  11529  msq11  11530  supmul1  11599  supmullem2  11601  supmul  11602  div4p1lem1div2  11881  mul2lt0rlt0  12481  mul2lt0bi  12485  prodge0rd  12486  qbtwnre  12582  xmulneg1  12652  xmulf  12655  lincmb01cmp  12871  iccf1o  12872  flmulnn0  13187  flhalf  13190  modcl  13231  mod0  13234  modge0  13237  modmulnn  13247  mulp1mod1  13270  2txmodxeq0  13289  modaddmulmod  13296  moddi  13297  modsubdir  13298  modirr  13300  addmodlteq  13304  bernneq  13580  bernneq3  13582  expnbnd  13583  expmulnbnd  13586  discr1  13590  discr  13591  faclbnd  13640  faclbnd6  13649  remullem  14477  sqrlem7  14598  sqrtmul  14609  abstri  14680  sqreulem  14709  bhmafibid1  14815  mulcn2  14942  reccn2  14943  o1rlimmul  14965  lo1mul  14974  iseraltlem2  15029  iseraltlem3  15030  iseralt  15031  o1fsum  15158  cvgcmpce  15163  climcndslem1  15194  climcndslem2  15195  climcnds  15196  geomulcvg  15222  cvgrat  15229  mertenslem1  15230  fprodge1  15339  eftlub  15452  sin02gt0  15535  eirrlem  15547  bitsp1o  15772  2mulprm  16027  isprm5  16041  modprm0  16132  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  2expltfac  16416  metss2lem  23050  nlmvscnlem2  23223  nrginvrcnlem  23229  nmoco  23275  nmotri  23277  nghmcn  23283  icopnfhmeo  23476  nmoleub2lem3  23648  ipcau2  23766  tcphcphlem1  23767  ipcnlem2  23776  rrxcph  23924  csbren  23931  trirn  23932  pjthlem1  23969  opnmbllem  24131  vitalilem4  24141  itg1val2  24214  itg1cl  24215  itg1ge0  24216  itg1addlem4  24229  itg1mulc  24234  itg1ge0a  24241  itg1climres  24244  mbfi1fseqlem1  24245  mbfi1fseqlem3  24247  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  itg2const2  24271  itg2mulclem  24276  itg2mulc  24277  itg2monolem1  24280  itg2monolem3  24282  itg2cnlem2  24292  iblconst  24347  iblmulc2  24360  itgmulc2lem1  24361  itgmulc2lem2  24362  bddmulibl  24368  dveflem  24505  cmvth  24517  dvlip  24519  dvlipcn  24520  dvivthlem1  24534  lhop1lem  24539  dvcvx  24546  dvfsumlem2  24553  dvfsumlem3  24554  dvfsumlem4  24555  dvfsum2  24560  ftc1lem4  24565  plyeq0lem  24729  aalioulem3  24852  aalioulem4  24853  aaliou3lem9  24868  ulmdvlem1  24917  itgulm  24925  radcnvlem1  24930  radcnvlem2  24931  dvradcnv  24938  abelthlem2  24949  abelthlem7  24955  tangtx  25020  tanregt0  25050  logdivlti  25130  logcnlem3  25154  logcnlem4  25155  logccv  25173  recxpcl  25185  cxpmul  25198  cxplt  25204  cxple2  25207  abscxpbnd  25261  lawcoslem1  25320  heron  25343  atans2  25436  efrlim  25475  o1cxp  25480  scvxcvx  25491  jensenlem2  25493  amgmlem  25495  fsumharmonic  25517  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem5  25538  lgamgulmlem6  25539  relgamcl  25567  ftalem1  25578  ftalem2  25579  ftalem5  25582  basellem3  25588  basellem8  25593  chpub  25724  logfacubnd  25725  logfaclbnd  25726  logfacbnd3  25727  logexprlim  25729  perfectlem2  25734  bclbnd  25784  efexple  25785  bposlem1  25788  bposlem2  25789  bposlem6  25793  bposlem9  25796  lgsdilem  25828  gausslemma2dlem0c  25862  gausslemma2dlem2  25871  gausslemma2dlem3  25872  gausslemma2dlem6  25876  lgseisenlem4  25882  lgseisen  25883  lgsquadlem1  25884  lgsquadlem2  25885  2lgslem1a1  25893  2sqmod  25940  chebbnd1lem1  25973  chebbnd1lem3  25975  chtppilimlem1  25977  chpchtlim  25983  vmadivsum  25986  rplogsumlem1  25988  rpvmasumlem  25991  dchrisumlem2  25994  dchrisumlem3  25995  dchrmusum2  25998  dchrvmasumlem2  26002  dchrvmasumiflem1  26005  dchrisum0re  26017  dchrisum0lem1  26020  dirith2  26032  mulogsumlem  26035  mulogsum  26036  mulog2sumlem2  26039  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  logsqvma  26046  logsqvma2  26047  log2sumbnd  26048  selberglem2  26050  selberg  26052  selbergb  26053  selberg2lem  26054  selberg2b  26056  chpdifbndlem1  26057  chpdifbndlem2  26058  selberg3lem1  26061  selberg3lem2  26062  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrsumbnd2  26071  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntsf  26077  pntsval2  26080  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntibndlem2a  26094  pntibndlem2  26095  pntlemb  26101  pntlemr  26106  pntlemj  26107  pntlemf  26109  pntlemk  26110  pntlemo  26111  pntlem3  26113  ostth2lem1  26122  ostth2lem2  26138  ostth2lem3  26139  ostth2lem4  26140  ostth3  26142  ttgcontlem1  26599  brbtwn2  26619  colinearalglem4  26623  axsegconlem8  26638  axsegconlem9  26639  axsegconlem10  26640  ax5seglem3  26645  axpaschlem  26654  axpasch  26655  axeuclidlem  26676  numclwwlk5  28095  numclwwlk7  28098  smcnlem  28402  ubthlem2  28576  htthlem  28622  pjhthlem1  29096  cnlnadjlem7  29778  nmopcoadji  29806  branmfn  29810  leopnmid  29843  rmulccn  31071  xrge0iifhom  31080  nexple  31168  dya2icoseg  31435  eulerpartlems  31518  eulerpartlemgc  31520  eulerpartlemb  31526  plymulx0  31717  signsvtp  31753  reprgt  31792  breprexplemc  31803  circlemethhgt  31814  hgt750lemd  31819  logdivsqrle  31821  hgt750lem  31822  hgt750lemf  31824  hgt750lemb  31827  hgt750lema  31828  hgt750leme  31829  tgoldbachgtde  31831  resconn  32391  knoppcnlem2  33731  knoppcnlem4  33733  knoppcnlem10  33739  unbdqndv2lem1  33746  unbdqndv2lem2  33747  knoppndvlem1  33749  knoppndvlem11  33759  knoppndvlem12  33760  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem17  33765  knoppndvlem18  33766  knoppndvlem19  33767  knoppndvlem20  33768  knoppndvlem21  33769  opnmbllem0  34810  itg2addnclem2  34826  itg2addnclem3  34827  iblmulc2nc  34839  itgmulc2nclem1  34840  bddiblnc  34844  ftc1cnnclem  34847  ftc1anclem3  34851  areacirclem4  34867  geomcau  34917  equivbnd  34951  bfplem1  34983  bfplem2  34984  bfp  34985  rrnequiv  34996  rrntotbnd  34997  cxpgt0d  39060  resubdi  39106  remul02  39115  remul01  39117  remulinvcom  39128  fltnltalem  39154  fltnlta  39155  3cubeslem2  39162  3cubeslem3r  39164  3cubeslem4  39166  irrapxlem1  39299  irrapxlem2  39300  irrapxlem3  39301  irrapxlem4  39302  irrapxlem5  39303  pellexlem2  39307  pellexlem6  39311  pell14qrgt0  39336  pell1qrge1  39347  pell1qrgaplem  39350  pellqrexplicit  39354  pellqrex  39356  rmspecsqrtnq  39383  rmxycomplete  39394  rmxypos  39424  ltrmynn0  39425  ltrmxnn0  39426  jm2.24nn  39436  jm2.17a  39437  jm2.17b  39438  jm2.17c  39439  jm2.27c  39484  jm3.1lem2  39495  areaquad  39703  imo72b2lem0  40396  cvgdvgrat  40525  nzprmdif  40531  lt3addmuld  41448  fperiodmullem  41450  fperiodmul  41451  lt4addmuld  41453  xralrple2  41502  xralrple3  41522  ltmulneg  41544  fmul01  41741  fmuldfeqlem1  41743  fmul01lt1lem1  41745  sumnnodd  41791  ltmod  41799  0ellimcdiv  41810  limclner  41812  dvdivbd  42088  dvbdfbdioolem2  42094  dvbdfbdioo  42095  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  stoweidlem1  42167  stoweidlem11  42177  stoweidlem13  42179  stoweidlem14  42180  stoweidlem16  42182  stoweidlem17  42183  stoweidlem22  42188  stoweidlem24  42190  stoweidlem25  42191  stoweidlem26  42192  stoweidlem30  42196  stoweidlem34  42200  stoweidlem36  42202  stoweidlem49  42215  stoweidlem59  42225  stoweidlem60  42226  wallispilem4  42234  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2  42239  stirlinglem1  42240  stirlinglem3  42242  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  stirlinglem15  42254  stirlingr  42256  dirker2re  42258  dirkerval2  42260  dirkerre  42261  dirkertrigeqlem1  42264  dirkertrigeqlem2  42265  dirkeritg  42268  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem4  42277  fourierdlem5  42278  fourierdlem6  42279  fourierdlem7  42280  fourierdlem16  42289  fourierdlem18  42291  fourierdlem19  42292  fourierdlem21  42294  fourierdlem22  42295  fourierdlem26  42299  fourierdlem35  42308  fourierdlem39  42312  fourierdlem41  42314  fourierdlem42  42315  fourierdlem43  42316  fourierdlem48  42320  fourierdlem49  42321  fourierdlem51  42323  fourierdlem55  42327  fourierdlem56  42328  fourierdlem57  42329  fourierdlem58  42330  fourierdlem62  42334  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem66  42338  fourierdlem67  42339  fourierdlem68  42340  fourierdlem71  42343  fourierdlem72  42344  fourierdlem73  42345  fourierdlem76  42348  fourierdlem77  42349  fourierdlem78  42350  fourierdlem83  42355  fourierdlem84  42356  fourierdlem87  42359  fourierdlem88  42360  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem94  42366  fourierdlem95  42367  fourierdlem97  42369  fourierdlem103  42375  fourierdlem104  42376  fourierdlem112  42384  fourierdlem113  42385  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  etransclem23  42423  etransclem48  42448  rrndistlt  42456  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem4  42761  smfmullem1  42947  smfmullem2  42948  smfmullem3  42949  smfmul  42951  fmtno4prmfac  43581  lighneallem4a  43620  requad01  43633  requad1  43634  requad2  43635  perfectALTVlem2  43734  ply1mulgsumlem2  44339  digvalnn0  44557  dignn0fr  44559  dig2nn0  44569  affinecomb1  44587  rrx2linest2  44629  line2  44637  itsclc0lem1  44641  itsclc0lem2  44642  itsclc0lem3  44643  itscnhlc0yqe  44644  itsclc0yqsollem2  44648  itsclc0yqsol  44649  itscnhlc0xyqsol  44650  itsclc0xyqsolr  44654  itsclinecirc0  44658  itsclinecirc0b  44659  itsclinecirc0in  44660  itsclquadb  44661  itsclquadeu  44662  2itscp  44666  itscnhlinecirc02plem1  44667  itscnhlinecirc02p  44670  inlinecirc02plem  44671  amgmwlem  44801
  Copyright terms: Public domain W3C validator