Theorem remulcld 10355

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

Syntax hints:   → wi 4   ∈ wcel 2156  (class class class)co 6874  ℝcr 10220   · cmul 10226

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

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

This theorem is referenced by:  mulge0  10831  msqge0  10834  redivcl  11029  prodgt0  11153  prodge0OLD  11155  ltmul1a  11157  ltmul1  11158  ltmuldiv  11181  lt2msq1  11192  lt2msq  11193  le2msq  11208  msq11  11209  supmul1  11277  supmullem2  11279  supmul  11280  div4p1lem1div2  11554  mul2lt0rlt0  12146  mul2lt0bi  12150  prodge0rd  12151  qbtwnre  12248  xmulneg1  12317  xmulf  12320  lincmb01cmp  12538  iccf1o  12539  flmulnn0  12852  flhalf  12855  modcl  12896  mod0  12899  modge0  12902  modmulnn  12912  mulp1mod1  12935  2txmodxeq0  12954  modaddmulmod  12961  moddi  12962  modsubdir  12963  modirr  12965  addmodlteq  12969  bernneq  13213  bernneq3  13215  expnbnd  13216  expmulnbnd  13219  discr1  13223  discr  13224  faclbnd  13297  faclbnd6  13306  remullem  14091  sqrlem7  14212  sqrtmul  14223  abstri  14293  sqreulem  14322  mulcn2  14549  reccn2  14550  o1rlimmul  14572  lo1mul  14581  iseraltlem2  14636  iseraltlem3  14637  iseralt  14638  o1fsum  14767  cvgcmpce  14772  climcndslem1  14803  climcndslem2  14804  climcnds  14805  geomulcvg  14829  cvgrat  14836  mertenslem1  14837  fprodge1  14946  eftlub  15059  sin02gt0  15142  eirrlem  15152  bitsp1o  15374  isprm5  15636  modprm0  15727  prmreclem3  15839  prmreclem4  15840  prmreclem5  15841  2expltfac  16011  metss2lem  22529  nlmvscnlem2  22702  nrginvrcnlem  22708  nmoco  22754  nmotri  22756  nghmcn  22762  icopnfhmeo  22955  nmoleub2lem3  23127  ipcau2  23245  tchcphlem1  23246  ipcnlem2  23255  rrxcph  23392  csbren  23394  trirn  23395  pjthlem1  23420  opnmbllem  23582  vitalilem4  23592  itg1val2  23665  itg1cl  23666  itg1ge0  23667  itg1addlem4  23680  itg1mulc  23685  itg1ge0a  23692  itg1climres  23695  mbfi1fseqlem1  23696  mbfi1fseqlem3  23698  mbfi1fseqlem4  23699  mbfi1fseqlem5  23700  mbfi1fseqlem6  23701  itg2const2  23722  itg2mulclem  23727  itg2mulc  23728  itg2monolem1  23731  itg2monolem3  23733  itg2cnlem2  23743  iblconst  23798  iblmulc2  23811  itgmulc2lem1  23812  itgmulc2lem2  23813  bddmulibl  23819  dveflem  23956  cmvth  23968  dvlip  23970  dvlipcn  23971  dvivthlem1  23985  lhop1lem  23990  dvcvx  23997  dvfsumlem2  24004  dvfsumlem3  24005  dvfsumlem4  24006  dvfsum2  24011  ftc1lem4  24016  plyeq0lem  24180  aalioulem3  24303  aalioulem4  24304  aaliou3lem9  24319  ulmdvlem1  24368  itgulm  24376  radcnvlem1  24381  radcnvlem2  24382  dvradcnv  24389  abelthlem2  24400  abelthlem7  24406  tangtx  24472  tanregt0  24500  logdivlti  24580  logcnlem3  24604  logcnlem4  24605  logccv  24623  recxpcl  24635  cxpmul  24648  cxplt  24654  cxple2  24657  abscxpbnd  24708  lawcoslem1  24759  heron  24779  atans2  24872  efrlim  24910  o1cxp  24915  scvxcvx  24926  jensenlem2  24928  amgmlem  24930  fsumharmonic  24952  lgamgulmlem2  24970  lgamgulmlem3  24971  lgamgulmlem4  24972  lgamgulmlem5  24973  lgamgulmlem6  24974  relgamcl  25002  ftalem1  25013  ftalem2  25014  ftalem5  25017  basellem3  25023  basellem8  25028  chpub  25159  logfacubnd  25160  logfaclbnd  25161  logfacbnd3  25162  logexprlim  25164  perfectlem2  25169  bclbnd  25219  efexple  25220  bposlem1  25223  bposlem2  25224  bposlem6  25228  bposlem9  25231  lgsdilem  25263  gausslemma2dlem0c  25297  gausslemma2dlem2  25306  gausslemma2dlem3  25307  gausslemma2dlem6  25311  lgseisenlem4  25317  lgseisen  25318  lgsquadlem1  25319  lgsquadlem2  25320  2lgslem1a1  25328  chebbnd1lem1  25372  chebbnd1lem3  25374  chtppilimlem1  25376  chpchtlim  25382  vmadivsum  25385  rplogsumlem1  25387  rpvmasumlem  25390  dchrisumlem2  25393  dchrisumlem3  25394  dchrmusum2  25397  dchrvmasumlem2  25401  dchrvmasumiflem1  25404  dchrisum0re  25416  dchrisum0lem1  25419  dirith2  25431  mulogsumlem  25434  mulogsum  25435  mulog2sumlem2  25438  vmalogdivsum2  25441  vmalogdivsum  25442  2vmadivsumlem  25443  logsqvma  25445  logsqvma2  25446  log2sumbnd  25447  selberglem2  25449  selberg  25451  selbergb  25452  selberg2lem  25453  selberg2b  25455  chpdifbndlem1  25456  chpdifbndlem2  25457  selberg3lem1  25460  selberg3lem2  25461  selberg3  25462  selberg4lem1  25463  selberg4  25464  pntrsumbnd2  25470  selberg3r  25472  selberg4r  25473  selberg34r  25474  pntsf  25476  pntsval2  25479  pntrlog2bndlem1  25480  pntrlog2bndlem2  25481  pntrlog2bndlem3  25482  pntrlog2bndlem4  25483  pntrlog2bndlem5  25484  pntrlog2bndlem6  25486  pntrlog2bnd  25487  pntpbnd1a  25488  pntpbnd1  25489  pntpbnd2  25490  pntibndlem2a  25493  pntibndlem2  25494  pntlemb  25500  pntlemr  25505  pntlemj  25506  pntlemf  25508  pntlemk  25509  pntlemo  25510  pntlem3  25512  ostth2lem1  25521  ostth2lem2  25537  ostth2lem3  25538  ostth2lem4  25539  ostth3  25541  ttgcontlem1  25979  brbtwn2  25999  colinearalglem4  26003  axsegconlem8  26018  axsegconlem9  26019  axsegconlem10  26020  ax5seglem3  26025  axpaschlem  26034  axpasch  26035  axeuclidlem  26056  numclwwlk5  27576  numclwwlk7  27579  smcnlem  27880  ubthlem2  28055  htthlem  28102  pjhthlem1  28578  cnlnadjlem7  29260  nmopcoadji  29288  branmfn  29292  leopnmid  29325  bhmafibid1  29969  2sqmod  29973  rmulccn  30299  xrge0iifhom  30308  nexple  30396  dya2icoseg  30664  eulerpartlems  30747  eulerpartlemgc  30749  eulerpartlemb  30755  plymulx0  30949  signsvtp  30985  reprgt  31024  breprexplemc  31035  circlemethhgt  31046  hgt750lemd  31051  logdivsqrle  31053  hgt750lem  31054  hgt750lemf  31056  hgt750lemb  31059  hgt750lema  31060  hgt750leme  31061  tgoldbachgtde  31063  resconn  31551  knoppcnlem2  32801  knoppcnlem4  32803  knoppcnlem10  32809  unbdqndv2lem1  32817  unbdqndv2lem2  32818  knoppndvlem1  32820  knoppndvlem11  32830  knoppndvlem12  32831  knoppndvlem14  32833  knoppndvlem15  32834  knoppndvlem17  32836  knoppndvlem18  32837  knoppndvlem19  32838  knoppndvlem20  32839  knoppndvlem21  32840  opnmbllem0  33758  itg2addnclem2  33774  itg2addnclem3  33775  iblmulc2nc  33787  itgmulc2nclem1  33788  bddiblnc  33792  ftc1cnnclem  33795  ftc1anclem3  33799  areacirclem4  33815  geomcau  33866  equivbnd  33900  bfplem1  33932  bfplem2  33933  bfp  33934  rrnequiv  33945  rrntotbnd  33946  irrapxlem1  37888  irrapxlem2  37889  irrapxlem3  37890  irrapxlem4  37891  irrapxlem5  37892  pellexlem2  37896  pellexlem6  37900  pell14qrgt0  37925  pell1qrge1  37936  pell1qrgaplem  37939  pellqrexplicit  37943  pellqrex  37945  rmspecsqrtnq  37972  rmxycomplete  37983  rmxypos  38015  ltrmynn0  38016  ltrmxnn0  38017  jm2.24nn  38027  jm2.17a  38028  jm2.17b  38029  jm2.17c  38030  jm2.27c  38075  jm3.1lem2  38086  areaquad  38302  imo72b2lem0  38965  cvgdvgrat  39012  nzprmdif  39018  lt3addmuld  39996  fperiodmullem  39998  fperiodmul  39999  lt4addmuld  40001  xralrple2  40050  xralrple3  40070  ltmulneg  40094  fmul01  40292  fmuldfeqlem1  40294  fmul01lt1lem1  40296  sumnnodd  40342  ltmod  40350  0ellimcdiv  40361  limclner  40363  dvdivbd  40618  dvbdfbdioolem2  40624  dvbdfbdioo  40625  ioodvbdlimc1lem1  40626  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  stoweidlem1  40697  stoweidlem11  40707  stoweidlem13  40709  stoweidlem14  40710  stoweidlem16  40712  stoweidlem17  40713  stoweidlem22  40718  stoweidlem24  40720  stoweidlem25  40721  stoweidlem26  40722  stoweidlem30  40726  stoweidlem34  40730  stoweidlem36  40732  stoweidlem49  40745  stoweidlem59  40755  stoweidlem60  40756  wallispilem4  40764  wallispilem5  40765  wallispi  40766  wallispi2lem1  40767  wallispi2  40769  stirlinglem1  40770  stirlinglem3  40772  stirlinglem5  40774  stirlinglem6  40775  stirlinglem7  40776  stirlinglem10  40779  stirlinglem11  40780  stirlinglem12  40781  stirlinglem15  40784  stirlingr  40786  dirker2re  40788  dirkerval2  40790  dirkerre  40791  dirkertrigeqlem1  40794  dirkertrigeqlem2  40795  dirkeritg  40798  dirkercncflem2  40800  dirkercncflem4  40802  fourierdlem4  40807  fourierdlem5  40808  fourierdlem6  40809  fourierdlem7  40810  fourierdlem16  40819  fourierdlem18  40821  fourierdlem19  40822  fourierdlem21  40824  fourierdlem22  40825  fourierdlem26  40829  fourierdlem35  40838  fourierdlem39  40842  fourierdlem41  40844  fourierdlem42  40845  fourierdlem43  40846  fourierdlem48  40850  fourierdlem49  40851  fourierdlem51  40853  fourierdlem55  40857  fourierdlem56  40858  fourierdlem57  40859  fourierdlem58  40860  fourierdlem62  40864  fourierdlem63  40865  fourierdlem64  40866  fourierdlem65  40867  fourierdlem66  40868  fourierdlem67  40869  fourierdlem68  40870  fourierdlem71  40873  fourierdlem72  40874  fourierdlem73  40875  fourierdlem76  40878  fourierdlem77  40879  fourierdlem78  40880  fourierdlem83  40885  fourierdlem84  40886  fourierdlem87  40889  fourierdlem88  40890  fourierdlem89  40891  fourierdlem90  40892  fourierdlem91  40893  fourierdlem94  40896  fourierdlem95  40897  fourierdlem97  40899  fourierdlem103  40905  fourierdlem104  40906  fourierdlem112  40914  fourierdlem113  40915  sqwvfoura  40924  sqwvfourb  40925  fouriersw  40927  etransclem23  40953  etransclem48  40978  rrndistlt  40989  hoidmvlelem1  41291  hoidmvlelem2  41292  hoidmvlelem4  41294  smfmullem1  41480  smfmullem2  41481  smfmullem3  41482  smfmul  41484  fmtno4prmfac  42059  lighneallem4a  42100  perfectALTVlem2  42206  ply1mulgsumlem2  42743  digvalnn0  42961  dignn0fr  42963  dig2nn0  42973  amgmwlem  43119