Theorem remulcld 11166

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7360  ℝcr 11029   · cmul 11035

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

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

This theorem is referenced by:  mulge0  11659  msqge0  11662  redivcl  11864  prodgt0  11992  ltmul1a  11994  ltmul1  11995  ltmuldiv  12019  lt2msq1  12030  lt2msq  12031  le2msq  12046  msq11  12047  supmul1  12115  supmullem2  12117  supmul  12118  div4p1lem1div2  12400  mul2lt0rlt0  13013  mul2lt0bi  13017  prodge0rd  13018  ge2halflem1  13026  qbtwnre  13118  xmulneg1  13188  xmulf  13191  lincmb01cmp  13415  iccf1o  13416  flmulnn0  13751  flhalf  13754  modcl  13797  mod0  13800  modge0  13803  modmulnn  13813  mulp1mod1  13838  muladdmod  13839  2txmodxeq0  13858  modaddmulmod  13865  moddi  13866  modsubdir  13867  modirr  13869  addmodlteq  13873  bernneq  14156  bernneq3  14158  expnbnd  14159  expmulnbnd  14162  discr1  14166  discr  14167  faclbnd  14217  faclbnd6  14226  remullem  15055  01sqrexlem7  15175  sqrtmul  15186  abstri  15258  sqreulem  15287  bhmafibid1  15395  mulcn2  15523  reccn2  15524  o1rlimmul  15546  lo1mul  15555  iseraltlem2  15610  iseraltlem3  15611  iseralt  15612  o1fsum  15740  cvgcmpce  15745  climcndslem1  15776  climcndslem2  15777  climcnds  15778  geomulcvg  15803  cvgrat  15810  mertenslem1  15811  fprodge1  15922  eftlub  16038  sin02gt0  16121  eirrlem  16133  bitsp1o  16364  2mulprm  16624  isprm5  16638  modprm0  16737  prmreclem3  16850  prmreclem4  16851  prmreclem5  16852  2expltfac  17024  metss2lem  24459  nlmvscnlem2  24633  nrginvrcnlem  24639  nmoco  24685  nmotri  24687  nghmcn  24693  icopnfhmeo  24901  nmoleub2lem3  25075  ipcau2  25194  tcphcphlem1  25195  ipcnlem2  25204  rrxcph  25352  csbren  25359  trirn  25360  pjthlem1  25397  opnmbllem  25562  vitalilem4  25572  itg1val2  25645  itg1cl  25646  itg1ge0  25647  itg1addlem4  25660  itg1mulc  25665  itg1ge0a  25672  itg1climres  25675  mbfi1fseqlem1  25676  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  mbfi1fseqlem6  25681  itg2const2  25702  itg2mulclem  25707  itg2mulc  25708  itg2monolem1  25711  itg2monolem3  25713  itg2cnlem2  25723  iblconst  25779  iblmulc2  25792  itgmulc2lem1  25793  itgmulc2lem2  25794  bddmulibl  25800  bddiblnc  25803  dveflem  25943  cmvth  25955  cmvthOLD  25956  dvlip  25958  dvlipcn  25959  dvivthlem1  25973  lhop1lem  25978  dvcvx  25985  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  ftc1lem4  26006  plyeq0lem  26175  aalioulem3  26302  aalioulem4  26303  aaliou3lem9  26318  ulmdvlem1  26369  itgulm  26377  radcnvlem1  26382  radcnvlem2  26383  dvradcnv  26390  abelthlem2  26402  abelthlem7  26408  tangtx  26474  tanregt0  26508  logdivlti  26589  logcnlem3  26613  logcnlem4  26614  logccv  26632  recxpcl  26644  cxpmul  26657  cxplt  26663  cxple2  26666  abscxpbnd  26723  lawcoslem1  26785  heron  26808  atans2  26901  efrlim  26939  efrlimOLD  26940  o1cxp  26945  scvxcvx  26956  jensenlem2  26958  amgmlem  26960  fsumharmonic  26982  lgamgulmlem2  27000  lgamgulmlem3  27001  lgamgulmlem4  27002  lgamgulmlem5  27003  lgamgulmlem6  27004  relgamcl  27032  ftalem1  27043  ftalem2  27044  ftalem5  27047  basellem3  27053  basellem8  27058  chpub  27191  logfacubnd  27192  logfaclbnd  27193  logfacbnd3  27194  logexprlim  27196  perfectlem2  27201  bclbnd  27251  efexple  27252  bposlem1  27255  bposlem2  27256  bposlem6  27260  bposlem9  27263  lgsdilem  27295  gausslemma2dlem0c  27329  gausslemma2dlem2  27338  gausslemma2dlem3  27339  gausslemma2dlem6  27343  lgseisenlem4  27349  lgseisen  27350  lgsquadlem1  27351  lgsquadlem2  27352  2lgslem1a1  27360  2sqmod  27407  chebbnd1lem1  27440  chebbnd1lem3  27442  chtppilimlem1  27444  chpchtlim  27450  vmadivsum  27453  rplogsumlem1  27455  rpvmasumlem  27458  dchrisumlem2  27461  dchrisumlem3  27462  dchrmusum2  27465  dchrvmasumlem2  27469  dchrvmasumiflem1  27472  dchrisum0re  27484  dchrisum0lem1  27487  dirith2  27499  mulogsumlem  27502  mulogsum  27503  mulog2sumlem2  27506  vmalogdivsum2  27509  vmalogdivsum  27510  2vmadivsumlem  27511  logsqvma  27513  logsqvma2  27514  log2sumbnd  27515  selberglem2  27517  selberg  27519  selbergb  27520  selberg2lem  27521  selberg2b  27523  chpdifbndlem1  27524  chpdifbndlem2  27525  selberg3lem1  27528  selberg3lem2  27529  selberg3  27530  selberg4lem1  27531  selberg4  27532  pntrsumbnd2  27538  selberg3r  27540  selberg4r  27541  selberg34r  27542  pntsf  27544  pntsval2  27547  pntrlog2bndlem1  27548  pntrlog2bndlem2  27549  pntrlog2bndlem3  27550  pntrlog2bndlem4  27551  pntrlog2bndlem5  27552  pntrlog2bndlem6  27554  pntrlog2bnd  27555  pntpbnd1a  27556  pntpbnd1  27557  pntpbnd2  27558  pntibndlem2a  27561  pntibndlem2  27562  pntlemb  27568  pntlemr  27573  pntlemj  27574  pntlemf  27576  pntlemk  27577  pntlemo  27578  pntlem3  27580  ostth2lem1  27589  ostth2lem2  27605  ostth2lem3  27606  ostth2lem4  27607  ostth3  27609  ttgcontlem1  28961  brbtwn2  28982  colinearalglem4  28986  axsegconlem8  29001  axsegconlem9  29002  axsegconlem10  29003  ax5seglem3  29008  axpaschlem  29017  axpasch  29018  axeuclidlem  29039  numclwwlk5  30467  numclwwlk7  30470  smcnlem  30776  ubthlem2  30950  htthlem  30996  pjhthlem1  31470  cnlnadjlem7  32152  nmopcoadji  32180  branmfn  32184  leopnmid  32217  nexple  32927  constrremulcl  33926  constrmulcl  33930  cos9thpiminplylem1  33941  cos9thpinconstrlem1  33948  rmulccn  34087  xrge0iifhom  34096  dya2icoseg  34436  eulerpartlems  34519  eulerpartlemgc  34521  eulerpartlemb  34527  plymulx0  34706  signsvtp  34742  reprgt  34780  breprexplemc  34791  circlemethhgt  34802  hgt750lemd  34807  logdivsqrle  34809  hgt750lem  34810  hgt750lemf  34812  hgt750lemb  34815  hgt750lema  34816  hgt750leme  34817  tgoldbachgtde  34819  resconn  35442  knoppcnlem2  36696  knoppcnlem4  36698  knoppcnlem10  36704  unbdqndv2lem1  36711  unbdqndv2lem2  36712  knoppndvlem1  36714  knoppndvlem11  36724  knoppndvlem12  36725  knoppndvlem14  36727  knoppndvlem15  36728  knoppndvlem17  36730  knoppndvlem18  36731  knoppndvlem19  36732  knoppndvlem20  36733  knoppndvlem21  36734  opnmbllem0  37859  itg2addnclem2  37875  itg2addnclem3  37876  iblmulc2nc  37888  itgmulc2nclem1  37889  ftc1cnnclem  37894  ftc1anclem3  37898  areacirclem4  37914  geomcau  37962  equivbnd  37993  bfplem1  38025  bfplem2  38026  bfp  38027  rrnequiv  38038  rrntotbnd  38039  lcmineqlem19  42369  lcmineqlem20  42370  lcmineqlem21  42371  lcmineqlem22  42372  3lexlogpow2ineq2  42381  dvrelogpow2b  42390  aks4d1p1p2  42392  aks4d1p1p4  42393  aks4d1p1p6  42395  aks4d1p1p7  42396  aks4d1p1p5  42397  aks4d1p1  42398  aks4d1p8d2  42407  aks4d1p8  42409  posbezout  42422  aks6d1c2lem4  42449  2np3bcnp1  42466  2ap1caineq  42467  aks6d1c6lem4  42495  aks6d1c7lem1  42502  aks6d1c7lem2  42503  resubdi  42718  remul02  42727  remul01  42729  remulinvcom  42755  rediveud  42765  redivcan3d  42769  sn-0tie0  42773  renegmulnnass  42787  mulgt0con1d  42792  mulgt0con2d  42793  mulgt0b1d  42794  sn-ltmul2d  42795  mulgt0b2d  42800  sn-mulgt1d  42801  mulltgt0d  42804  mullt0b1d  42805  mullt0b2d  42806  sn-mullt0d  42807  sn-itrere  42810  sn-retire  42811  fltnltalem  42972  fltnlta  42973  3cubeslem2  42994  3cubeslem3r  42996  3cubeslem4  42998  irrapxlem1  43131  irrapxlem2  43132  irrapxlem3  43133  irrapxlem4  43134  irrapxlem5  43135  pellexlem2  43139  pellexlem6  43143  pell14qrgt0  43168  pell1qrge1  43179  pell1qrgaplem  43182  pellqrexplicit  43186  pellqrex  43188  rmspecsqrtnq  43215  rmxycomplete  43226  rmxypos  43256  ltrmynn0  43257  ltrmxnn0  43258  jm2.24nn  43268  jm2.17a  43269  jm2.17b  43270  jm2.17c  43271  jm2.27c  43316  jm3.1lem2  43327  areaquad  43525  sqrtcval  43949  resqrtval  43951  imsqrtval  43952  imo72b2lem0  44473  cvgdvgrat  44621  nzprmdif  44627  lt3addmuld  45616  fperiodmullem  45618  fperiodmul  45619  lt4addmuld  45621  xralrple2  45666  xralrple3  45685  ltmulneg  45703  fmul01  45893  fmuldfeqlem1  45895  fmul01lt1lem1  45897  sumnnodd  45943  ltmod  45949  0ellimcdiv  45960  limclner  45962  dvdivbd  46234  dvbdfbdioolem2  46240  dvbdfbdioo  46241  ioodvbdlimc1lem1  46242  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  stoweidlem1  46312  stoweidlem11  46322  stoweidlem13  46324  stoweidlem14  46325  stoweidlem16  46327  stoweidlem17  46328  stoweidlem22  46333  stoweidlem24  46335  stoweidlem25  46336  stoweidlem26  46337  stoweidlem30  46341  stoweidlem34  46345  stoweidlem36  46347  stoweidlem49  46360  stoweidlem59  46370  stoweidlem60  46371  wallispilem4  46379  wallispilem5  46380  wallispi  46381  wallispi2lem1  46382  wallispi2  46384  stirlinglem1  46385  stirlinglem3  46387  stirlinglem5  46389  stirlinglem6  46390  stirlinglem7  46391  stirlinglem10  46394  stirlinglem11  46395  stirlinglem12  46396  stirlinglem15  46399  stirlingr  46401  dirker2re  46403  dirkerval2  46405  dirkerre  46406  dirkertrigeqlem1  46409  dirkertrigeqlem2  46410  dirkeritg  46413  dirkercncflem2  46415  dirkercncflem4  46417  fourierdlem4  46422  fourierdlem5  46423  fourierdlem6  46424  fourierdlem7  46425  fourierdlem16  46434  fourierdlem18  46436  fourierdlem19  46437  fourierdlem21  46439  fourierdlem22  46440  fourierdlem26  46444  fourierdlem35  46453  fourierdlem39  46457  fourierdlem41  46459  fourierdlem42  46460  fourierdlem43  46461  fourierdlem48  46465  fourierdlem49  46466  fourierdlem51  46468  fourierdlem55  46472  fourierdlem56  46473  fourierdlem57  46474  fourierdlem58  46475  fourierdlem62  46479  fourierdlem63  46480  fourierdlem64  46481  fourierdlem65  46482  fourierdlem66  46483  fourierdlem67  46484  fourierdlem68  46485  fourierdlem71  46488  fourierdlem72  46489  fourierdlem73  46490  fourierdlem76  46493  fourierdlem77  46494  fourierdlem78  46495  fourierdlem83  46500  fourierdlem84  46501  fourierdlem87  46504  fourierdlem88  46505  fourierdlem89  46506  fourierdlem90  46507  fourierdlem91  46508  fourierdlem94  46511  fourierdlem95  46512  fourierdlem97  46514  fourierdlem103  46520  fourierdlem104  46521  fourierdlem112  46529  fourierdlem113  46530  sqwvfoura  46539  sqwvfourb  46540  fouriersw  46542  etransclem23  46568  etransclem48  46593  rrndistlt  46601  hoidmvlelem1  46906  hoidmvlelem2  46907  hoidmvlelem4  46909  smfmullem1  47102  smfmullem2  47103  smfmullem3  47104  smfmul  47106  fmtno4prmfac  47885  lighneallem4a  47921  requad01  47934  requad1  47935  requad2  47936  perfectALTVlem2  48035  gpg3kgrtriexlem1  48396  gpg3kgrtriexlem4  48399  gpg3kgrtriexlem6  48401  ply1mulgsumlem2  48700  digvalnn0  48912  dignn0fr  48914  dig2nn0  48924  affinecomb1  49015  rrx2linest2  49057  line2  49065  itsclc0lem1  49069  itsclc0lem2  49070  itsclc0lem3  49071  itscnhlc0yqe  49072  itsclc0yqsollem2  49076  itsclc0yqsol  49077  itscnhlc0xyqsol  49078  itsclc0xyqsolr  49082  itsclinecirc0  49086  itsclinecirc0b  49087  itsclinecirc0in  49088  itsclquadb  49089  itsclquadeu  49090  2itscp  49094  itscnhlinecirc02plem1  49095  itscnhlinecirc02p  49098  inlinecirc02plem  49099  amgmwlem  50114