Theorem remulcld 11160

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023   · cmul 11029

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

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

This theorem is referenced by:  mulge0  11653  msqge0  11656  redivcl  11858  prodgt0  11986  ltmul1a  11988  ltmul1  11989  ltmuldiv  12013  lt2msq1  12024  lt2msq  12025  le2msq  12040  msq11  12041  supmul1  12109  supmullem2  12111  supmul  12112  div4p1lem1div2  12394  mul2lt0rlt0  13007  mul2lt0bi  13011  prodge0rd  13012  ge2halflem1  13020  qbtwnre  13112  xmulneg1  13182  xmulf  13185  lincmb01cmp  13409  iccf1o  13410  flmulnn0  13745  flhalf  13748  modcl  13791  mod0  13794  modge0  13797  modmulnn  13807  mulp1mod1  13832  muladdmod  13833  2txmodxeq0  13852  modaddmulmod  13859  moddi  13860  modsubdir  13861  modirr  13863  addmodlteq  13867  bernneq  14150  bernneq3  14152  expnbnd  14153  expmulnbnd  14156  discr1  14160  discr  14161  faclbnd  14211  faclbnd6  14220  remullem  15049  01sqrexlem7  15169  sqrtmul  15180  abstri  15252  sqreulem  15281  bhmafibid1  15389  mulcn2  15517  reccn2  15518  o1rlimmul  15540  lo1mul  15549  iseraltlem2  15604  iseraltlem3  15605  iseralt  15606  o1fsum  15734  cvgcmpce  15739  climcndslem1  15770  climcndslem2  15771  climcnds  15772  geomulcvg  15797  cvgrat  15804  mertenslem1  15805  fprodge1  15916  eftlub  16032  sin02gt0  16115  eirrlem  16127  bitsp1o  16358  2mulprm  16618  isprm5  16632  modprm0  16731  prmreclem3  16844  prmreclem4  16845  prmreclem5  16846  2expltfac  17018  metss2lem  24453  nlmvscnlem2  24627  nrginvrcnlem  24633  nmoco  24679  nmotri  24681  nghmcn  24687  icopnfhmeo  24895  nmoleub2lem3  25069  ipcau2  25188  tcphcphlem1  25189  ipcnlem2  25198  rrxcph  25346  csbren  25353  trirn  25354  pjthlem1  25391  opnmbllem  25556  vitalilem4  25566  itg1val2  25639  itg1cl  25640  itg1ge0  25641  itg1addlem4  25654  itg1mulc  25659  itg1ge0a  25666  itg1climres  25669  mbfi1fseqlem1  25670  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  mbfi1fseqlem6  25675  itg2const2  25696  itg2mulclem  25701  itg2mulc  25702  itg2monolem1  25705  itg2monolem3  25707  itg2cnlem2  25717  iblconst  25773  iblmulc2  25786  itgmulc2lem1  25787  itgmulc2lem2  25788  bddmulibl  25794  bddiblnc  25797  dveflem  25937  cmvth  25949  cmvthOLD  25950  dvlip  25952  dvlipcn  25953  dvivthlem1  25967  lhop1lem  25972  dvcvx  25979  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem3  25989  dvfsumlem4  25990  dvfsum2  25995  ftc1lem4  26000  plyeq0lem  26169  aalioulem3  26296  aalioulem4  26297  aaliou3lem9  26312  ulmdvlem1  26363  itgulm  26371  radcnvlem1  26376  radcnvlem2  26377  dvradcnv  26384  abelthlem2  26396  abelthlem7  26402  tangtx  26468  tanregt0  26502  logdivlti  26583  logcnlem3  26607  logcnlem4  26608  logccv  26626  recxpcl  26638  cxpmul  26651  cxplt  26657  cxple2  26660  abscxpbnd  26717  lawcoslem1  26779  heron  26802  atans2  26895  efrlim  26933  efrlimOLD  26934  o1cxp  26939  scvxcvx  26950  jensenlem2  26952  amgmlem  26954  fsumharmonic  26976  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem4  26996  lgamgulmlem5  26997  lgamgulmlem6  26998  relgamcl  27026  ftalem1  27037  ftalem2  27038  ftalem5  27041  basellem3  27047  basellem8  27052  chpub  27185  logfacubnd  27186  logfaclbnd  27187  logfacbnd3  27188  logexprlim  27190  perfectlem2  27195  bclbnd  27245  efexple  27246  bposlem1  27249  bposlem2  27250  bposlem6  27254  bposlem9  27257  lgsdilem  27289  gausslemma2dlem0c  27323  gausslemma2dlem2  27332  gausslemma2dlem3  27333  gausslemma2dlem6  27337  lgseisenlem4  27343  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  2lgslem1a1  27354  2sqmod  27401  chebbnd1lem1  27434  chebbnd1lem3  27436  chtppilimlem1  27438  chpchtlim  27444  vmadivsum  27447  rplogsumlem1  27449  rpvmasumlem  27452  dchrisumlem2  27455  dchrisumlem3  27456  dchrmusum2  27459  dchrvmasumlem2  27463  dchrvmasumiflem1  27466  dchrisum0re  27478  dchrisum0lem1  27481  dirith2  27493  mulogsumlem  27496  mulogsum  27497  mulog2sumlem2  27500  vmalogdivsum2  27503  vmalogdivsum  27504  2vmadivsumlem  27505  logsqvma  27507  logsqvma2  27508  log2sumbnd  27509  selberglem2  27511  selberg  27513  selbergb  27514  selberg2lem  27515  selberg2b  27517  chpdifbndlem1  27518  chpdifbndlem2  27519  selberg3lem1  27522  selberg3lem2  27523  selberg3  27524  selberg4lem1  27525  selberg4  27526  pntrsumbnd2  27532  selberg3r  27534  selberg4r  27535  selberg34r  27536  pntsf  27538  pntsval2  27541  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntibndlem2a  27555  pntibndlem2  27556  pntlemb  27562  pntlemr  27567  pntlemj  27568  pntlemf  27570  pntlemk  27571  pntlemo  27572  pntlem3  27574  ostth2lem1  27583  ostth2lem2  27599  ostth2lem3  27600  ostth2lem4  27601  ostth3  27603  ttgcontlem1  28906  brbtwn2  28927  colinearalglem4  28931  axsegconlem8  28946  axsegconlem9  28947  axsegconlem10  28948  ax5seglem3  28953  axpaschlem  28962  axpasch  28963  axeuclidlem  28984  numclwwlk5  30412  numclwwlk7  30415  smcnlem  30721  ubthlem2  30895  htthlem  30941  pjhthlem1  31415  cnlnadjlem7  32097  nmopcoadji  32125  branmfn  32129  leopnmid  32162  nexple  32874  constrremulcl  33873  constrmulcl  33877  cos9thpiminplylem1  33888  cos9thpinconstrlem1  33895  rmulccn  34034  xrge0iifhom  34043  dya2icoseg  34383  eulerpartlems  34466  eulerpartlemgc  34468  eulerpartlemb  34474  plymulx0  34653  signsvtp  34689  reprgt  34727  breprexplemc  34738  circlemethhgt  34749  hgt750lemd  34754  logdivsqrle  34756  hgt750lem  34757  hgt750lemf  34759  hgt750lemb  34762  hgt750lema  34763  hgt750leme  34764  tgoldbachgtde  34766  resconn  35389  knoppcnlem2  36637  knoppcnlem4  36639  knoppcnlem10  36645  unbdqndv2lem1  36652  unbdqndv2lem2  36653  knoppndvlem1  36655  knoppndvlem11  36665  knoppndvlem12  36666  knoppndvlem14  36668  knoppndvlem15  36669  knoppndvlem17  36671  knoppndvlem18  36672  knoppndvlem19  36673  knoppndvlem20  36674  knoppndvlem21  36675  opnmbllem0  37796  itg2addnclem2  37812  itg2addnclem3  37813  iblmulc2nc  37825  itgmulc2nclem1  37826  ftc1cnnclem  37831  ftc1anclem3  37835  areacirclem4  37851  geomcau  37899  equivbnd  37930  bfplem1  37962  bfplem2  37963  bfp  37964  rrnequiv  37975  rrntotbnd  37976  lcmineqlem19  42240  lcmineqlem20  42241  lcmineqlem21  42242  lcmineqlem22  42243  3lexlogpow2ineq2  42252  dvrelogpow2b  42261  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  aks4d1p8d2  42278  aks4d1p8  42280  posbezout  42293  aks6d1c2lem4  42320  2np3bcnp1  42337  2ap1caineq  42338  aks6d1c6lem4  42366  aks6d1c7lem1  42373  aks6d1c7lem2  42374  resubdi  42593  remul02  42602  remul01  42604  remulinvcom  42630  rediveud  42640  redivcan3d  42644  sn-0tie0  42648  renegmulnnass  42662  mulgt0con1d  42667  mulgt0con2d  42668  mulgt0b1d  42669  sn-ltmul2d  42670  mulgt0b2d  42675  sn-mulgt1d  42676  mulltgt0d  42679  mullt0b1d  42680  mullt0b2d  42681  sn-mullt0d  42682  sn-itrere  42685  sn-retire  42686  fltnltalem  42847  fltnlta  42848  3cubeslem2  42869  3cubeslem3r  42871  3cubeslem4  42873  irrapxlem1  43006  irrapxlem2  43007  irrapxlem3  43008  irrapxlem4  43009  irrapxlem5  43010  pellexlem2  43014  pellexlem6  43018  pell14qrgt0  43043  pell1qrge1  43054  pell1qrgaplem  43057  pellqrexplicit  43061  pellqrex  43063  rmspecsqrtnq  43090  rmxycomplete  43101  rmxypos  43131  ltrmynn0  43132  ltrmxnn0  43133  jm2.24nn  43143  jm2.17a  43144  jm2.17b  43145  jm2.17c  43146  jm2.27c  43191  jm3.1lem2  43202  areaquad  43400  sqrtcval  43824  resqrtval  43826  imsqrtval  43827  imo72b2lem0  44348  cvgdvgrat  44496  nzprmdif  44502  lt3addmuld  45491  fperiodmullem  45493  fperiodmul  45494  lt4addmuld  45496  xralrple2  45541  xralrple3  45560  ltmulneg  45578  fmul01  45768  fmuldfeqlem1  45770  fmul01lt1lem1  45772  sumnnodd  45818  ltmod  45824  0ellimcdiv  45835  limclner  45837  dvdivbd  46109  dvbdfbdioolem2  46115  dvbdfbdioo  46116  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  stoweidlem1  46187  stoweidlem11  46197  stoweidlem13  46199  stoweidlem14  46200  stoweidlem16  46202  stoweidlem17  46203  stoweidlem22  46208  stoweidlem24  46210  stoweidlem25  46211  stoweidlem26  46212  stoweidlem30  46216  stoweidlem34  46220  stoweidlem36  46222  stoweidlem49  46235  stoweidlem59  46245  stoweidlem60  46246  wallispilem4  46254  wallispilem5  46255  wallispi  46256  wallispi2lem1  46257  wallispi2  46259  stirlinglem1  46260  stirlinglem3  46262  stirlinglem5  46264  stirlinglem6  46265  stirlinglem7  46266  stirlinglem10  46269  stirlinglem11  46270  stirlinglem12  46271  stirlinglem15  46274  stirlingr  46276  dirker2re  46278  dirkerval2  46280  dirkerre  46281  dirkertrigeqlem1  46284  dirkertrigeqlem2  46285  dirkeritg  46288  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem4  46297  fourierdlem5  46298  fourierdlem6  46299  fourierdlem7  46300  fourierdlem16  46309  fourierdlem18  46311  fourierdlem19  46312  fourierdlem21  46314  fourierdlem22  46315  fourierdlem26  46319  fourierdlem35  46328  fourierdlem39  46332  fourierdlem41  46334  fourierdlem42  46335  fourierdlem43  46336  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem55  46347  fourierdlem56  46348  fourierdlem57  46349  fourierdlem58  46350  fourierdlem62  46354  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem66  46358  fourierdlem67  46359  fourierdlem68  46360  fourierdlem71  46363  fourierdlem72  46364  fourierdlem73  46365  fourierdlem76  46368  fourierdlem77  46369  fourierdlem78  46370  fourierdlem83  46375  fourierdlem84  46376  fourierdlem87  46379  fourierdlem88  46380  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem94  46386  fourierdlem95  46387  fourierdlem97  46389  fourierdlem103  46395  fourierdlem104  46396  fourierdlem112  46404  fourierdlem113  46405  sqwvfoura  46414  sqwvfourb  46415  fouriersw  46417  etransclem23  46443  etransclem48  46468  rrndistlt  46476  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem4  46784  smfmullem1  46977  smfmullem2  46978  smfmullem3  46979  smfmul  46981  fmtno4prmfac  47760  lighneallem4a  47796  requad01  47809  requad1  47810  requad2  47811  perfectALTVlem2  47910  gpg3kgrtriexlem1  48271  gpg3kgrtriexlem4  48274  gpg3kgrtriexlem6  48276  ply1mulgsumlem2  48575  digvalnn0  48787  dignn0fr  48789  dig2nn0  48799  affinecomb1  48890  rrx2linest2  48932  line2  48940  itsclc0lem1  48944  itsclc0lem2  48945  itsclc0lem3  48946  itscnhlc0yqe  48947  itsclc0yqsollem2  48951  itsclc0yqsol  48952  itscnhlc0xyqsol  48953  itsclc0xyqsolr  48957  itsclinecirc0  48961  itsclinecirc0b  48962  itsclinecirc0in  48963  itsclquadb  48964  itsclquadeu  48965  2itscp  48969  itscnhlinecirc02plem1  48970  itscnhlinecirc02p  48973  inlinecirc02plem  48974  amgmwlem  49989