Theorem remulcld 11263

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126   · cmul 11132

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

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

This theorem is referenced by:  mulge0  11753  msqge0  11756  redivcl  11958  prodgt0  12086  ltmul1a  12088  ltmul1  12089  ltmuldiv  12113  lt2msq1  12124  lt2msq  12125  le2msq  12140  msq11  12141  supmul1  12209  supmullem2  12211  supmul  12212  div4p1lem1div2  12494  mul2lt0rlt0  13109  mul2lt0bi  13113  prodge0rd  13114  ge2halflem1  13122  qbtwnre  13213  xmulneg1  13283  xmulf  13286  lincmb01cmp  13510  iccf1o  13511  flmulnn0  13842  flhalf  13845  modcl  13888  mod0  13891  modge0  13894  modmulnn  13904  mulp1mod1  13927  muladdmod  13928  2txmodxeq0  13947  modaddmulmod  13954  moddi  13955  modsubdir  13956  modirr  13958  addmodlteq  13962  bernneq  14245  bernneq3  14247  expnbnd  14248  expmulnbnd  14251  discr1  14255  discr  14256  faclbnd  14306  faclbnd6  14315  remullem  15145  01sqrexlem7  15265  sqrtmul  15276  abstri  15347  sqreulem  15376  bhmafibid1  15482  mulcn2  15610  reccn2  15611  o1rlimmul  15633  lo1mul  15642  iseraltlem2  15697  iseraltlem3  15698  iseralt  15699  o1fsum  15827  cvgcmpce  15832  climcndslem1  15863  climcndslem2  15864  climcnds  15865  geomulcvg  15890  cvgrat  15897  mertenslem1  15898  fprodge1  16009  eftlub  16125  sin02gt0  16208  eirrlem  16220  bitsp1o  16450  2mulprm  16710  isprm5  16724  modprm0  16823  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  2expltfac  17110  metss2lem  24448  nlmvscnlem2  24622  nrginvrcnlem  24628  nmoco  24674  nmotri  24676  nghmcn  24682  icopnfhmeo  24890  nmoleub2lem3  25064  ipcau2  25184  tcphcphlem1  25185  ipcnlem2  25194  rrxcph  25342  csbren  25349  trirn  25350  pjthlem1  25387  opnmbllem  25552  vitalilem4  25562  itg1val2  25635  itg1cl  25636  itg1ge0  25637  itg1addlem4  25650  itg1mulc  25655  itg1ge0a  25662  itg1climres  25665  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  itg2const2  25692  itg2mulclem  25697  itg2mulc  25698  itg2monolem1  25701  itg2monolem3  25703  itg2cnlem2  25713  iblconst  25769  iblmulc2  25782  itgmulc2lem1  25783  itgmulc2lem2  25784  bddmulibl  25790  bddiblnc  25793  dveflem  25933  cmvth  25945  cmvthOLD  25946  dvlip  25948  dvlipcn  25949  dvivthlem1  25963  lhop1lem  25968  dvcvx  25975  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsum2  25991  ftc1lem4  25996  plyeq0lem  26165  aalioulem3  26292  aalioulem4  26293  aaliou3lem9  26308  ulmdvlem1  26359  itgulm  26367  radcnvlem1  26372  radcnvlem2  26373  dvradcnv  26380  abelthlem2  26392  abelthlem7  26398  tangtx  26464  tanregt0  26498  logdivlti  26579  logcnlem3  26603  logcnlem4  26604  logccv  26622  recxpcl  26634  cxpmul  26647  cxplt  26653  cxple2  26656  abscxpbnd  26713  lawcoslem1  26775  heron  26798  atans2  26891  efrlim  26929  efrlimOLD  26930  o1cxp  26935  scvxcvx  26946  jensenlem2  26948  amgmlem  26950  fsumharmonic  26972  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  relgamcl  27022  ftalem1  27033  ftalem2  27034  ftalem5  27037  basellem3  27043  basellem8  27048  chpub  27181  logfacubnd  27182  logfaclbnd  27183  logfacbnd3  27184  logexprlim  27186  perfectlem2  27191  bclbnd  27241  efexple  27242  bposlem1  27245  bposlem2  27246  bposlem6  27250  bposlem9  27253  lgsdilem  27285  gausslemma2dlem0c  27319  gausslemma2dlem2  27328  gausslemma2dlem3  27329  gausslemma2dlem6  27333  lgseisenlem4  27339  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  2lgslem1a1  27350  2sqmod  27397  chebbnd1lem1  27430  chebbnd1lem3  27432  chtppilimlem1  27434  chpchtlim  27440  vmadivsum  27443  rplogsumlem1  27445  rpvmasumlem  27448  dchrisumlem2  27451  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  dchrisum0re  27474  dchrisum0lem1  27477  dirith2  27489  mulogsumlem  27492  mulogsum  27493  mulog2sumlem2  27496  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  logsqvma  27503  logsqvma2  27504  log2sumbnd  27505  selberglem2  27507  selberg  27509  selbergb  27510  selberg2lem  27511  selberg2b  27513  chpdifbndlem1  27514  chpdifbndlem2  27515  selberg3lem1  27518  selberg3lem2  27519  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrsumbnd2  27528  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntsf  27534  pntsval2  27537  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntibndlem2a  27551  pntibndlem2  27552  pntlemb  27558  pntlemr  27563  pntlemj  27564  pntlemf  27566  pntlemk  27567  pntlemo  27568  pntlem3  27570  ostth2lem1  27579  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth3  27599  ttgcontlem1  28810  brbtwn2  28830  colinearalglem4  28834  axsegconlem8  28849  axsegconlem9  28850  axsegconlem10  28851  ax5seglem3  28856  axpaschlem  28865  axpasch  28866  axeuclidlem  28887  numclwwlk5  30315  numclwwlk7  30318  smcnlem  30624  ubthlem2  30798  htthlem  30844  pjhthlem1  31318  cnlnadjlem7  32000  nmopcoadji  32028  branmfn  32032  leopnmid  32065  nexple  32769  constrremulcl  33747  constrmulcl  33751  cos9thpiminplylem1  33762  cos9thpinconstrlem1  33769  rmulccn  33905  xrge0iifhom  33914  dya2icoseg  34255  eulerpartlems  34338  eulerpartlemgc  34340  eulerpartlemb  34346  plymulx0  34525  signsvtp  34561  reprgt  34599  breprexplemc  34610  circlemethhgt  34621  hgt750lemd  34626  logdivsqrle  34628  hgt750lem  34629  hgt750lemf  34631  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  tgoldbachgtde  34638  resconn  35214  knoppcnlem2  36458  knoppcnlem4  36460  knoppcnlem10  36466  unbdqndv2lem1  36473  unbdqndv2lem2  36474  knoppndvlem1  36476  knoppndvlem11  36486  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem18  36493  knoppndvlem19  36494  knoppndvlem20  36495  knoppndvlem21  36496  opnmbllem0  37626  itg2addnclem2  37642  itg2addnclem3  37643  iblmulc2nc  37655  itgmulc2nclem1  37656  ftc1cnnclem  37661  ftc1anclem3  37665  areacirclem4  37681  geomcau  37729  equivbnd  37760  bfplem1  37792  bfplem2  37793  bfp  37794  rrnequiv  37805  rrntotbnd  37806  lcmineqlem19  42006  lcmineqlem20  42007  lcmineqlem21  42008  lcmineqlem22  42009  3lexlogpow2ineq2  42018  dvrelogpow2b  42027  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p8d2  42044  aks4d1p8  42046  posbezout  42059  aks6d1c2lem4  42086  2np3bcnp1  42103  2ap1caineq  42104  aks6d1c6lem4  42132  aks6d1c7lem1  42139  aks6d1c7lem2  42140  resubdi  42386  remul02  42395  remul01  42397  remulinvcom  42422  sn-0tie0  42429  renegmulnnass  42443  mulgt0con1d  42448  mulgt0con2d  42449  mulgt0b2d  42450  sn-ltmul2d  42451  sn-mulgt1d  42455  sn-inelr  42457  sn-itrere  42458  sn-retire  42459  fltnltalem  42632  fltnlta  42633  3cubeslem2  42655  3cubeslem3r  42657  3cubeslem4  42659  irrapxlem1  42792  irrapxlem2  42793  irrapxlem3  42794  irrapxlem4  42795  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  pell14qrgt0  42829  pell1qrge1  42840  pell1qrgaplem  42843  pellqrexplicit  42847  pellqrex  42849  rmspecsqrtnq  42876  rmxycomplete  42888  rmxypos  42918  ltrmynn0  42919  ltrmxnn0  42920  jm2.24nn  42930  jm2.17a  42931  jm2.17b  42932  jm2.17c  42933  jm2.27c  42978  jm3.1lem2  42989  areaquad  43187  sqrtcval  43612  resqrtval  43614  imsqrtval  43615  imo72b2lem0  44136  cvgdvgrat  44285  nzprmdif  44291  lt3addmuld  45278  fperiodmullem  45280  fperiodmul  45281  lt4addmuld  45283  xralrple2  45329  xralrple3  45349  ltmulneg  45367  fmul01  45557  fmuldfeqlem1  45559  fmul01lt1lem1  45561  sumnnodd  45607  ltmod  45615  0ellimcdiv  45626  limclner  45628  dvdivbd  45900  dvbdfbdioolem2  45906  dvbdfbdioo  45907  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweidlem1  45978  stoweidlem11  45988  stoweidlem13  45990  stoweidlem14  45991  stoweidlem16  45993  stoweidlem17  45994  stoweidlem22  45999  stoweidlem24  46001  stoweidlem25  46002  stoweidlem26  46003  stoweidlem30  46007  stoweidlem34  46011  stoweidlem36  46013  stoweidlem49  46026  stoweidlem59  46036  stoweidlem60  46037  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem15  46065  stirlingr  46067  dirker2re  46069  dirkerval2  46071  dirkerre  46072  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem4  46088  fourierdlem5  46089  fourierdlem6  46090  fourierdlem7  46091  fourierdlem16  46100  fourierdlem18  46102  fourierdlem19  46103  fourierdlem21  46105  fourierdlem22  46106  fourierdlem26  46110  fourierdlem35  46119  fourierdlem39  46123  fourierdlem41  46125  fourierdlem42  46126  fourierdlem43  46127  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem55  46138  fourierdlem56  46139  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem66  46149  fourierdlem67  46150  fourierdlem68  46151  fourierdlem71  46154  fourierdlem72  46155  fourierdlem73  46156  fourierdlem76  46159  fourierdlem77  46160  fourierdlem78  46161  fourierdlem83  46166  fourierdlem84  46167  fourierdlem87  46170  fourierdlem88  46171  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem94  46177  fourierdlem95  46178  fourierdlem97  46180  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem113  46196  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  etransclem23  46234  etransclem48  46259  rrndistlt  46267  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem4  46575  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  smfmul  46772  fmtno4prmfac  47534  lighneallem4a  47570  requad01  47583  requad1  47584  requad2  47585  perfectALTVlem2  47684  gpg3kgrtriexlem1  48033  gpg3kgrtriexlem4  48036  gpg3kgrtriexlem6  48038  ply1mulgsumlem2  48311  digvalnn0  48527  dignn0fr  48529  dig2nn0  48539  affinecomb1  48630  rrx2linest2  48672  line2  48680  itsclc0lem1  48684  itsclc0lem2  48685  itsclc0lem3  48686  itscnhlc0yqe  48687  itsclc0yqsollem2  48691  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itsclc0xyqsolr  48697  itsclinecirc0  48701  itsclinecirc0b  48702  itsclinecirc0in  48703  itsclquadb  48704  itsclquadeu  48705  2itscp  48709  itscnhlinecirc02plem1  48710  itscnhlinecirc02p  48713  inlinecirc02plem  48714  amgmwlem  49614