Theorem remulcld 11180

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043   · cmul 11049

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mulge0  11672  msqge0  11675  redivcl  11877  prodgt0  12005  ltmul1a  12007  ltmul1  12008  ltmuldiv  12032  lt2msq1  12043  lt2msq  12044  le2msq  12059  msq11  12060  supmul1  12128  supmullem2  12130  supmul  12131  div4p1lem1div2  12413  mul2lt0rlt0  13031  mul2lt0bi  13035  prodge0rd  13036  ge2halflem1  13044  qbtwnre  13135  xmulneg1  13205  xmulf  13208  lincmb01cmp  13432  iccf1o  13433  flmulnn0  13765  flhalf  13768  modcl  13811  mod0  13814  modge0  13817  modmulnn  13827  mulp1mod1  13852  muladdmod  13853  2txmodxeq0  13872  modaddmulmod  13879  moddi  13880  modsubdir  13881  modirr  13883  addmodlteq  13887  bernneq  14170  bernneq3  14172  expnbnd  14173  expmulnbnd  14176  discr1  14180  discr  14181  faclbnd  14231  faclbnd6  14240  remullem  15070  01sqrexlem7  15190  sqrtmul  15201  abstri  15273  sqreulem  15302  bhmafibid1  15410  mulcn2  15538  reccn2  15539  o1rlimmul  15561  lo1mul  15570  iseraltlem2  15625  iseraltlem3  15626  iseralt  15627  o1fsum  15755  cvgcmpce  15760  climcndslem1  15791  climcndslem2  15792  climcnds  15793  geomulcvg  15818  cvgrat  15825  mertenslem1  15826  fprodge1  15937  eftlub  16053  sin02gt0  16136  eirrlem  16148  bitsp1o  16379  2mulprm  16639  isprm5  16653  modprm0  16752  prmreclem3  16865  prmreclem4  16866  prmreclem5  16867  2expltfac  17039  metss2lem  24432  nlmvscnlem2  24606  nrginvrcnlem  24612  nmoco  24658  nmotri  24660  nghmcn  24666  icopnfhmeo  24874  nmoleub2lem3  25048  ipcau2  25167  tcphcphlem1  25168  ipcnlem2  25177  rrxcph  25325  csbren  25332  trirn  25333  pjthlem1  25370  opnmbllem  25535  vitalilem4  25545  itg1val2  25618  itg1cl  25619  itg1ge0  25620  itg1addlem4  25633  itg1mulc  25638  itg1ge0a  25645  itg1climres  25648  mbfi1fseqlem1  25649  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  mbfi1fseqlem6  25654  itg2const2  25675  itg2mulclem  25680  itg2mulc  25681  itg2monolem1  25684  itg2monolem3  25686  itg2cnlem2  25696  iblconst  25752  iblmulc2  25765  itgmulc2lem1  25766  itgmulc2lem2  25767  bddmulibl  25773  bddiblnc  25776  dveflem  25916  cmvth  25928  cmvthOLD  25929  dvlip  25931  dvlipcn  25932  dvivthlem1  25946  lhop1lem  25951  dvcvx  25958  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsum2  25974  ftc1lem4  25979  plyeq0lem  26148  aalioulem3  26275  aalioulem4  26276  aaliou3lem9  26291  ulmdvlem1  26342  itgulm  26350  radcnvlem1  26355  radcnvlem2  26356  dvradcnv  26363  abelthlem2  26375  abelthlem7  26381  tangtx  26447  tanregt0  26481  logdivlti  26562  logcnlem3  26586  logcnlem4  26587  logccv  26605  recxpcl  26617  cxpmul  26630  cxplt  26636  cxple2  26639  abscxpbnd  26696  lawcoslem1  26758  heron  26781  atans2  26874  efrlim  26912  efrlimOLD  26913  o1cxp  26918  scvxcvx  26929  jensenlem2  26931  amgmlem  26933  fsumharmonic  26955  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem4  26975  lgamgulmlem5  26976  lgamgulmlem6  26977  relgamcl  27005  ftalem1  27016  ftalem2  27017  ftalem5  27020  basellem3  27026  basellem8  27031  chpub  27164  logfacubnd  27165  logfaclbnd  27166  logfacbnd3  27167  logexprlim  27169  perfectlem2  27174  bclbnd  27224  efexple  27225  bposlem1  27228  bposlem2  27229  bposlem6  27233  bposlem9  27236  lgsdilem  27268  gausslemma2dlem0c  27302  gausslemma2dlem2  27311  gausslemma2dlem3  27312  gausslemma2dlem6  27316  lgseisenlem4  27322  lgseisen  27323  lgsquadlem1  27324  lgsquadlem2  27325  2lgslem1a1  27333  2sqmod  27380  chebbnd1lem1  27413  chebbnd1lem3  27415  chtppilimlem1  27417  chpchtlim  27423  vmadivsum  27426  rplogsumlem1  27428  rpvmasumlem  27431  dchrisumlem2  27434  dchrisumlem3  27435  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumiflem1  27445  dchrisum0re  27457  dchrisum0lem1  27460  dirith2  27472  mulogsumlem  27475  mulogsum  27476  mulog2sumlem2  27479  vmalogdivsum2  27482  vmalogdivsum  27483  2vmadivsumlem  27484  logsqvma  27486  logsqvma2  27487  log2sumbnd  27488  selberglem2  27490  selberg  27492  selbergb  27493  selberg2lem  27494  selberg2b  27496  chpdifbndlem1  27497  chpdifbndlem2  27498  selberg3lem1  27501  selberg3lem2  27502  selberg3  27503  selberg4lem1  27504  selberg4  27505  pntrsumbnd2  27511  selberg3r  27513  selberg4r  27514  selberg34r  27515  pntsf  27517  pntsval2  27520  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem2a  27534  pntibndlem2  27535  pntlemb  27541  pntlemr  27546  pntlemj  27547  pntlemf  27549  pntlemk  27550  pntlemo  27551  pntlem3  27553  ostth2lem1  27562  ostth2lem2  27578  ostth2lem3  27579  ostth2lem4  27580  ostth3  27582  ttgcontlem1  28865  brbtwn2  28885  colinearalglem4  28889  axsegconlem8  28904  axsegconlem9  28905  axsegconlem10  28906  ax5seglem3  28911  axpaschlem  28920  axpasch  28921  axeuclidlem  28942  numclwwlk5  30367  numclwwlk7  30370  smcnlem  30676  ubthlem2  30850  htthlem  30896  pjhthlem1  31370  cnlnadjlem7  32052  nmopcoadji  32080  branmfn  32084  leopnmid  32117  nexple  32819  constrremulcl  33750  constrmulcl  33754  cos9thpiminplylem1  33765  cos9thpinconstrlem1  33772  rmulccn  33911  xrge0iifhom  33920  dya2icoseg  34261  eulerpartlems  34344  eulerpartlemgc  34346  eulerpartlemb  34352  plymulx0  34531  signsvtp  34567  reprgt  34605  breprexplemc  34616  circlemethhgt  34627  hgt750lemd  34632  logdivsqrle  34634  hgt750lem  34635  hgt750lemf  34637  hgt750lemb  34640  hgt750lema  34641  hgt750leme  34642  tgoldbachgtde  34644  resconn  35226  knoppcnlem2  36475  knoppcnlem4  36477  knoppcnlem10  36483  unbdqndv2lem1  36490  unbdqndv2lem2  36491  knoppndvlem1  36493  knoppndvlem11  36503  knoppndvlem12  36504  knoppndvlem14  36506  knoppndvlem15  36507  knoppndvlem17  36509  knoppndvlem18  36510  knoppndvlem19  36511  knoppndvlem20  36512  knoppndvlem21  36513  opnmbllem0  37643  itg2addnclem2  37659  itg2addnclem3  37660  iblmulc2nc  37672  itgmulc2nclem1  37673  ftc1cnnclem  37678  ftc1anclem3  37682  areacirclem4  37698  geomcau  37746  equivbnd  37777  bfplem1  37809  bfplem2  37810  bfp  37811  rrnequiv  37822  rrntotbnd  37823  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem21  42030  lcmineqlem22  42031  3lexlogpow2ineq2  42040  dvrelogpow2b  42049  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p8d2  42066  aks4d1p8  42068  posbezout  42081  aks6d1c2lem4  42108  2np3bcnp1  42125  2ap1caineq  42126  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7lem2  42162  resubdi  42377  remul02  42386  remul01  42388  remulinvcom  42414  rediveud  42424  redivcan3d  42428  sn-0tie0  42432  renegmulnnass  42446  mulgt0con1d  42451  mulgt0con2d  42452  mulgt0b1d  42453  sn-ltmul2d  42454  mulgt0b2d  42459  sn-mulgt1d  42460  mulltgt0d  42463  mullt0b1d  42464  mullt0b2d  42465  sn-mullt0d  42466  sn-itrere  42469  sn-retire  42470  fltnltalem  42643  fltnlta  42644  3cubeslem2  42666  3cubeslem3r  42668  3cubeslem4  42670  irrapxlem1  42803  irrapxlem2  42804  irrapxlem3  42805  irrapxlem4  42806  irrapxlem5  42807  pellexlem2  42811  pellexlem6  42815  pell14qrgt0  42840  pell1qrge1  42851  pell1qrgaplem  42854  pellqrexplicit  42858  pellqrex  42860  rmspecsqrtnq  42887  rmxycomplete  42899  rmxypos  42929  ltrmynn0  42930  ltrmxnn0  42931  jm2.24nn  42941  jm2.17a  42942  jm2.17b  42943  jm2.17c  42944  jm2.27c  42989  jm3.1lem2  43000  areaquad  43198  sqrtcval  43623  resqrtval  43625  imsqrtval  43626  imo72b2lem0  44147  cvgdvgrat  44295  nzprmdif  44301  lt3addmuld  45292  fperiodmullem  45294  fperiodmul  45295  lt4addmuld  45297  xralrple2  45343  xralrple3  45363  ltmulneg  45381  fmul01  45571  fmuldfeqlem1  45573  fmul01lt1lem1  45575  sumnnodd  45621  ltmod  45629  0ellimcdiv  45640  limclner  45642  dvdivbd  45914  dvbdfbdioolem2  45920  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem1  45992  stoweidlem11  46002  stoweidlem13  46004  stoweidlem14  46005  stoweidlem16  46007  stoweidlem17  46008  stoweidlem22  46013  stoweidlem24  46015  stoweidlem25  46016  stoweidlem26  46017  stoweidlem30  46021  stoweidlem34  46025  stoweidlem36  46027  stoweidlem49  46040  stoweidlem59  46050  stoweidlem60  46051  wallispilem4  46059  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  wallispi2  46064  stirlinglem1  46065  stirlinglem3  46067  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem10  46074  stirlinglem11  46075  stirlinglem12  46076  stirlinglem15  46079  stirlingr  46081  dirker2re  46083  dirkerval2  46085  dirkerre  46086  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkeritg  46093  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem4  46102  fourierdlem5  46103  fourierdlem6  46104  fourierdlem7  46105  fourierdlem16  46114  fourierdlem18  46116  fourierdlem19  46117  fourierdlem21  46119  fourierdlem22  46120  fourierdlem26  46124  fourierdlem35  46133  fourierdlem39  46137  fourierdlem41  46139  fourierdlem42  46140  fourierdlem43  46141  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem55  46152  fourierdlem56  46153  fourierdlem57  46154  fourierdlem58  46155  fourierdlem62  46159  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem66  46163  fourierdlem67  46164  fourierdlem68  46165  fourierdlem71  46168  fourierdlem72  46169  fourierdlem73  46170  fourierdlem76  46173  fourierdlem77  46174  fourierdlem78  46175  fourierdlem83  46180  fourierdlem84  46181  fourierdlem87  46184  fourierdlem88  46185  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem94  46191  fourierdlem95  46192  fourierdlem97  46194  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  fourierdlem113  46210  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  etransclem23  46248  etransclem48  46273  rrndistlt  46281  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem4  46589  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  smfmul  46786  fmtno4prmfac  47566  lighneallem4a  47602  requad01  47615  requad1  47616  requad2  47617  perfectALTVlem2  47716  gpg3kgrtriexlem1  48067  gpg3kgrtriexlem4  48070  gpg3kgrtriexlem6  48072  ply1mulgsumlem2  48369  digvalnn0  48581  dignn0fr  48583  dig2nn0  48593  affinecomb1  48684  rrx2linest2  48726  line2  48734  itsclc0lem1  48738  itsclc0lem2  48739  itsclc0lem3  48740  itscnhlc0yqe  48741  itsclc0yqsollem2  48745  itsclc0yqsol  48746  itscnhlc0xyqsol  48747  itsclc0xyqsolr  48751  itsclinecirc0  48755  itsclinecirc0b  48756  itsclinecirc0in  48757  itsclquadb  48758  itsclquadeu  48759  2itscp  48763  itscnhlinecirc02plem1  48764  itscnhlinecirc02p  48767  inlinecirc02plem  48768  amgmwlem  49784