Theorem remulcld 11210

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7389  ℝcr 11073   · cmul 11079

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

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

This theorem is referenced by:  mulge0  11702  msqge0  11705  redivcl  11907  prodgt0  12035  ltmul1a  12037  ltmul1  12038  ltmuldiv  12062  lt2msq1  12073  lt2msq  12074  le2msq  12089  msq11  12090  supmul1  12158  supmullem2  12160  supmul  12161  div4p1lem1div2  12443  mul2lt0rlt0  13061  mul2lt0bi  13065  prodge0rd  13066  ge2halflem1  13074  qbtwnre  13165  xmulneg1  13235  xmulf  13238  lincmb01cmp  13462  iccf1o  13463  flmulnn0  13795  flhalf  13798  modcl  13841  mod0  13844  modge0  13847  modmulnn  13857  mulp1mod1  13882  muladdmod  13883  2txmodxeq0  13902  modaddmulmod  13909  moddi  13910  modsubdir  13911  modirr  13913  addmodlteq  13917  bernneq  14200  bernneq3  14202  expnbnd  14203  expmulnbnd  14206  discr1  14210  discr  14211  faclbnd  14261  faclbnd6  14270  remullem  15100  01sqrexlem7  15220  sqrtmul  15231  abstri  15303  sqreulem  15332  bhmafibid1  15440  mulcn2  15568  reccn2  15569  o1rlimmul  15591  lo1mul  15600  iseraltlem2  15655  iseraltlem3  15656  iseralt  15657  o1fsum  15785  cvgcmpce  15790  climcndslem1  15821  climcndslem2  15822  climcnds  15823  geomulcvg  15848  cvgrat  15855  mertenslem1  15856  fprodge1  15967  eftlub  16083  sin02gt0  16166  eirrlem  16178  bitsp1o  16409  2mulprm  16669  isprm5  16683  modprm0  16782  prmreclem3  16895  prmreclem4  16896  prmreclem5  16897  2expltfac  17069  metss2lem  24405  nlmvscnlem2  24579  nrginvrcnlem  24585  nmoco  24631  nmotri  24633  nghmcn  24639  icopnfhmeo  24847  nmoleub2lem3  25021  ipcau2  25140  tcphcphlem1  25141  ipcnlem2  25150  rrxcph  25298  csbren  25305  trirn  25306  pjthlem1  25343  opnmbllem  25508  vitalilem4  25518  itg1val2  25591  itg1cl  25592  itg1ge0  25593  itg1addlem4  25606  itg1mulc  25611  itg1ge0a  25618  itg1climres  25621  mbfi1fseqlem1  25622  mbfi1fseqlem3  25624  mbfi1fseqlem4  25625  mbfi1fseqlem5  25626  mbfi1fseqlem6  25627  itg2const2  25648  itg2mulclem  25653  itg2mulc  25654  itg2monolem1  25657  itg2monolem3  25659  itg2cnlem2  25669  iblconst  25725  iblmulc2  25738  itgmulc2lem1  25739  itgmulc2lem2  25740  bddmulibl  25746  bddiblnc  25749  dveflem  25889  cmvth  25901  cmvthOLD  25902  dvlip  25904  dvlipcn  25905  dvivthlem1  25919  lhop1lem  25924  dvcvx  25931  dvfsumlem2  25939  dvfsumlem2OLD  25940  dvfsumlem3  25941  dvfsumlem4  25942  dvfsum2  25947  ftc1lem4  25952  plyeq0lem  26121  aalioulem3  26248  aalioulem4  26249  aaliou3lem9  26264  ulmdvlem1  26315  itgulm  26323  radcnvlem1  26328  radcnvlem2  26329  dvradcnv  26336  abelthlem2  26348  abelthlem7  26354  tangtx  26420  tanregt0  26454  logdivlti  26535  logcnlem3  26559  logcnlem4  26560  logccv  26578  recxpcl  26590  cxpmul  26603  cxplt  26609  cxple2  26612  abscxpbnd  26669  lawcoslem1  26731  heron  26754  atans2  26847  efrlim  26885  efrlimOLD  26886  o1cxp  26891  scvxcvx  26902  jensenlem2  26904  amgmlem  26906  fsumharmonic  26928  lgamgulmlem2  26946  lgamgulmlem3  26947  lgamgulmlem4  26948  lgamgulmlem5  26949  lgamgulmlem6  26950  relgamcl  26978  ftalem1  26989  ftalem2  26990  ftalem5  26993  basellem3  26999  basellem8  27004  chpub  27137  logfacubnd  27138  logfaclbnd  27139  logfacbnd3  27140  logexprlim  27142  perfectlem2  27147  bclbnd  27197  efexple  27198  bposlem1  27201  bposlem2  27202  bposlem6  27206  bposlem9  27209  lgsdilem  27241  gausslemma2dlem0c  27275  gausslemma2dlem2  27284  gausslemma2dlem3  27285  gausslemma2dlem6  27289  lgseisenlem4  27295  lgseisen  27296  lgsquadlem1  27297  lgsquadlem2  27298  2lgslem1a1  27306  2sqmod  27353  chebbnd1lem1  27386  chebbnd1lem3  27388  chtppilimlem1  27390  chpchtlim  27396  vmadivsum  27399  rplogsumlem1  27401  rpvmasumlem  27404  dchrisumlem2  27407  dchrisumlem3  27408  dchrmusum2  27411  dchrvmasumlem2  27415  dchrvmasumiflem1  27418  dchrisum0re  27430  dchrisum0lem1  27433  dirith2  27445  mulogsumlem  27448  mulogsum  27449  mulog2sumlem2  27452  vmalogdivsum2  27455  vmalogdivsum  27456  2vmadivsumlem  27457  logsqvma  27459  logsqvma2  27460  log2sumbnd  27461  selberglem2  27463  selberg  27465  selbergb  27466  selberg2lem  27467  selberg2b  27469  chpdifbndlem1  27470  chpdifbndlem2  27471  selberg3lem1  27474  selberg3lem2  27475  selberg3  27476  selberg4lem1  27477  selberg4  27478  pntrsumbnd2  27484  selberg3r  27486  selberg4r  27487  selberg34r  27488  pntsf  27490  pntsval2  27493  pntrlog2bndlem1  27494  pntrlog2bndlem2  27495  pntrlog2bndlem3  27496  pntrlog2bndlem4  27497  pntrlog2bndlem5  27498  pntrlog2bndlem6  27500  pntrlog2bnd  27501  pntpbnd1a  27502  pntpbnd1  27503  pntpbnd2  27504  pntibndlem2a  27507  pntibndlem2  27508  pntlemb  27514  pntlemr  27519  pntlemj  27520  pntlemf  27522  pntlemk  27523  pntlemo  27524  pntlem3  27526  ostth2lem1  27535  ostth2lem2  27551  ostth2lem3  27552  ostth2lem4  27553  ostth3  27555  ttgcontlem1  28818  brbtwn2  28838  colinearalglem4  28842  axsegconlem8  28857  axsegconlem9  28858  axsegconlem10  28859  ax5seglem3  28864  axpaschlem  28873  axpasch  28874  axeuclidlem  28895  numclwwlk5  30323  numclwwlk7  30326  smcnlem  30632  ubthlem2  30806  htthlem  30852  pjhthlem1  31326  cnlnadjlem7  32008  nmopcoadji  32036  branmfn  32040  leopnmid  32073  nexple  32775  constrremulcl  33763  constrmulcl  33767  cos9thpiminplylem1  33778  cos9thpinconstrlem1  33785  rmulccn  33924  xrge0iifhom  33933  dya2icoseg  34274  eulerpartlems  34357  eulerpartlemgc  34359  eulerpartlemb  34365  plymulx0  34544  signsvtp  34580  reprgt  34618  breprexplemc  34629  circlemethhgt  34640  hgt750lemd  34645  logdivsqrle  34647  hgt750lem  34648  hgt750lemf  34650  hgt750lemb  34653  hgt750lema  34654  hgt750leme  34655  tgoldbachgtde  34657  resconn  35233  knoppcnlem2  36477  knoppcnlem4  36479  knoppcnlem10  36485  unbdqndv2lem1  36492  unbdqndv2lem2  36493  knoppndvlem1  36495  knoppndvlem11  36505  knoppndvlem12  36506  knoppndvlem14  36508  knoppndvlem15  36509  knoppndvlem17  36511  knoppndvlem18  36512  knoppndvlem19  36513  knoppndvlem20  36514  knoppndvlem21  36515  opnmbllem0  37645  itg2addnclem2  37661  itg2addnclem3  37662  iblmulc2nc  37674  itgmulc2nclem1  37675  ftc1cnnclem  37680  ftc1anclem3  37684  areacirclem4  37700  geomcau  37748  equivbnd  37779  bfplem1  37811  bfplem2  37812  bfp  37813  rrnequiv  37824  rrntotbnd  37825  lcmineqlem19  42030  lcmineqlem20  42031  lcmineqlem21  42032  lcmineqlem22  42033  3lexlogpow2ineq2  42042  dvrelogpow2b  42051  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p6  42056  aks4d1p1p7  42057  aks4d1p1p5  42058  aks4d1p1  42059  aks4d1p8d2  42068  aks4d1p8  42070  posbezout  42083  aks6d1c2lem4  42110  2np3bcnp1  42127  2ap1caineq  42128  aks6d1c6lem4  42156  aks6d1c7lem1  42163  aks6d1c7lem2  42164  resubdi  42379  remul02  42388  remul01  42390  remulinvcom  42416  rediveud  42426  redivcan3d  42430  sn-0tie0  42434  renegmulnnass  42448  mulgt0con1d  42453  mulgt0con2d  42454  mulgt0b1d  42455  sn-ltmul2d  42456  mulgt0b2d  42461  sn-mulgt1d  42462  mulltgt0d  42465  mullt0b1d  42466  mullt0b2d  42467  sn-inelr  42468  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  47563  lighneallem4a  47599  requad01  47612  requad1  47613  requad2  47614  perfectALTVlem2  47713  gpg3kgrtriexlem1  48064  gpg3kgrtriexlem4  48067  gpg3kgrtriexlem6  48069  ply1mulgsumlem2  48366  digvalnn0  48578  dignn0fr  48580  dig2nn0  48590  affinecomb1  48681  rrx2linest2  48723  line2  48731  itsclc0lem1  48735  itsclc0lem2  48736  itsclc0lem3  48737  itscnhlc0yqe  48738  itsclc0yqsollem2  48742  itsclc0yqsol  48743  itscnhlc0xyqsol  48744  itsclc0xyqsolr  48748  itsclinecirc0  48752  itsclinecirc0b  48753  itsclinecirc0in  48754  itsclquadb  48755  itsclquadeu  48756  2itscp  48760  itscnhlinecirc02plem1  48761  itscnhlinecirc02p  48764  inlinecirc02plem  48765  amgmwlem  49781