Theorem remulcld 11296

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

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7426  ℝcr 11159   · cmul 11165

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

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

This theorem is referenced by:  mulge0  11784  msqge0  11787  redivcl  11986  prodgt0  12114  ltmul1a  12116  ltmul1  12117  ltmuldiv  12141  lt2msq1  12152  lt2msq  12153  le2msq  12168  msq11  12169  supmul1  12237  supmullem2  12239  supmul  12240  div4p1lem1div2  12521  mul2lt0rlt0  13132  mul2lt0bi  13136  prodge0rd  13137  qbtwnre  13234  xmulneg1  13304  xmulf  13307  lincmb01cmp  13528  iccf1o  13529  flmulnn0  13849  flhalf  13852  modcl  13895  mod0  13898  modge0  13901  modmulnn  13911  mulp1mod1  13934  2txmodxeq0  13953  modaddmulmod  13960  moddi  13961  modsubdir  13962  modirr  13964  addmodlteq  13968  bernneq  14248  bernneq3  14250  expnbnd  14251  expmulnbnd  14254  discr1  14258  discr  14259  faclbnd  14309  faclbnd6  14318  remullem  15135  01sqrexlem7  15255  sqrtmul  15266  abstri  15337  sqreulem  15366  bhmafibid1  15472  mulcn2  15600  reccn2  15601  o1rlimmul  15623  lo1mul  15632  iseraltlem2  15689  iseraltlem3  15690  iseralt  15691  o1fsum  15819  cvgcmpce  15824  climcndslem1  15855  climcndslem2  15856  climcnds  15857  geomulcvg  15882  cvgrat  15889  mertenslem1  15890  fprodge1  15999  eftlub  16113  sin02gt0  16196  eirrlem  16208  bitsp1o  16435  2mulprm  16696  isprm5  16710  modprm0  16809  prmreclem3  16922  prmreclem4  16923  prmreclem5  16924  2expltfac  17097  metss2lem  24514  nlmvscnlem2  24696  nrginvrcnlem  24702  nmoco  24748  nmotri  24750  nghmcn  24756  icopnfhmeo  24962  nmoleub2lem3  25136  ipcau2  25256  tcphcphlem1  25257  ipcnlem2  25266  rrxcph  25414  csbren  25421  trirn  25422  pjthlem1  25459  opnmbllem  25624  vitalilem4  25634  itg1val2  25707  itg1cl  25708  itg1ge0  25709  itg1addlem4  25722  itg1addlem4OLD  25723  itg1mulc  25728  itg1ge0a  25735  itg1climres  25738  mbfi1fseqlem1  25739  mbfi1fseqlem3  25741  mbfi1fseqlem4  25742  mbfi1fseqlem5  25743  mbfi1fseqlem6  25744  itg2const2  25765  itg2mulclem  25770  itg2mulc  25771  itg2monolem1  25774  itg2monolem3  25776  itg2cnlem2  25786  iblconst  25841  iblmulc2  25854  itgmulc2lem1  25855  itgmulc2lem2  25856  bddmulibl  25862  bddiblnc  25865  dveflem  26005  cmvth  26017  cmvthOLD  26018  dvlip  26020  dvlipcn  26021  dvivthlem1  26035  lhop1lem  26040  dvcvx  26047  dvfsumlem2  26055  dvfsumlem2OLD  26056  dvfsumlem3  26057  dvfsumlem4  26058  dvfsum2  26063  ftc1lem4  26068  plyeq0lem  26240  aalioulem3  26365  aalioulem4  26366  aaliou3lem9  26381  ulmdvlem1  26432  itgulm  26440  radcnvlem1  26445  radcnvlem2  26446  dvradcnv  26453  abelthlem2  26465  abelthlem7  26471  tangtx  26536  tanregt0  26569  logdivlti  26650  logcnlem3  26674  logcnlem4  26675  logccv  26693  recxpcl  26705  cxpmul  26718  cxplt  26724  cxple2  26727  abscxpbnd  26784  lawcoslem1  26846  heron  26869  atans2  26962  efrlim  27000  efrlimOLD  27001  o1cxp  27006  scvxcvx  27017  jensenlem2  27019  amgmlem  27021  fsumharmonic  27043  lgamgulmlem2  27061  lgamgulmlem3  27062  lgamgulmlem4  27063  lgamgulmlem5  27064  lgamgulmlem6  27065  relgamcl  27093  ftalem1  27104  ftalem2  27105  ftalem5  27108  basellem3  27114  basellem8  27119  chpub  27252  logfacubnd  27253  logfaclbnd  27254  logfacbnd3  27255  logexprlim  27257  perfectlem2  27262  bclbnd  27312  efexple  27313  bposlem1  27316  bposlem2  27317  bposlem6  27321  bposlem9  27324  lgsdilem  27356  gausslemma2dlem0c  27390  gausslemma2dlem2  27399  gausslemma2dlem3  27400  gausslemma2dlem6  27404  lgseisenlem4  27410  lgseisen  27411  lgsquadlem1  27412  lgsquadlem2  27413  2lgslem1a1  27421  2sqmod  27468  chebbnd1lem1  27501  chebbnd1lem3  27503  chtppilimlem1  27505  chpchtlim  27511  vmadivsum  27514  rplogsumlem1  27516  rpvmasumlem  27519  dchrisumlem2  27522  dchrisumlem3  27523  dchrmusum2  27526  dchrvmasumlem2  27530  dchrvmasumiflem1  27533  dchrisum0re  27545  dchrisum0lem1  27548  dirith2  27560  mulogsumlem  27563  mulogsum  27564  mulog2sumlem2  27567  vmalogdivsum2  27570  vmalogdivsum  27571  2vmadivsumlem  27572  logsqvma  27574  logsqvma2  27575  log2sumbnd  27576  selberglem2  27578  selberg  27580  selbergb  27581  selberg2lem  27582  selberg2b  27584  chpdifbndlem1  27585  chpdifbndlem2  27586  selberg3lem1  27589  selberg3lem2  27590  selberg3  27591  selberg4lem1  27592  selberg4  27593  pntrsumbnd2  27599  selberg3r  27601  selberg4r  27602  selberg34r  27603  pntsf  27605  pntsval2  27608  pntrlog2bndlem1  27609  pntrlog2bndlem2  27610  pntrlog2bndlem3  27611  pntrlog2bndlem4  27612  pntrlog2bndlem5  27613  pntrlog2bndlem6  27615  pntrlog2bnd  27616  pntpbnd1a  27617  pntpbnd1  27618  pntpbnd2  27619  pntibndlem2a  27622  pntibndlem2  27623  pntlemb  27629  pntlemr  27634  pntlemj  27635  pntlemf  27637  pntlemk  27638  pntlemo  27639  pntlem3  27641  ostth2lem1  27650  ostth2lem2  27666  ostth2lem3  27667  ostth2lem4  27668  ostth3  27670  ttgcontlem1  28821  brbtwn2  28842  colinearalglem4  28846  axsegconlem8  28861  axsegconlem9  28862  axsegconlem10  28863  ax5seglem3  28868  axpaschlem  28877  axpasch  28878  axeuclidlem  28899  numclwwlk5  30324  numclwwlk7  30327  smcnlem  30633  ubthlem2  30807  htthlem  30853  pjhthlem1  31327  cnlnadjlem7  32009  nmopcoadji  32037  branmfn  32041  leopnmid  32074  rmulccn  33745  xrge0iifhom  33754  nexple  33844  dya2icoseg  34113  eulerpartlems  34196  eulerpartlemgc  34198  eulerpartlemb  34204  plymulx0  34395  signsvtp  34431  reprgt  34469  breprexplemc  34480  circlemethhgt  34491  hgt750lemd  34496  logdivsqrle  34498  hgt750lem  34499  hgt750lemf  34501  hgt750lemb  34504  hgt750lema  34505  hgt750leme  34506  tgoldbachgtde  34508  resconn  35076  knoppcnlem2  36199  knoppcnlem4  36201  knoppcnlem10  36207  unbdqndv2lem1  36214  unbdqndv2lem2  36215  knoppndvlem1  36217  knoppndvlem11  36227  knoppndvlem12  36228  knoppndvlem14  36230  knoppndvlem15  36231  knoppndvlem17  36233  knoppndvlem18  36234  knoppndvlem19  36235  knoppndvlem20  36236  knoppndvlem21  36237  opnmbllem0  37359  itg2addnclem2  37375  itg2addnclem3  37376  iblmulc2nc  37388  itgmulc2nclem1  37389  ftc1cnnclem  37394  ftc1anclem3  37398  areacirclem4  37414  geomcau  37462  equivbnd  37493  bfplem1  37525  bfplem2  37526  bfp  37527  rrnequiv  37538  rrntotbnd  37539  lcmineqlem19  41748  lcmineqlem20  41749  lcmineqlem21  41750  lcmineqlem22  41751  3lexlogpow2ineq2  41760  dvrelogpow2b  41769  aks4d1p1p2  41771  aks4d1p1p4  41772  aks4d1p1p6  41774  aks4d1p1p7  41775  aks4d1p1p5  41776  aks4d1p1  41777  aks4d1p8d2  41786  aks4d1p8  41788  posbezout  41800  aks6d1c2lem4  41827  2np3bcnp1  41844  2ap1caineq  41845  aks6d1c6lem4  41873  aks6d1c7lem1  41880  aks6d1c7lem2  41881  resubdi  42087  remul02  42096  remul01  42098  remulinvcom  42123  sn-0tie0  42130  renegmulnnass  42144  mulgt0con1d  42149  mulgt0con2d  42150  mulgt0b2d  42151  sn-ltmul2d  42152  sn-mulgt1d  42156  sn-inelr  42158  sn-itrere  42159  sn-retire  42160  fltnltalem  42332  fltnlta  42333  3cubeslem2  42360  3cubeslem3r  42362  3cubeslem4  42364  irrapxlem1  42497  irrapxlem2  42498  irrapxlem3  42499  irrapxlem4  42500  irrapxlem5  42501  pellexlem2  42505  pellexlem6  42509  pell14qrgt0  42534  pell1qrge1  42545  pell1qrgaplem  42548  pellqrexplicit  42552  pellqrex  42554  rmspecsqrtnq  42581  rmxycomplete  42593  rmxypos  42623  ltrmynn0  42624  ltrmxnn0  42625  jm2.24nn  42635  jm2.17a  42636  jm2.17b  42637  jm2.17c  42638  jm2.27c  42683  jm3.1lem2  42694  areaquad  42899  sqrtcval  43326  resqrtval  43328  imsqrtval  43329  imo72b2lem0  43850  cvgdvgrat  44005  nzprmdif  44011  lt3addmuld  44934  fperiodmullem  44936  fperiodmul  44937  lt4addmuld  44939  xralrple2  44987  xralrple3  45007  ltmulneg  45025  fmul01  45219  fmuldfeqlem1  45221  fmul01lt1lem1  45223  sumnnodd  45269  ltmod  45277  0ellimcdiv  45288  limclner  45290  dvdivbd  45562  dvbdfbdioolem2  45568  dvbdfbdioo  45569  ioodvbdlimc1lem1  45570  ioodvbdlimc1lem2  45571  ioodvbdlimc2lem  45573  stoweidlem1  45640  stoweidlem11  45650  stoweidlem13  45652  stoweidlem14  45653  stoweidlem16  45655  stoweidlem17  45656  stoweidlem22  45661  stoweidlem24  45663  stoweidlem25  45664  stoweidlem26  45665  stoweidlem30  45669  stoweidlem34  45673  stoweidlem36  45675  stoweidlem49  45688  stoweidlem59  45698  stoweidlem60  45699  wallispilem4  45707  wallispilem5  45708  wallispi  45709  wallispi2lem1  45710  wallispi2  45712  stirlinglem1  45713  stirlinglem3  45715  stirlinglem5  45717  stirlinglem6  45718  stirlinglem7  45719  stirlinglem10  45722  stirlinglem11  45723  stirlinglem12  45724  stirlinglem15  45727  stirlingr  45729  dirker2re  45731  dirkerval2  45733  dirkerre  45734  dirkertrigeqlem1  45737  dirkertrigeqlem2  45738  dirkeritg  45741  dirkercncflem2  45743  dirkercncflem4  45745  fourierdlem4  45750  fourierdlem5  45751  fourierdlem6  45752  fourierdlem7  45753  fourierdlem16  45762  fourierdlem18  45764  fourierdlem19  45765  fourierdlem21  45767  fourierdlem22  45768  fourierdlem26  45772  fourierdlem35  45781  fourierdlem39  45785  fourierdlem41  45787  fourierdlem42  45788  fourierdlem43  45789  fourierdlem48  45793  fourierdlem49  45794  fourierdlem51  45796  fourierdlem55  45800  fourierdlem56  45801  fourierdlem57  45802  fourierdlem58  45803  fourierdlem62  45807  fourierdlem63  45808  fourierdlem64  45809  fourierdlem65  45810  fourierdlem66  45811  fourierdlem67  45812  fourierdlem68  45813  fourierdlem71  45816  fourierdlem72  45817  fourierdlem73  45818  fourierdlem76  45821  fourierdlem77  45822  fourierdlem78  45823  fourierdlem83  45828  fourierdlem84  45829  fourierdlem87  45832  fourierdlem88  45833  fourierdlem89  45834  fourierdlem90  45835  fourierdlem91  45836  fourierdlem94  45839  fourierdlem95  45840  fourierdlem97  45842  fourierdlem103  45848  fourierdlem104  45849  fourierdlem112  45857  fourierdlem113  45858  sqwvfoura  45867  sqwvfourb  45868  fouriersw  45870  etransclem23  45896  etransclem48  45921  rrndistlt  45929  hoidmvlelem1  46234  hoidmvlelem2  46235  hoidmvlelem4  46237  smfmullem1  46430  smfmullem2  46431  smfmullem3  46432  smfmul  46434  fmtno4prmfac  47162  lighneallem4a  47198  requad01  47211  requad1  47212  requad2  47213  perfectALTVlem2  47312  ply1mulgsumlem2  47788  digvalnn0  48005  dignn0fr  48007  dig2nn0  48017  affinecomb1  48108  rrx2linest2  48150  line2  48158  itsclc0lem1  48162  itsclc0lem2  48163  itsclc0lem3  48164  itscnhlc0yqe  48165  itsclc0yqsollem2  48169  itsclc0yqsol  48170  itscnhlc0xyqsol  48171  itsclc0xyqsolr  48175  itsclinecirc0  48179  itsclinecirc0b  48180  itsclinecirc0in  48181  itsclquadb  48182  itsclquadeu  48183  2itscp  48187  itscnhlinecirc02plem1  48188  itscnhlinecirc02p  48191  inlinecirc02plem  48192  amgmwlem  48568