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

Theorem remulcld 10233
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 10184 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  (class class class)co 6801  cr 10098   · cmul 10104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10162
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  mulge0  10709  msqge0  10712  redivcl  10907  prodgt0  11031  prodge0  11033  ltmul1a  11035  ltmul1  11036  ltmuldiv  11059  lt2msq1  11070  lt2msq  11071  le2msq  11086  msq11  11087  supmul1  11155  supmullem2  11157  supmul  11158  div4p1lem1div2  11450  mul2lt0rlt0  12096  mul2lt0bi  12100  qbtwnre  12194  xmulneg1  12263  xmulf  12266  lincmb01cmp  12479  iccf1o  12480  flmulnn0  12793  flhalf  12796  modcl  12837  mod0  12840  modge0  12843  modmulnn  12853  mulp1mod1  12876  2txmodxeq0  12895  modaddmulmod  12902  moddi  12903  modsubdir  12904  modirr  12906  addmodlteq  12910  bernneq  13155  bernneq3  13157  expnbnd  13158  expmulnbnd  13161  discr1  13165  discr  13166  faclbnd  13242  faclbnd6  13251  remullem  14038  sqrlem7  14159  sqrtmul  14170  abstri  14240  sqreulem  14269  mulcn2  14496  reccn2  14497  o1rlimmul  14519  lo1mul  14528  iseraltlem2  14583  iseraltlem3  14584  iseralt  14585  o1fsum  14715  cvgcmpce  14720  climcndslem1  14751  climcndslem2  14752  climcnds  14753  geomulcvg  14777  cvgrat  14785  mertenslem1  14786  fprodge1  14896  eftlub  15009  sin02gt0  15092  eirrlem  15102  bitsp1o  15328  isprm5  15592  modprm0  15683  prmreclem3  15795  prmreclem4  15796  prmreclem5  15797  2expltfac  15972  metss2lem  22488  nlmvscnlem2  22661  nrginvrcnlem  22667  nmoco  22713  nmotri  22715  nghmcn  22721  icopnfhmeo  22914  nmoleub2lem3  23086  ipcau2  23204  tchcphlem1  23205  ipcnlem2  23214  rrxcph  23351  csbren  23353  trirn  23354  pjthlem1  23379  opnmbllem  23540  vitalilem4  23550  itg1val2  23621  itg1cl  23622  itg1ge0  23623  itg1addlem4  23636  itg1mulc  23641  itg1ge0a  23648  itg1climres  23651  mbfi1fseqlem1  23652  mbfi1fseqlem3  23654  mbfi1fseqlem4  23655  mbfi1fseqlem5  23656  mbfi1fseqlem6  23657  itg2const2  23678  itg2mulclem  23683  itg2mulc  23684  itg2monolem1  23687  itg2monolem3  23689  itg2cnlem2  23699  iblconst  23754  iblmulc2  23767  itgmulc2lem1  23768  itgmulc2lem2  23769  bddmulibl  23775  dveflem  23912  cmvth  23924  dvlip  23926  dvlipcn  23927  dvivthlem1  23941  lhop1lem  23946  dvcvx  23953  dvfsumlem2  23960  dvfsumlem3  23961  dvfsumlem4  23962  dvfsum2  23967  ftc1lem4  23972  plyeq0lem  24136  aalioulem3  24259  aalioulem4  24260  aaliou3lem9  24275  ulmdvlem1  24324  itgulm  24332  radcnvlem1  24337  radcnvlem2  24338  dvradcnv  24345  abelthlem2  24356  abelthlem7  24362  tangtx  24427  tanregt0  24455  logdivlti  24536  logcnlem3  24560  logcnlem4  24561  logccv  24579  recxpcl  24591  cxpmul  24604  cxplt  24610  cxple2  24613  abscxpbnd  24664  lawcoslem1  24715  heron  24735  atans2  24828  efrlim  24866  o1cxp  24871  scvxcvx  24882  jensenlem2  24884  amgmlem  24886  fsumharmonic  24908  lgamgulmlem2  24926  lgamgulmlem3  24927  lgamgulmlem4  24928  lgamgulmlem5  24929  lgamgulmlem6  24930  relgamcl  24958  ftalem1  24969  ftalem2  24970  ftalem5  24973  basellem3  24979  basellem8  24984  chpub  25115  logfacubnd  25116  logfaclbnd  25117  logfacbnd3  25118  logexprlim  25120  perfectlem2  25125  bclbnd  25175  efexple  25176  bposlem1  25179  bposlem2  25180  bposlem6  25184  bposlem9  25187  lgsdilem  25219  gausslemma2dlem0c  25253  gausslemma2dlem2  25262  gausslemma2dlem3  25263  gausslemma2dlem6  25267  lgseisenlem4  25273  lgseisen  25274  lgsquadlem1  25275  lgsquadlem2  25276  2lgslem1a1  25284  chebbnd1lem1  25328  chebbnd1lem3  25330  chtppilimlem1  25332  chpchtlim  25338  vmadivsum  25341  rplogsumlem1  25343  rpvmasumlem  25346  dchrisumlem2  25349  dchrisumlem3  25350  dchrmusum2  25353  dchrvmasumlem2  25357  dchrvmasumiflem1  25360  dchrisum0re  25372  dchrisum0lem1  25375  dirith2  25387  mulogsumlem  25390  mulogsum  25391  mulog2sumlem2  25394  vmalogdivsum2  25397  vmalogdivsum  25398  2vmadivsumlem  25399  logsqvma  25401  logsqvma2  25402  log2sumbnd  25403  selberglem2  25405  selberg  25407  selbergb  25408  selberg2lem  25409  selberg2b  25411  chpdifbndlem1  25412  chpdifbndlem2  25413  selberg3lem1  25416  selberg3lem2  25417  selberg3  25418  selberg4lem1  25419  selberg4  25420  pntrsumbnd2  25426  selberg3r  25428  selberg4r  25429  selberg34r  25430  pntsf  25432  pntsval2  25435  pntrlog2bndlem1  25436  pntrlog2bndlem2  25437  pntrlog2bndlem3  25438  pntrlog2bndlem4  25439  pntrlog2bndlem5  25440  pntrlog2bndlem6  25442  pntrlog2bnd  25443  pntpbnd1a  25444  pntpbnd1  25445  pntpbnd2  25446  pntibndlem2a  25449  pntibndlem2  25450  pntlemb  25456  pntlemr  25461  pntlemj  25462  pntlemf  25464  pntlemk  25465  pntlemo  25466  pntlem3  25468  ostth2lem1  25477  ostth2lem2  25493  ostth2lem3  25494  ostth2lem4  25495  ostth3  25497  ttgcontlem1  25935  brbtwn2  25955  colinearalglem4  25959  axsegconlem8  25974  axsegconlem9  25975  axsegconlem10  25976  ax5seglem3  25981  axpaschlem  25990  axpasch  25991  axeuclidlem  26012  numclwwlk5  27527  numclwwlk7  27530  smcnlem  27832  ubthlem2  28007  htthlem  28054  pjhthlem1  28530  cnlnadjlem7  29212  nmopcoadji  29240  branmfn  29244  leopnmid  29277  bhmafibid1  29924  2sqmod  29928  rmulccn  30254  xrge0iifhom  30263  nexple  30351  dya2icoseg  30619  eulerpartlems  30702  eulerpartlemgc  30704  eulerpartlemb  30710  plymulx0  30904  signsvtp  30940  reprgt  30979  breprexplemc  30990  circlemethhgt  31001  hgt750lemd  31006  logdivsqrle  31008  hgt750lem  31009  hgt750lemf  31011  hgt750lemb  31014  hgt750lema  31015  hgt750leme  31016  tgoldbachgtde  31018  resconn  31506  knoppcnlem2  32761  knoppcnlem4  32763  knoppcnlem10  32769  unbdqndv2lem1  32777  unbdqndv2lem2  32778  knoppndvlem1  32780  knoppndvlem11  32790  knoppndvlem12  32791  knoppndvlem14  32793  knoppndvlem15  32794  knoppndvlem17  32796  knoppndvlem18  32797  knoppndvlem19  32798  knoppndvlem20  32799  knoppndvlem21  32800  opnmbllem0  33727  itg2addnclem2  33744  itg2addnclem3  33745  iblmulc2nc  33757  itgmulc2nclem1  33758  bddiblnc  33762  ftc1cnnclem  33765  ftc1anclem3  33769  areacirclem4  33785  geomcau  33837  equivbnd  33871  bfplem1  33903  bfplem2  33904  bfp  33905  rrnequiv  33916  rrntotbnd  33917  irrapxlem1  37857  irrapxlem2  37858  irrapxlem3  37859  irrapxlem4  37860  irrapxlem5  37861  pellexlem2  37865  pellexlem6  37869  pell14qrgt0  37894  pell1qrge1  37905  pell1qrgaplem  37908  pellqrexplicit  37912  pellqrex  37914  rmspecsqrtnq  37941  rmxycomplete  37953  rmxypos  37985  ltrmynn0  37986  ltrmxnn0  37987  jm2.24nn  37997  jm2.17a  37998  jm2.17b  37999  jm2.17c  38000  jm2.27c  38045  jm3.1lem2  38056  areaquad  38273  imo72b2lem0  38936  cvgdvgrat  38983  nzprmdif  38989  lt3addmuld  39983  fperiodmullem  39985  fperiodmul  39986  lt4addmuld  39988  xralrple2  40037  xralrple3  40057  ltmulneg  40082  fmul01  40284  fmuldfeqlem1  40286  fmul01lt1lem1  40288  sumnnodd  40334  ltmod  40342  0ellimcdiv  40353  limclner  40355  dvdivbd  40610  dvbdfbdioolem2  40616  dvbdfbdioo  40617  ioodvbdlimc1lem1  40618  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  stoweidlem1  40690  stoweidlem11  40700  stoweidlem13  40702  stoweidlem14  40703  stoweidlem16  40705  stoweidlem17  40706  stoweidlem22  40711  stoweidlem24  40713  stoweidlem25  40714  stoweidlem26  40715  stoweidlem30  40719  stoweidlem34  40723  stoweidlem36  40725  stoweidlem49  40738  stoweidlem59  40748  stoweidlem60  40749  wallispilem4  40757  wallispilem5  40758  wallispi  40759  wallispi2lem1  40760  wallispi2  40762  stirlinglem1  40763  stirlinglem3  40765  stirlinglem5  40767  stirlinglem6  40768  stirlinglem7  40769  stirlinglem10  40772  stirlinglem11  40773  stirlinglem12  40774  stirlinglem15  40777  stirlingr  40779  dirker2re  40781  dirkerval2  40783  dirkerre  40784  dirkertrigeqlem1  40787  dirkertrigeqlem2  40788  dirkeritg  40791  dirkercncflem2  40793  dirkercncflem4  40795  fourierdlem4  40800  fourierdlem5  40801  fourierdlem6  40802  fourierdlem7  40803  fourierdlem16  40812  fourierdlem18  40814  fourierdlem19  40815  fourierdlem21  40817  fourierdlem22  40818  fourierdlem26  40822  fourierdlem35  40831  fourierdlem39  40835  fourierdlem41  40837  fourierdlem42  40838  fourierdlem43  40839  fourierdlem48  40843  fourierdlem49  40844  fourierdlem51  40846  fourierdlem55  40850  fourierdlem56  40851  fourierdlem57  40852  fourierdlem58  40853  fourierdlem62  40857  fourierdlem63  40858  fourierdlem64  40859  fourierdlem65  40860  fourierdlem66  40861  fourierdlem67  40862  fourierdlem68  40863  fourierdlem71  40866  fourierdlem72  40867  fourierdlem73  40868  fourierdlem76  40871  fourierdlem77  40872  fourierdlem78  40873  fourierdlem83  40878  fourierdlem84  40879  fourierdlem87  40882  fourierdlem88  40883  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886  fourierdlem94  40889  fourierdlem95  40890  fourierdlem97  40892  fourierdlem103  40898  fourierdlem104  40899  fourierdlem112  40907  fourierdlem113  40908  sqwvfoura  40917  sqwvfourb  40918  fouriersw  40920  etransclem23  40946  etransclem48  40971  rrndistlt  40982  hoidmvlelem1  41284  hoidmvlelem2  41285  hoidmvlelem4  41287  smfmullem1  41473  smfmullem2  41474  smfmullem3  41475  smfmul  41477  fmtno4prmfac  41963  lighneallem4a  42004  perfectALTVlem2  42110  ply1mulgsumlem2  42654  digvalnn0  42872  dignn0fr  42874  dig2nn0  42884  amgmwlem  43030
  Copyright terms: Public domain W3C validator