Theorem remulcld 11248

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

Syntax hints:   → wi 4   ∈ wcel 2104  (class class class)co 7411  ℝcr 11111   · cmul 11117

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

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

This theorem is referenced by:  mulge0  11736  msqge0  11739  redivcl  11937  prodgt0  12065  ltmul1a  12067  ltmul1  12068  ltmuldiv  12091  lt2msq1  12102  lt2msq  12103  le2msq  12118  msq11  12119  supmul1  12187  supmullem2  12189  supmul  12190  div4p1lem1div2  12471  mul2lt0rlt0  13080  mul2lt0bi  13084  prodge0rd  13085  qbtwnre  13182  xmulneg1  13252  xmulf  13255  lincmb01cmp  13476  iccf1o  13477  flmulnn0  13796  flhalf  13799  modcl  13842  mod0  13845  modge0  13848  modmulnn  13858  mulp1mod1  13881  2txmodxeq0  13900  modaddmulmod  13907  moddi  13908  modsubdir  13909  modirr  13911  addmodlteq  13915  bernneq  14196  bernneq3  14198  expnbnd  14199  expmulnbnd  14202  discr1  14206  discr  14207  faclbnd  14254  faclbnd6  14263  remullem  15079  01sqrexlem7  15199  sqrtmul  15210  abstri  15281  sqreulem  15310  bhmafibid1  15416  mulcn2  15544  reccn2  15545  o1rlimmul  15567  lo1mul  15576  iseraltlem2  15633  iseraltlem3  15634  iseralt  15635  o1fsum  15763  cvgcmpce  15768  climcndslem1  15799  climcndslem2  15800  climcnds  15801  geomulcvg  15826  cvgrat  15833  mertenslem1  15834  fprodge1  15943  eftlub  16056  sin02gt0  16139  eirrlem  16151  bitsp1o  16378  2mulprm  16634  isprm5  16648  modprm0  16742  prmreclem3  16855  prmreclem4  16856  prmreclem5  16857  2expltfac  17030  metss2lem  24240  nlmvscnlem2  24422  nrginvrcnlem  24428  nmoco  24474  nmotri  24476  nghmcn  24482  icopnfhmeo  24688  nmoleub2lem3  24862  ipcau2  24982  tcphcphlem1  24983  ipcnlem2  24992  rrxcph  25140  csbren  25147  trirn  25148  pjthlem1  25185  opnmbllem  25350  vitalilem4  25360  itg1val2  25433  itg1cl  25434  itg1ge0  25435  itg1addlem4  25448  itg1addlem4OLD  25449  itg1mulc  25454  itg1ge0a  25461  itg1climres  25464  mbfi1fseqlem1  25465  mbfi1fseqlem3  25467  mbfi1fseqlem4  25468  mbfi1fseqlem5  25469  mbfi1fseqlem6  25470  itg2const2  25491  itg2mulclem  25496  itg2mulc  25497  itg2monolem1  25500  itg2monolem3  25502  itg2cnlem2  25512  iblconst  25567  iblmulc2  25580  itgmulc2lem1  25581  itgmulc2lem2  25582  bddmulibl  25588  bddiblnc  25591  dveflem  25731  cmvth  25743  dvlip  25745  dvlipcn  25746  dvivthlem1  25760  lhop1lem  25765  dvcvx  25772  dvfsumlem2  25779  dvfsumlem3  25780  dvfsumlem4  25781  dvfsum2  25786  ftc1lem4  25791  plyeq0lem  25959  aalioulem3  26083  aalioulem4  26084  aaliou3lem9  26099  ulmdvlem1  26148  itgulm  26156  radcnvlem1  26161  radcnvlem2  26162  dvradcnv  26169  abelthlem2  26180  abelthlem7  26186  tangtx  26251  tanregt0  26284  logdivlti  26364  logcnlem3  26388  logcnlem4  26389  logccv  26407  recxpcl  26419  cxpmul  26432  cxplt  26438  cxple2  26441  abscxpbnd  26497  lawcoslem1  26556  heron  26579  atans2  26672  efrlim  26710  o1cxp  26715  scvxcvx  26726  jensenlem2  26728  amgmlem  26730  fsumharmonic  26752  lgamgulmlem2  26770  lgamgulmlem3  26771  lgamgulmlem4  26772  lgamgulmlem5  26773  lgamgulmlem6  26774  relgamcl  26802  ftalem1  26813  ftalem2  26814  ftalem5  26817  basellem3  26823  basellem8  26828  chpub  26959  logfacubnd  26960  logfaclbnd  26961  logfacbnd3  26962  logexprlim  26964  perfectlem2  26969  bclbnd  27019  efexple  27020  bposlem1  27023  bposlem2  27024  bposlem6  27028  bposlem9  27031  lgsdilem  27063  gausslemma2dlem0c  27097  gausslemma2dlem2  27106  gausslemma2dlem3  27107  gausslemma2dlem6  27111  lgseisenlem4  27117  lgseisen  27118  lgsquadlem1  27119  lgsquadlem2  27120  2lgslem1a1  27128  2sqmod  27175  chebbnd1lem1  27208  chebbnd1lem3  27210  chtppilimlem1  27212  chpchtlim  27218  vmadivsum  27221  rplogsumlem1  27223  rpvmasumlem  27226  dchrisumlem2  27229  dchrisumlem3  27230  dchrmusum2  27233  dchrvmasumlem2  27237  dchrvmasumiflem1  27240  dchrisum0re  27252  dchrisum0lem1  27255  dirith2  27267  mulogsumlem  27270  mulogsum  27271  mulog2sumlem2  27274  vmalogdivsum2  27277  vmalogdivsum  27278  2vmadivsumlem  27279  logsqvma  27281  logsqvma2  27282  log2sumbnd  27283  selberglem2  27285  selberg  27287  selbergb  27288  selberg2lem  27289  selberg2b  27291  chpdifbndlem1  27292  chpdifbndlem2  27293  selberg3lem1  27296  selberg3lem2  27297  selberg3  27298  selberg4lem1  27299  selberg4  27300  pntrsumbnd2  27306  selberg3r  27308  selberg4r  27309  selberg34r  27310  pntsf  27312  pntsval2  27315  pntrlog2bndlem1  27316  pntrlog2bndlem2  27317  pntrlog2bndlem3  27318  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntrlog2bnd  27323  pntpbnd1a  27324  pntpbnd1  27325  pntpbnd2  27326  pntibndlem2a  27329  pntibndlem2  27330  pntlemb  27336  pntlemr  27341  pntlemj  27342  pntlemf  27344  pntlemk  27345  pntlemo  27346  pntlem3  27348  ostth2lem1  27357  ostth2lem2  27373  ostth2lem3  27374  ostth2lem4  27375  ostth3  27377  ttgcontlem1  28409  brbtwn2  28430  colinearalglem4  28434  axsegconlem8  28449  axsegconlem9  28450  axsegconlem10  28451  ax5seglem3  28456  axpaschlem  28465  axpasch  28466  axeuclidlem  28487  numclwwlk5  29908  numclwwlk7  29911  smcnlem  30217  ubthlem2  30391  htthlem  30437  pjhthlem1  30911  cnlnadjlem7  31593  nmopcoadji  31621  branmfn  31625  leopnmid  31658  rmulccn  33206  xrge0iifhom  33215  nexple  33305  dya2icoseg  33574  eulerpartlems  33657  eulerpartlemgc  33659  eulerpartlemb  33665  plymulx0  33856  signsvtp  33892  reprgt  33931  breprexplemc  33942  circlemethhgt  33953  hgt750lemd  33958  logdivsqrle  33960  hgt750lem  33961  hgt750lemf  33963  hgt750lemb  33966  hgt750lema  33967  hgt750leme  33968  tgoldbachgtde  33970  resconn  34535  gg-rmulccn  35465  gg-cmvth  35466  gg-dvfsumlem2  35469  knoppcnlem2  35673  knoppcnlem4  35675  knoppcnlem10  35681  unbdqndv2lem1  35688  unbdqndv2lem2  35689  knoppndvlem1  35691  knoppndvlem11  35701  knoppndvlem12  35702  knoppndvlem14  35704  knoppndvlem15  35705  knoppndvlem17  35707  knoppndvlem18  35708  knoppndvlem19  35709  knoppndvlem20  35710  knoppndvlem21  35711  opnmbllem0  36827  itg2addnclem2  36843  itg2addnclem3  36844  iblmulc2nc  36856  itgmulc2nclem1  36857  ftc1cnnclem  36862  ftc1anclem3  36866  areacirclem4  36882  geomcau  36930  equivbnd  36961  bfplem1  36993  bfplem2  36994  bfp  36995  rrnequiv  37006  rrntotbnd  37007  lcmineqlem19  41218  lcmineqlem20  41219  lcmineqlem21  41220  lcmineqlem22  41221  3lexlogpow2ineq2  41230  dvrelogpow2b  41239  aks4d1p1p2  41241  aks4d1p1p4  41242  aks4d1p1p6  41244  aks4d1p1p7  41245  aks4d1p1p5  41246  aks4d1p1  41247  aks4d1p8d2  41256  aks4d1p8  41258  2np3bcnp1  41266  2ap1caineq  41267  resubdi  41571  remul02  41580  remul01  41582  remulinvcom  41607  sn-0tie0  41614  renegmulnnass  41628  mulgt0con1d  41633  mulgt0con2d  41634  mulgt0b2d  41635  sn-ltmul2d  41636  sn-inelr  41640  itrere  41641  retire  41642  fltnltalem  41706  fltnlta  41707  3cubeslem2  41725  3cubeslem3r  41727  3cubeslem4  41729  irrapxlem1  41862  irrapxlem2  41863  irrapxlem3  41864  irrapxlem4  41865  irrapxlem5  41866  pellexlem2  41870  pellexlem6  41874  pell14qrgt0  41899  pell1qrge1  41910  pell1qrgaplem  41913  pellqrexplicit  41917  pellqrex  41919  rmspecsqrtnq  41946  rmxycomplete  41958  rmxypos  41988  ltrmynn0  41989  ltrmxnn0  41990  jm2.24nn  42000  jm2.17a  42001  jm2.17b  42002  jm2.17c  42003  jm2.27c  42048  jm3.1lem2  42059  areaquad  42267  sqrtcval  42694  resqrtval  42696  imsqrtval  42697  imo72b2lem0  43219  cvgdvgrat  43374  nzprmdif  43380  lt3addmuld  44309  fperiodmullem  44311  fperiodmul  44312  lt4addmuld  44314  xralrple2  44362  xralrple3  44382  ltmulneg  44400  fmul01  44594  fmuldfeqlem1  44596  fmul01lt1lem1  44598  sumnnodd  44644  ltmod  44652  0ellimcdiv  44663  limclner  44665  dvdivbd  44937  dvbdfbdioolem2  44943  dvbdfbdioo  44944  ioodvbdlimc1lem1  44945  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stoweidlem1  45015  stoweidlem11  45025  stoweidlem13  45027  stoweidlem14  45028  stoweidlem16  45030  stoweidlem17  45031  stoweidlem22  45036  stoweidlem24  45038  stoweidlem25  45039  stoweidlem26  45040  stoweidlem30  45044  stoweidlem34  45048  stoweidlem36  45050  stoweidlem49  45063  stoweidlem59  45073  stoweidlem60  45074  wallispilem4  45082  wallispilem5  45083  wallispi  45084  wallispi2lem1  45085  wallispi2  45087  stirlinglem1  45088  stirlinglem3  45090  stirlinglem5  45092  stirlinglem6  45093  stirlinglem7  45094  stirlinglem10  45097  stirlinglem11  45098  stirlinglem12  45099  stirlinglem15  45102  stirlingr  45104  dirker2re  45106  dirkerval2  45108  dirkerre  45109  dirkertrigeqlem1  45112  dirkertrigeqlem2  45113  dirkeritg  45116  dirkercncflem2  45118  dirkercncflem4  45120  fourierdlem4  45125  fourierdlem5  45126  fourierdlem6  45127  fourierdlem7  45128  fourierdlem16  45137  fourierdlem18  45139  fourierdlem19  45140  fourierdlem21  45142  fourierdlem22  45143  fourierdlem26  45147  fourierdlem35  45156  fourierdlem39  45160  fourierdlem41  45162  fourierdlem42  45163  fourierdlem43  45164  fourierdlem48  45168  fourierdlem49  45169  fourierdlem51  45171  fourierdlem55  45175  fourierdlem56  45176  fourierdlem57  45177  fourierdlem58  45178  fourierdlem62  45182  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem66  45186  fourierdlem67  45187  fourierdlem68  45188  fourierdlem71  45191  fourierdlem72  45192  fourierdlem73  45193  fourierdlem76  45196  fourierdlem77  45197  fourierdlem78  45198  fourierdlem83  45203  fourierdlem84  45204  fourierdlem87  45207  fourierdlem88  45208  fourierdlem89  45209  fourierdlem90  45210  fourierdlem91  45211  fourierdlem94  45214  fourierdlem95  45215  fourierdlem97  45217  fourierdlem103  45223  fourierdlem104  45224  fourierdlem112  45232  fourierdlem113  45233  sqwvfoura  45242  sqwvfourb  45243  fouriersw  45245  etransclem23  45271  etransclem48  45296  rrndistlt  45304  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem4  45612  smfmullem1  45805  smfmullem2  45806  smfmullem3  45807  smfmul  45809  fmtno4prmfac  46538  lighneallem4a  46574  requad01  46587  requad1  46588  requad2  46589  perfectALTVlem2  46688  ply1mulgsumlem2  47155  digvalnn0  47372  dignn0fr  47374  dig2nn0  47384  affinecomb1  47475  rrx2linest2  47517  line2  47525  itsclc0lem1  47529  itsclc0lem2  47530  itsclc0lem3  47531  itscnhlc0yqe  47532  itsclc0yqsollem2  47536  itsclc0yqsol  47537  itscnhlc0xyqsol  47538  itsclc0xyqsolr  47542  itsclinecirc0  47546  itsclinecirc0b  47547  itsclinecirc0in  47548  itsclquadb  47549  itsclquadeu  47550  2itscp  47554  itscnhlinecirc02plem1  47555  itscnhlinecirc02p  47558  inlinecirc02plem  47559  amgmwlem  47936