Theorem remulcld 10506

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

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		remulcl 10457	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2079  (class class class)co 7007  ℝcr 10371   · cmul 10377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10435

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  mulge0  10995  msqge0  10998  redivcl  11196  prodgt0  11324  ltmul1a  11326  ltmul1  11327  ltmuldiv  11350  lt2msq1  11361  lt2msq  11362  le2msq  11377  msq11  11378  supmul1  11447  supmullem2  11449  supmul  11450  div4p1lem1div2  11729  mul2lt0rlt0  12330  mul2lt0bi  12334  prodge0rd  12335  qbtwnre  12431  xmulneg1  12501  xmulf  12504  lincmb01cmp  12720  iccf1o  12721  flmulnn0  13035  flhalf  13038  modcl  13079  mod0  13082  modge0  13085  modmulnn  13095  mulp1mod1  13118  2txmodxeq0  13137  modaddmulmod  13144  moddi  13145  modsubdir  13146  modirr  13148  addmodlteq  13152  bernneq  13428  bernneq3  13430  expnbnd  13431  expmulnbnd  13434  discr1  13438  discr  13439  faclbnd  13488  faclbnd6  13497  remullem  14309  sqrlem7  14430  sqrtmul  14441  abstri  14512  sqreulem  14541  bhmafibid1  14647  mulcn2  14774  reccn2  14775  o1rlimmul  14797  lo1mul  14806  iseraltlem2  14861  iseraltlem3  14862  iseralt  14863  o1fsum  14989  cvgcmpce  14994  climcndslem1  15025  climcndslem2  15026  climcnds  15027  geomulcvg  15053  cvgrat  15060  mertenslem1  15061  fprodge1  15170  eftlub  15283  sin02gt0  15366  eirrlem  15378  bitsp1o  15603  2mulprm  15854  isprm5  15868  modprm0  15959  prmreclem3  16071  prmreclem4  16072  prmreclem5  16073  2expltfac  16243  metss2lem  22792  nlmvscnlem2  22965  nrginvrcnlem  22971  nmoco  23017  nmotri  23019  nghmcn  23025  icopnfhmeo  23218  nmoleub2lem3  23390  ipcau2  23508  tcphcphlem1  23509  ipcnlem2  23518  rrxcph  23666  csbren  23673  trirn  23674  pjthlem1  23711  opnmbllem  23873  vitalilem4  23883  itg1val2  23956  itg1cl  23957  itg1ge0  23958  itg1addlem4  23971  itg1mulc  23976  itg1ge0a  23983  itg1climres  23986  mbfi1fseqlem1  23987  mbfi1fseqlem3  23989  mbfi1fseqlem4  23990  mbfi1fseqlem5  23991  mbfi1fseqlem6  23992  itg2const2  24013  itg2mulclem  24018  itg2mulc  24019  itg2monolem1  24022  itg2monolem3  24024  itg2cnlem2  24034  iblconst  24089  iblmulc2  24102  itgmulc2lem1  24103  itgmulc2lem2  24104  bddmulibl  24110  dveflem  24247  cmvth  24259  dvlip  24261  dvlipcn  24262  dvivthlem1  24276  lhop1lem  24281  dvcvx  24288  dvfsumlem2  24295  dvfsumlem3  24296  dvfsumlem4  24297  dvfsum2  24302  ftc1lem4  24307  plyeq0lem  24471  aalioulem3  24594  aalioulem4  24595  aaliou3lem9  24610  ulmdvlem1  24659  itgulm  24667  radcnvlem1  24672  radcnvlem2  24673  dvradcnv  24680  abelthlem2  24691  abelthlem7  24697  tangtx  24762  tanregt0  24792  logdivlti  24872  logcnlem3  24896  logcnlem4  24897  logccv  24915  recxpcl  24927  cxpmul  24940  cxplt  24946  cxple2  24949  abscxpbnd  25003  lawcoslem1  25062  heron  25085  atans2  25178  efrlim  25217  o1cxp  25222  scvxcvx  25233  jensenlem2  25235  amgmlem  25237  fsumharmonic  25259  lgamgulmlem2  25277  lgamgulmlem3  25278  lgamgulmlem4  25279  lgamgulmlem5  25280  lgamgulmlem6  25281  relgamcl  25309  ftalem1  25320  ftalem2  25321  ftalem5  25324  basellem3  25330  basellem8  25335  chpub  25466  logfacubnd  25467  logfaclbnd  25468  logfacbnd3  25469  logexprlim  25471  perfectlem2  25476  bclbnd  25526  efexple  25527  bposlem1  25530  bposlem2  25531  bposlem6  25535  bposlem9  25538  lgsdilem  25570  gausslemma2dlem0c  25604  gausslemma2dlem2  25613  gausslemma2dlem3  25614  gausslemma2dlem6  25618  lgseisenlem4  25624  lgseisen  25625  lgsquadlem1  25626  lgsquadlem2  25627  2lgslem1a1  25635  2sqmod  25682  chebbnd1lem1  25715  chebbnd1lem3  25717  chtppilimlem1  25719  chpchtlim  25725  vmadivsum  25728  rplogsumlem1  25730  rpvmasumlem  25733  dchrisumlem2  25736  dchrisumlem3  25737  dchrmusum2  25740  dchrvmasumlem2  25744  dchrvmasumiflem1  25747  dchrisum0re  25759  dchrisum0lem1  25762  dirith2  25774  mulogsumlem  25777  mulogsum  25778  mulog2sumlem2  25781  vmalogdivsum2  25784  vmalogdivsum  25785  2vmadivsumlem  25786  logsqvma  25788  logsqvma2  25789  log2sumbnd  25790  selberglem2  25792  selberg  25794  selbergb  25795  selberg2lem  25796  selberg2b  25798  chpdifbndlem1  25799  chpdifbndlem2  25800  selberg3lem1  25803  selberg3lem2  25804  selberg3  25805  selberg4lem1  25806  selberg4  25807  pntrsumbnd2  25813  selberg3r  25815  selberg4r  25816  selberg34r  25817  pntsf  25819  pntsval2  25822  pntrlog2bndlem1  25823  pntrlog2bndlem2  25824  pntrlog2bndlem3  25825  pntrlog2bndlem4  25826  pntrlog2bndlem5  25827  pntrlog2bndlem6  25829  pntrlog2bnd  25830  pntpbnd1a  25831  pntpbnd1  25832  pntpbnd2  25833  pntibndlem2a  25836  pntibndlem2  25837  pntlemb  25843  pntlemr  25848  pntlemj  25849  pntlemf  25851  pntlemk  25852  pntlemo  25853  pntlem3  25855  ostth2lem1  25864  ostth2lem2  25880  ostth2lem3  25881  ostth2lem4  25882  ostth3  25884  ttgcontlem1  26342  brbtwn2  26362  colinearalglem4  26366  axsegconlem8  26381  axsegconlem9  26382  axsegconlem10  26383  ax5seglem3  26388  axpaschlem  26397  axpasch  26398  axeuclidlem  26419  numclwwlk5  27847  numclwwlk7  27850  smcnlem  28153  ubthlem2  28327  htthlem  28373  pjhthlem1  28847  cnlnadjlem7  29529  nmopcoadji  29557  branmfn  29561  leopnmid  29594  rmulccn  30744  xrge0iifhom  30753  nexple  30841  dya2icoseg  31108  eulerpartlems  31191  eulerpartlemgc  31193  eulerpartlemb  31199  plymulx0  31390  signsvtp  31426  reprgt  31465  breprexplemc  31476  circlemethhgt  31487  hgt750lemd  31492  logdivsqrle  31494  hgt750lem  31495  hgt750lemf  31497  hgt750lemb  31500  hgt750lema  31501  hgt750leme  31502  tgoldbachgtde  31504  resconn  32057  knoppcnlem2  33386  knoppcnlem4  33388  knoppcnlem10  33394  unbdqndv2lem1  33401  unbdqndv2lem2  33402  knoppndvlem1  33404  knoppndvlem11  33414  knoppndvlem12  33415  knoppndvlem14  33417  knoppndvlem15  33418  knoppndvlem17  33420  knoppndvlem18  33421  knoppndvlem19  33422  knoppndvlem20  33423  knoppndvlem21  33424  opnmbllem0  34405  itg2addnclem2  34421  itg2addnclem3  34422  iblmulc2nc  34434  itgmulc2nclem1  34435  bddiblnc  34439  ftc1cnnclem  34442  ftc1anclem3  34446  areacirclem4  34462  geomcau  34512  equivbnd  34546  bfplem1  34578  bfplem2  34579  bfp  34580  rrnequiv  34591  rrntotbnd  34592  cxpgt0d  38652  resubdi  38697  fltnltalem  38721  fltnlta  38722  irrapxlem1  38855  irrapxlem2  38856  irrapxlem3  38857  irrapxlem4  38858  irrapxlem5  38859  pellexlem2  38863  pellexlem6  38867  pell14qrgt0  38892  pell1qrge1  38903  pell1qrgaplem  38906  pellqrexplicit  38910  pellqrex  38912  rmspecsqrtnq  38939  rmxycomplete  38950  rmxypos  38980  ltrmynn0  38981  ltrmxnn0  38982  jm2.24nn  38992  jm2.17a  38993  jm2.17b  38994  jm2.17c  38995  jm2.27c  39040  jm3.1lem2  39051  areaquad  39259  imo72b2lem0  39953  cvgdvgrat  40135  nzprmdif  40141  lt3addmuld  41062  fperiodmullem  41064  fperiodmul  41065  lt4addmuld  41067  xralrple2  41116  xralrple3  41136  ltmulneg  41159  fmul01  41357  fmuldfeqlem1  41359  fmul01lt1lem1  41361  sumnnodd  41407  ltmod  41415  0ellimcdiv  41426  limclner  41428  dvdivbd  41703  dvbdfbdioolem2  41709  dvbdfbdioo  41710  ioodvbdlimc1lem1  41711  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  stoweidlem1  41782  stoweidlem11  41792  stoweidlem13  41794  stoweidlem14  41795  stoweidlem16  41797  stoweidlem17  41798  stoweidlem22  41803  stoweidlem24  41805  stoweidlem25  41806  stoweidlem26  41807  stoweidlem30  41811  stoweidlem34  41815  stoweidlem36  41817  stoweidlem49  41830  stoweidlem59  41840  stoweidlem60  41841  wallispilem4  41849  wallispilem5  41850  wallispi  41851  wallispi2lem1  41852  wallispi2  41854  stirlinglem1  41855  stirlinglem3  41857  stirlinglem5  41859  stirlinglem6  41860  stirlinglem7  41861  stirlinglem10  41864  stirlinglem11  41865  stirlinglem12  41866  stirlinglem15  41869  stirlingr  41871  dirker2re  41873  dirkerval2  41875  dirkerre  41876  dirkertrigeqlem1  41879  dirkertrigeqlem2  41880  dirkeritg  41883  dirkercncflem2  41885  dirkercncflem4  41887  fourierdlem4  41892  fourierdlem5  41893  fourierdlem6  41894  fourierdlem7  41895  fourierdlem16  41904  fourierdlem18  41906  fourierdlem19  41907  fourierdlem21  41909  fourierdlem22  41910  fourierdlem26  41914  fourierdlem35  41923  fourierdlem39  41927  fourierdlem41  41929  fourierdlem42  41930  fourierdlem43  41931  fourierdlem48  41935  fourierdlem49  41936  fourierdlem51  41938  fourierdlem55  41942  fourierdlem56  41943  fourierdlem57  41944  fourierdlem58  41945  fourierdlem62  41949  fourierdlem63  41950  fourierdlem64  41951  fourierdlem65  41952  fourierdlem66  41953  fourierdlem67  41954  fourierdlem68  41955  fourierdlem71  41958  fourierdlem72  41959  fourierdlem73  41960  fourierdlem76  41963  fourierdlem77  41964  fourierdlem78  41965  fourierdlem83  41970  fourierdlem84  41971  fourierdlem87  41974  fourierdlem88  41975  fourierdlem89  41976  fourierdlem90  41977  fourierdlem91  41978  fourierdlem94  41981  fourierdlem95  41982  fourierdlem97  41984  fourierdlem103  41990  fourierdlem104  41991  fourierdlem112  41999  fourierdlem113  42000  sqwvfoura  42009  sqwvfourb  42010  fouriersw  42012  etransclem23  42038  etransclem48  42063  rrndistlt  42071  hoidmvlelem1  42373  hoidmvlelem2  42374  hoidmvlelem4  42376  smfmullem1  42562  smfmullem2  42563  smfmullem3  42564  smfmul  42566  fmtno4prmfac  43170  lighneallem4a  43209  requad01  43222  requad1  43223  requad2  43224  perfectALTVlem2  43323  ply1mulgsumlem2  43875  digvalnn0  44094  dignn0fr  44096  dig2nn0  44106  affinecomb1  44124  rrx2linest2  44166  line2  44174  itsclc0lem1  44178  itsclc0lem2  44179  itsclc0lem3  44180  itscnhlc0yqe  44181  itsclc0yqsollem2  44185  itsclc0yqsol  44186  itscnhlc0xyqsol  44187  itsclc0xyqsolr  44191  itsclinecirc0  44195  itsclinecirc0b  44196  itsclinecirc0in  44197  itsclquadb  44198  itsclquadeu  44199  2itscp  44203  itscnhlinecirc02plem1  44204  itscnhlinecirc02p  44207  inlinecirc02plem  44208  amgmwlem  44337