Theorem remulcld 11051

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 11002	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2104  (class class class)co 7307  ℝcr 10916   · cmul 10922

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

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  mulge0  11539  msqge0  11542  redivcl  11740  prodgt0  11868  ltmul1a  11870  ltmul1  11871  ltmuldiv  11894  lt2msq1  11905  lt2msq  11906  le2msq  11921  msq11  11922  supmul1  11990  supmullem2  11992  supmul  11993  div4p1lem1div2  12274  mul2lt0rlt0  12878  mul2lt0bi  12882  prodge0rd  12883  qbtwnre  12979  xmulneg1  13049  xmulf  13052  lincmb01cmp  13273  iccf1o  13274  flmulnn0  13593  flhalf  13596  modcl  13639  mod0  13642  modge0  13645  modmulnn  13655  mulp1mod1  13678  2txmodxeq0  13697  modaddmulmod  13704  moddi  13705  modsubdir  13706  modirr  13708  addmodlteq  13712  bernneq  13990  bernneq3  13992  expnbnd  13993  expmulnbnd  13996  discr1  14000  discr  14001  faclbnd  14050  faclbnd6  14059  remullem  14884  sqrlem7  15005  sqrtmul  15016  abstri  15087  sqreulem  15116  bhmafibid1  15222  mulcn2  15350  reccn2  15351  o1rlimmul  15373  lo1mul  15382  iseraltlem2  15439  iseraltlem3  15440  iseralt  15441  o1fsum  15570  cvgcmpce  15575  climcndslem1  15606  climcndslem2  15607  climcnds  15608  geomulcvg  15633  cvgrat  15640  mertenslem1  15641  fprodge1  15750  eftlub  15863  sin02gt0  15946  eirrlem  15958  bitsp1o  16185  2mulprm  16443  isprm5  16457  modprm0  16551  prmreclem3  16664  prmreclem4  16665  prmreclem5  16666  2expltfac  16839  metss2lem  23712  nlmvscnlem2  23894  nrginvrcnlem  23900  nmoco  23946  nmotri  23948  nghmcn  23954  icopnfhmeo  24151  nmoleub2lem3  24323  ipcau2  24443  tcphcphlem1  24444  ipcnlem2  24453  rrxcph  24601  csbren  24608  trirn  24609  pjthlem1  24646  opnmbllem  24810  vitalilem4  24820  itg1val2  24893  itg1cl  24894  itg1ge0  24895  itg1addlem4  24908  itg1addlem4OLD  24909  itg1mulc  24914  itg1ge0a  24921  itg1climres  24924  mbfi1fseqlem1  24925  mbfi1fseqlem3  24927  mbfi1fseqlem4  24928  mbfi1fseqlem5  24929  mbfi1fseqlem6  24930  itg2const2  24951  itg2mulclem  24956  itg2mulc  24957  itg2monolem1  24960  itg2monolem3  24962  itg2cnlem2  24972  iblconst  25027  iblmulc2  25040  itgmulc2lem1  25041  itgmulc2lem2  25042  bddmulibl  25048  bddiblnc  25051  dveflem  25188  cmvth  25200  dvlip  25202  dvlipcn  25203  dvivthlem1  25217  lhop1lem  25222  dvcvx  25229  dvfsumlem2  25236  dvfsumlem3  25237  dvfsumlem4  25238  dvfsum2  25243  ftc1lem4  25248  plyeq0lem  25416  aalioulem3  25539  aalioulem4  25540  aaliou3lem9  25555  ulmdvlem1  25604  itgulm  25612  radcnvlem1  25617  radcnvlem2  25618  dvradcnv  25625  abelthlem2  25636  abelthlem7  25642  tangtx  25707  tanregt0  25740  logdivlti  25820  logcnlem3  25844  logcnlem4  25845  logccv  25863  recxpcl  25875  cxpmul  25888  cxplt  25894  cxple2  25897  abscxpbnd  25951  lawcoslem1  26010  heron  26033  atans2  26126  efrlim  26164  o1cxp  26169  scvxcvx  26180  jensenlem2  26182  amgmlem  26184  fsumharmonic  26206  lgamgulmlem2  26224  lgamgulmlem3  26225  lgamgulmlem4  26226  lgamgulmlem5  26227  lgamgulmlem6  26228  relgamcl  26256  ftalem1  26267  ftalem2  26268  ftalem5  26271  basellem3  26277  basellem8  26282  chpub  26413  logfacubnd  26414  logfaclbnd  26415  logfacbnd3  26416  logexprlim  26418  perfectlem2  26423  bclbnd  26473  efexple  26474  bposlem1  26477  bposlem2  26478  bposlem6  26482  bposlem9  26485  lgsdilem  26517  gausslemma2dlem0c  26551  gausslemma2dlem2  26560  gausslemma2dlem3  26561  gausslemma2dlem6  26565  lgseisenlem4  26571  lgseisen  26572  lgsquadlem1  26573  lgsquadlem2  26574  2lgslem1a1  26582  2sqmod  26629  chebbnd1lem1  26662  chebbnd1lem3  26664  chtppilimlem1  26666  chpchtlim  26672  vmadivsum  26675  rplogsumlem1  26677  rpvmasumlem  26680  dchrisumlem2  26683  dchrisumlem3  26684  dchrmusum2  26687  dchrvmasumlem2  26691  dchrvmasumiflem1  26694  dchrisum0re  26706  dchrisum0lem1  26709  dirith2  26721  mulogsumlem  26724  mulogsum  26725  mulog2sumlem2  26728  vmalogdivsum2  26731  vmalogdivsum  26732  2vmadivsumlem  26733  logsqvma  26735  logsqvma2  26736  log2sumbnd  26737  selberglem2  26739  selberg  26741  selbergb  26742  selberg2lem  26743  selberg2b  26745  chpdifbndlem1  26746  chpdifbndlem2  26747  selberg3lem1  26750  selberg3lem2  26751  selberg3  26752  selberg4lem1  26753  selberg4  26754  pntrsumbnd2  26760  selberg3r  26762  selberg4r  26763  selberg34r  26764  pntsf  26766  pntsval2  26769  pntrlog2bndlem1  26770  pntrlog2bndlem2  26771  pntrlog2bndlem3  26772  pntrlog2bndlem4  26773  pntrlog2bndlem5  26774  pntrlog2bndlem6  26776  pntrlog2bnd  26777  pntpbnd1a  26778  pntpbnd1  26779  pntpbnd2  26780  pntibndlem2a  26783  pntibndlem2  26784  pntlemb  26790  pntlemr  26795  pntlemj  26796  pntlemf  26798  pntlemk  26799  pntlemo  26800  pntlem3  26802  ostth2lem1  26811  ostth2lem2  26827  ostth2lem3  26828  ostth2lem4  26829  ostth3  26831  ttgcontlem1  27297  brbtwn2  27318  colinearalglem4  27322  axsegconlem8  27337  axsegconlem9  27338  axsegconlem10  27339  ax5seglem3  27344  axpaschlem  27353  axpasch  27354  axeuclidlem  27375  numclwwlk5  28797  numclwwlk7  28800  smcnlem  29104  ubthlem2  29278  htthlem  29324  pjhthlem1  29798  cnlnadjlem7  30480  nmopcoadji  30508  branmfn  30512  leopnmid  30545  rmulccn  31923  xrge0iifhom  31932  nexple  32022  dya2icoseg  32289  eulerpartlems  32372  eulerpartlemgc  32374  eulerpartlemb  32380  plymulx0  32571  signsvtp  32607  reprgt  32646  breprexplemc  32657  circlemethhgt  32668  hgt750lemd  32673  logdivsqrle  32675  hgt750lem  32676  hgt750lemf  32678  hgt750lemb  32681  hgt750lema  32682  hgt750leme  32683  tgoldbachgtde  32685  resconn  33253  knoppcnlem2  34719  knoppcnlem4  34721  knoppcnlem10  34727  unbdqndv2lem1  34734  unbdqndv2lem2  34735  knoppndvlem1  34737  knoppndvlem11  34747  knoppndvlem12  34748  knoppndvlem14  34750  knoppndvlem15  34751  knoppndvlem17  34753  knoppndvlem18  34754  knoppndvlem19  34755  knoppndvlem20  34756  knoppndvlem21  34757  opnmbllem0  35857  itg2addnclem2  35873  itg2addnclem3  35874  iblmulc2nc  35886  itgmulc2nclem1  35887  ftc1cnnclem  35892  ftc1anclem3  35896  areacirclem4  35912  geomcau  35961  equivbnd  35992  bfplem1  36024  bfplem2  36025  bfp  36026  rrnequiv  36037  rrntotbnd  36038  lcmineqlem19  40097  lcmineqlem20  40098  lcmineqlem21  40099  lcmineqlem22  40100  3lexlogpow2ineq2  40109  dvrelogpow2b  40118  aks4d1p1p2  40120  aks4d1p1p4  40121  aks4d1p1p6  40123  aks4d1p1p7  40124  aks4d1p1p5  40125  aks4d1p1  40126  aks4d1p8d2  40135  aks4d1p8  40137  2np3bcnp1  40142  2ap1caineq  40143  resubdi  40416  remul02  40425  remul01  40427  remulinvcom  40451  sn-0tie0  40458  mulgt0con1d  40465  mulgt0con2d  40466  mulgt0b2d  40467  sn-ltmul2d  40468  sn-inelr  40472  itrere  40473  retire  40474  fltnltalem  40536  fltnlta  40537  3cubeslem2  40544  3cubeslem3r  40546  3cubeslem4  40548  irrapxlem1  40681  irrapxlem2  40682  irrapxlem3  40683  irrapxlem4  40684  irrapxlem5  40685  pellexlem2  40689  pellexlem6  40693  pell14qrgt0  40718  pell1qrge1  40729  pell1qrgaplem  40732  pellqrexplicit  40736  pellqrex  40738  rmspecsqrtnq  40765  rmxycomplete  40777  rmxypos  40807  ltrmynn0  40808  ltrmxnn0  40809  jm2.24nn  40819  jm2.17a  40820  jm2.17b  40821  jm2.17c  40822  jm2.27c  40867  jm3.1lem2  40878  areaquad  41085  sqrtcval  41287  resqrtval  41289  imsqrtval  41290  imo72b2lem0  41814  cvgdvgrat  41969  nzprmdif  41975  lt3addmuld  42888  fperiodmullem  42890  fperiodmul  42891  lt4addmuld  42893  xralrple2  42941  xralrple3  42961  ltmulneg  42980  fmul01  43170  fmuldfeqlem1  43172  fmul01lt1lem1  43174  sumnnodd  43220  ltmod  43228  0ellimcdiv  43239  limclner  43241  dvdivbd  43513  dvbdfbdioolem2  43519  dvbdfbdioo  43520  ioodvbdlimc1lem1  43521  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  stoweidlem1  43591  stoweidlem11  43601  stoweidlem13  43603  stoweidlem14  43604  stoweidlem16  43606  stoweidlem17  43607  stoweidlem22  43612  stoweidlem24  43614  stoweidlem25  43615  stoweidlem26  43616  stoweidlem30  43620  stoweidlem34  43624  stoweidlem36  43626  stoweidlem49  43639  stoweidlem59  43649  stoweidlem60  43650  wallispilem4  43658  wallispilem5  43659  wallispi  43660  wallispi2lem1  43661  wallispi2  43663  stirlinglem1  43664  stirlinglem3  43666  stirlinglem5  43668  stirlinglem6  43669  stirlinglem7  43670  stirlinglem10  43673  stirlinglem11  43674  stirlinglem12  43675  stirlinglem15  43678  stirlingr  43680  dirker2re  43682  dirkerval2  43684  dirkerre  43685  dirkertrigeqlem1  43688  dirkertrigeqlem2  43689  dirkeritg  43692  dirkercncflem2  43694  dirkercncflem4  43696  fourierdlem4  43701  fourierdlem5  43702  fourierdlem6  43703  fourierdlem7  43704  fourierdlem16  43713  fourierdlem18  43715  fourierdlem19  43716  fourierdlem21  43718  fourierdlem22  43719  fourierdlem26  43723  fourierdlem35  43732  fourierdlem39  43736  fourierdlem41  43738  fourierdlem42  43739  fourierdlem43  43740  fourierdlem48  43744  fourierdlem49  43745  fourierdlem51  43747  fourierdlem55  43751  fourierdlem56  43752  fourierdlem57  43753  fourierdlem58  43754  fourierdlem62  43758  fourierdlem63  43759  fourierdlem64  43760  fourierdlem65  43761  fourierdlem66  43762  fourierdlem67  43763  fourierdlem68  43764  fourierdlem71  43767  fourierdlem72  43768  fourierdlem73  43769  fourierdlem76  43772  fourierdlem77  43773  fourierdlem78  43774  fourierdlem83  43779  fourierdlem84  43780  fourierdlem87  43783  fourierdlem88  43784  fourierdlem89  43785  fourierdlem90  43786  fourierdlem91  43787  fourierdlem94  43790  fourierdlem95  43791  fourierdlem97  43793  fourierdlem103  43799  fourierdlem104  43800  fourierdlem112  43808  fourierdlem113  43809  sqwvfoura  43818  sqwvfourb  43819  fouriersw  43821  etransclem23  43847  etransclem48  43872  rrndistlt  43880  hoidmvlelem1  44183  hoidmvlelem2  44184  hoidmvlelem4  44186  smfmullem1  44379  smfmullem2  44380  smfmullem3  44381  smfmul  44383  fmtno4prmfac  45082  lighneallem4a  45118  requad01  45131  requad1  45132  requad2  45133  perfectALTVlem2  45232  ply1mulgsumlem2  45786  digvalnn0  46003  dignn0fr  46005  dig2nn0  46015  affinecomb1  46106  rrx2linest2  46148  line2  46156  itsclc0lem1  46160  itsclc0lem2  46161  itsclc0lem3  46162  itscnhlc0yqe  46163  itsclc0yqsollem2  46167  itsclc0yqsol  46168  itscnhlc0xyqsol  46169  itsclc0xyqsolr  46173  itsclinecirc0  46177  itsclinecirc0b  46178  itsclinecirc0in  46179  itsclquadb  46180  itsclquadeu  46181  2itscp  46185  itscnhlinecirc02plem1  46186  itscnhlinecirc02p  46189  inlinecirc02plem  46190  amgmwlem  46564