Theorem remulcld 9949

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

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814   · cmul 9820

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  mulge0  10425  msqge0  10428  redivcl  10623  prodgt0  10747  prodge0  10749  ltmul1a  10751  ltmul1  10752  ltmuldiv  10775  lt2msq1  10786  lt2msq  10787  le2msq  10802  msq11  10803  supmul1  10869  supmullem2  10871  supmul  10872  div4p1lem1div2  11164  mul2lt0rlt0  11808  mul2lt0bi  11812  qbtwnre  11904  xmulneg1  11971  xmulf  11974  lincmb01cmp  12186  iccf1o  12187  flmulnn0  12490  flhalf  12493  modcl  12534  mod0  12537  modge0  12540  modmulnn  12550  mulp1mod1  12573  2txmodxeq0  12592  modaddmulmod  12599  moddi  12600  modsubdir  12601  modirr  12603  addmodlteq  12607  bernneq  12852  bernneq3  12854  expnbnd  12855  expmulnbnd  12858  discr1  12862  discr  12863  faclbnd  12939  faclbnd6  12948  remullem  13716  sqrlem7  13837  sqrtmul  13848  abstri  13918  sqreulem  13947  mulcn2  14174  reccn2  14175  o1rlimmul  14197  lo1mul  14206  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  o1fsum  14386  cvgcmpce  14391  climcndslem1  14420  climcndslem2  14421  climcnds  14422  geomulcvg  14446  cvgrat  14454  mertenslem1  14455  fprodge1  14565  eftlub  14678  sin02gt0  14761  eirrlem  14771  bitsp1o  14993  isprm5  15257  modprm0  15348  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  2expltfac  15637  metss2lem  22126  nlmvscnlem2  22299  nrginvrcnlem  22305  nmoco  22351  nmotri  22353  nghmcn  22359  icopnfhmeo  22550  nmoleub2lem3  22723  ipcau2  22841  tchcphlem1  22842  ipcnlem2  22851  rrxcph  22988  csbren  22990  trirn  22991  pjthlem1  23016  opnmbllem  23175  vitalilem4  23186  itg1val2  23257  itg1cl  23258  itg1ge0  23259  itg1addlem4  23272  itg1mulc  23277  itg1ge0a  23284  itg1climres  23287  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2const2  23314  itg2mulclem  23319  itg2mulc  23320  itg2monolem1  23323  itg2monolem3  23325  itg2cnlem2  23335  iblconst  23390  iblmulc2  23403  itgmulc2lem1  23404  itgmulc2lem2  23405  bddmulibl  23411  dveflem  23546  cmvth  23558  dvlip  23560  dvlipcn  23561  dvivthlem1  23575  lhop1lem  23580  dvcvx  23587  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsum2  23601  ftc1lem4  23606  plyeq0lem  23770  aalioulem3  23893  aalioulem4  23894  aaliou3lem9  23909  ulmdvlem1  23958  itgulm  23966  radcnvlem1  23971  radcnvlem2  23972  dvradcnv  23979  abelthlem2  23990  abelthlem7  23996  tangtx  24061  tanregt0  24089  logdivlti  24170  logcnlem3  24190  logcnlem4  24191  logccv  24209  recxpcl  24221  cxpmul  24234  cxplt  24240  cxple2  24243  abscxpbnd  24294  lawcoslem1  24345  heron  24365  atans2  24458  efrlim  24496  o1cxp  24501  scvxcvx  24512  jensenlem2  24514  amgmlem  24516  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  relgamcl  24588  ftalem1  24599  ftalem2  24600  ftalem5  24603  basellem3  24609  basellem8  24614  chpub  24745  logfacubnd  24746  logfaclbnd  24747  logfacbnd3  24748  logexprlim  24750  perfectlem2  24755  bclbnd  24805  efexple  24806  bposlem1  24809  bposlem2  24810  bposlem6  24814  bposlem9  24817  lgsdilem  24849  gausslemma2dlem0c  24883  gausslemma2dlem2  24892  gausslemma2dlem3  24893  gausslemma2dlem6  24897  lgseisenlem4  24903  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1a1  24914  chebbnd1lem1  24958  chebbnd1lem3  24960  chtppilimlem1  24962  chpchtlim  24968  vmadivsum  24971  rplogsumlem1  24973  rpvmasumlem  24976  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0re  25002  dchrisum0lem1  25005  dirith2  25017  mulogsumlem  25020  mulogsum  25021  mulog2sumlem2  25024  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  logsqvma  25031  logsqvma2  25032  log2sumbnd  25033  selberglem2  25035  selberg  25037  selbergb  25038  selberg2lem  25039  selberg2b  25041  chpdifbndlem1  25042  chpdifbndlem2  25043  selberg3lem1  25046  selberg3lem2  25047  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrsumbnd2  25056  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntsf  25062  pntsval2  25065  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2a  25079  pntibndlem2  25080  pntlemb  25086  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntlem3  25098  ostth2lem1  25107  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth3  25127  ttgcontlem1  25565  brbtwn2  25585  colinearalglem4  25589  axsegconlem8  25604  axsegconlem9  25605  axsegconlem10  25606  ax5seglem3  25611  axpaschlem  25620  axpasch  25621  axeuclidlem  25642  numclwwlk5  26639  numclwwlk7  26641  smcnlem  26936  ubthlem2  27111  htthlem  27158  pjhthlem1  27634  cnlnadjlem7  28316  nmopcoadji  28344  branmfn  28348  leopnmid  28381  bhmafibid1  28975  2sqmod  28979  rmulccn  29302  xrge0iifhom  29311  nexple  29399  dya2icoseg  29666  eulerpartlems  29749  eulerpartlemgc  29751  eulerpartlemb  29757  plymulx0  29950  signsvtp  29986  rescon  30482  knoppcnlem2  31654  knoppcnlem4  31656  knoppcnlem10  31662  unbdqndv2lem1  31670  unbdqndv2lem2  31671  knoppndvlem1  31673  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem18  31690  knoppndvlem19  31691  knoppndvlem20  31692  knoppndvlem21  31693  opnmbllem0  32615  itg2addnclem2  32632  itg2addnclem3  32633  iblmulc2nc  32645  itgmulc2nclem1  32646  bddiblnc  32650  ftc1cnnclem  32653  ftc1anclem3  32657  areacirclem4  32673  geomcau  32725  equivbnd  32759  bfplem1  32791  bfplem2  32792  bfp  32793  rrnequiv  32804  rrntotbnd  32805  irrapxlem1  36404  irrapxlem2  36405  irrapxlem3  36406  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  pell14qrgt0  36441  pell1qrge1  36452  pell1qrgaplem  36455  pellqrexplicit  36459  pellqrex  36461  rmspecsqrtnq  36488  rmxycomplete  36500  rmxypos  36532  ltrmynn0  36533  ltrmxnn0  36534  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  jm2.27c  36592  jm3.1lem2  36603  areaquad  36821  imo72b2lem0  37487  cvgdvgrat  37534  nzprmdif  37540  lt3addmuld  38456  fperiodmullem  38458  fperiodmul  38459  lt4addmuld  38461  xralrple2  38511  xralrple3  38531  ltmulneg  38556  fmul01  38647  fmuldfeqlem1  38649  fmul01lt1lem1  38651  sumnnodd  38697  ltmod  38705  0ellimcdiv  38716  limclner  38718  dvdivbd  38813  dvbdfbdioolem2  38819  dvbdfbdioo  38820  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem1  38894  stoweidlem11  38904  stoweidlem13  38906  stoweidlem14  38907  stoweidlem16  38909  stoweidlem17  38910  stoweidlem22  38915  stoweidlem24  38917  stoweidlem25  38918  stoweidlem26  38919  stoweidlem30  38923  stoweidlem34  38927  stoweidlem36  38929  stoweidlem49  38942  stoweidlem59  38952  stoweidlem60  38953  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem15  38981  stirlingr  38983  dirker2re  38985  dirkerval2  38987  dirkerre  38988  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem4  39004  fourierdlem5  39005  fourierdlem6  39006  fourierdlem7  39007  fourierdlem16  39016  fourierdlem18  39018  fourierdlem19  39019  fourierdlem21  39021  fourierdlem22  39022  fourierdlem26  39026  fourierdlem35  39035  fourierdlem39  39039  fourierdlem41  39041  fourierdlem42  39042  fourierdlem43  39043  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem55  39054  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem66  39065  fourierdlem67  39066  fourierdlem68  39067  fourierdlem71  39070  fourierdlem72  39071  fourierdlem73  39072  fourierdlem76  39075  fourierdlem77  39076  fourierdlem78  39077  fourierdlem83  39082  fourierdlem84  39083  fourierdlem87  39086  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem94  39093  fourierdlem95  39094  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem23  39150  etransclem48  39175  rrndistlt  39186  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem4  39488  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  smfmul  39680  fmtno4prmfac  40022  lighneallem4a  40063  perfectALTVlem2  40165  av-numclwwlk5  41542  av-numclwwlk7  41545  ply1mulgsumlem2  41969  digvalnn0  42191  dignn0fr  42193  dig2nn0  42203  amgmwlem  42357