Theorem remulcld 11176

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7370  ℝcr 11039   · cmul 11045

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

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

This theorem is referenced by:  mulge0  11669  msqge0  11672  redivcl  11874  prodgt0  12002  ltmul1a  12004  ltmul1  12005  ltmuldiv  12029  lt2msq1  12040  lt2msq  12041  le2msq  12056  msq11  12057  supmul1  12125  supmullem2  12127  supmul  12128  div4p1lem1div2  12410  mul2lt0rlt0  13023  mul2lt0bi  13027  prodge0rd  13028  ge2halflem1  13036  qbtwnre  13128  xmulneg1  13198  xmulf  13201  lincmb01cmp  13425  iccf1o  13426  flmulnn0  13761  flhalf  13764  modcl  13807  mod0  13810  modge0  13813  modmulnn  13823  mulp1mod1  13848  muladdmod  13849  2txmodxeq0  13868  modaddmulmod  13875  moddi  13876  modsubdir  13877  modirr  13879  addmodlteq  13883  bernneq  14166  bernneq3  14168  expnbnd  14169  expmulnbnd  14172  discr1  14176  discr  14177  faclbnd  14227  faclbnd6  14236  remullem  15065  01sqrexlem7  15185  sqrtmul  15196  abstri  15268  sqreulem  15297  bhmafibid1  15405  mulcn2  15533  reccn2  15534  o1rlimmul  15556  lo1mul  15565  iseraltlem2  15620  iseraltlem3  15621  iseralt  15622  o1fsum  15750  cvgcmpce  15755  climcndslem1  15786  climcndslem2  15787  climcnds  15788  geomulcvg  15813  cvgrat  15820  mertenslem1  15821  fprodge1  15932  eftlub  16048  sin02gt0  16131  eirrlem  16143  bitsp1o  16374  2mulprm  16634  isprm5  16648  modprm0  16747  prmreclem3  16860  prmreclem4  16861  prmreclem5  16862  2expltfac  17034  metss2lem  24472  nlmvscnlem2  24646  nrginvrcnlem  24652  nmoco  24698  nmotri  24700  nghmcn  24706  icopnfhmeo  24914  nmoleub2lem3  25088  ipcau2  25207  tcphcphlem1  25208  ipcnlem2  25217  rrxcph  25365  csbren  25372  trirn  25373  pjthlem1  25410  opnmbllem  25575  vitalilem4  25585  itg1val2  25658  itg1cl  25659  itg1ge0  25660  itg1addlem4  25673  itg1mulc  25678  itg1ge0a  25685  itg1climres  25688  mbfi1fseqlem1  25689  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  mbfi1fseqlem6  25694  itg2const2  25715  itg2mulclem  25720  itg2mulc  25721  itg2monolem1  25724  itg2monolem3  25726  itg2cnlem2  25736  iblconst  25792  iblmulc2  25805  itgmulc2lem1  25806  itgmulc2lem2  25807  bddmulibl  25813  bddiblnc  25816  dveflem  25956  cmvth  25968  cmvthOLD  25969  dvlip  25971  dvlipcn  25972  dvivthlem1  25986  lhop1lem  25991  dvcvx  25998  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsum2  26014  ftc1lem4  26019  plyeq0lem  26188  aalioulem3  26315  aalioulem4  26316  aaliou3lem9  26331  ulmdvlem1  26382  itgulm  26390  radcnvlem1  26395  radcnvlem2  26396  dvradcnv  26403  abelthlem2  26415  abelthlem7  26421  tangtx  26487  tanregt0  26521  logdivlti  26602  logcnlem3  26626  logcnlem4  26627  logccv  26645  recxpcl  26657  cxpmul  26670  cxplt  26676  cxple2  26679  abscxpbnd  26736  lawcoslem1  26798  heron  26821  atans2  26914  efrlim  26952  efrlimOLD  26953  o1cxp  26958  scvxcvx  26969  jensenlem2  26971  amgmlem  26973  fsumharmonic  26995  lgamgulmlem2  27013  lgamgulmlem3  27014  lgamgulmlem4  27015  lgamgulmlem5  27016  lgamgulmlem6  27017  relgamcl  27045  ftalem1  27056  ftalem2  27057  ftalem5  27060  basellem3  27066  basellem8  27071  chpub  27204  logfacubnd  27205  logfaclbnd  27206  logfacbnd3  27207  logexprlim  27209  perfectlem2  27214  bclbnd  27264  efexple  27265  bposlem1  27268  bposlem2  27269  bposlem6  27273  bposlem9  27276  lgsdilem  27308  gausslemma2dlem0c  27342  gausslemma2dlem2  27351  gausslemma2dlem3  27352  gausslemma2dlem6  27356  lgseisenlem4  27362  lgseisen  27363  lgsquadlem1  27364  lgsquadlem2  27365  2lgslem1a1  27373  2sqmod  27420  chebbnd1lem1  27453  chebbnd1lem3  27455  chtppilimlem1  27457  chpchtlim  27463  vmadivsum  27466  rplogsumlem1  27468  rpvmasumlem  27471  dchrisumlem2  27474  dchrisumlem3  27475  dchrmusum2  27478  dchrvmasumlem2  27482  dchrvmasumiflem1  27485  dchrisum0re  27497  dchrisum0lem1  27500  dirith2  27512  mulogsumlem  27515  mulogsum  27516  mulog2sumlem2  27519  vmalogdivsum2  27522  vmalogdivsum  27523  2vmadivsumlem  27524  logsqvma  27526  logsqvma2  27527  log2sumbnd  27528  selberglem2  27530  selberg  27532  selbergb  27533  selberg2lem  27534  selberg2b  27536  chpdifbndlem1  27537  chpdifbndlem2  27538  selberg3lem1  27541  selberg3lem2  27542  selberg3  27543  selberg4lem1  27544  selberg4  27545  pntrsumbnd2  27551  selberg3r  27553  selberg4r  27554  selberg34r  27555  pntsf  27557  pntsval2  27560  pntrlog2bndlem1  27561  pntrlog2bndlem2  27562  pntrlog2bndlem3  27563  pntrlog2bndlem4  27564  pntrlog2bndlem5  27565  pntrlog2bndlem6  27567  pntrlog2bnd  27568  pntpbnd1a  27569  pntpbnd1  27570  pntpbnd2  27571  pntibndlem2a  27574  pntibndlem2  27575  pntlemb  27581  pntlemr  27586  pntlemj  27587  pntlemf  27589  pntlemk  27590  pntlemo  27591  pntlem3  27593  ostth2lem1  27602  ostth2lem2  27618  ostth2lem3  27619  ostth2lem4  27620  ostth3  27622  ttgcontlem1  28975  brbtwn2  28996  colinearalglem4  29000  axsegconlem8  29015  axsegconlem9  29016  axsegconlem10  29017  ax5seglem3  29022  axpaschlem  29031  axpasch  29032  axeuclidlem  29053  numclwwlk5  30481  numclwwlk7  30484  smcnlem  30791  ubthlem2  30965  htthlem  31011  pjhthlem1  31485  cnlnadjlem7  32167  nmopcoadji  32195  branmfn  32199  leopnmid  32232  nexple  32942  constrremulcl  33951  constrmulcl  33955  cos9thpiminplylem1  33966  cos9thpinconstrlem1  33973  rmulccn  34112  xrge0iifhom  34121  dya2icoseg  34461  eulerpartlems  34544  eulerpartlemgc  34546  eulerpartlemb  34552  plymulx0  34731  signsvtp  34767  reprgt  34805  breprexplemc  34816  circlemethhgt  34827  hgt750lemd  34832  logdivsqrle  34834  hgt750lem  34835  hgt750lemf  34837  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  tgoldbachgtde  34844  resconn  35468  knoppcnlem2  36722  knoppcnlem4  36724  knoppcnlem10  36730  unbdqndv2lem1  36737  unbdqndv2lem2  36738  knoppndvlem1  36740  knoppndvlem11  36750  knoppndvlem12  36751  knoppndvlem14  36753  knoppndvlem15  36754  knoppndvlem17  36756  knoppndvlem18  36757  knoppndvlem19  36758  knoppndvlem20  36759  knoppndvlem21  36760  opnmbllem0  37936  itg2addnclem2  37952  itg2addnclem3  37953  iblmulc2nc  37965  itgmulc2nclem1  37966  ftc1cnnclem  37971  ftc1anclem3  37975  areacirclem4  37991  geomcau  38039  equivbnd  38070  bfplem1  38102  bfplem2  38103  bfp  38104  rrnequiv  38115  rrntotbnd  38116  lcmineqlem19  42446  lcmineqlem20  42447  lcmineqlem21  42448  lcmineqlem22  42449  3lexlogpow2ineq2  42458  dvrelogpow2b  42467  aks4d1p1p2  42469  aks4d1p1p4  42470  aks4d1p1p6  42472  aks4d1p1p7  42473  aks4d1p1p5  42474  aks4d1p1  42475  aks4d1p8d2  42484  aks4d1p8  42486  posbezout  42499  aks6d1c2lem4  42526  2np3bcnp1  42543  2ap1caineq  42544  aks6d1c6lem4  42572  aks6d1c7lem1  42579  aks6d1c7lem2  42580  resubdi  42795  remul02  42804  remul01  42806  remulinvcom  42832  rediveud  42842  redivcan3d  42846  sn-0tie0  42850  renegmulnnass  42864  mulgt0con1d  42869  mulgt0con2d  42870  mulgt0b1d  42871  sn-ltmul2d  42872  mulgt0b2d  42877  sn-mulgt1d  42878  mulltgt0d  42881  mullt0b1d  42882  mullt0b2d  42883  sn-mullt0d  42884  sn-itrere  42887  sn-retire  42888  fltnltalem  43049  fltnlta  43050  3cubeslem2  43071  3cubeslem3r  43073  3cubeslem4  43075  irrapxlem1  43208  irrapxlem2  43209  irrapxlem3  43210  irrapxlem4  43211  irrapxlem5  43212  pellexlem2  43216  pellexlem6  43220  pell14qrgt0  43245  pell1qrge1  43256  pell1qrgaplem  43259  pellqrexplicit  43263  pellqrex  43265  rmspecsqrtnq  43292  rmxycomplete  43303  rmxypos  43333  ltrmynn0  43334  ltrmxnn0  43335  jm2.24nn  43345  jm2.17a  43346  jm2.17b  43347  jm2.17c  43348  jm2.27c  43393  jm3.1lem2  43404  areaquad  43602  sqrtcval  44026  resqrtval  44028  imsqrtval  44029  imo72b2lem0  44550  cvgdvgrat  44698  nzprmdif  44704  lt3addmuld  45692  fperiodmullem  45694  fperiodmul  45695  lt4addmuld  45697  xralrple2  45742  xralrple3  45761  ltmulneg  45779  fmul01  45969  fmuldfeqlem1  45971  fmul01lt1lem1  45973  sumnnodd  46019  ltmod  46025  0ellimcdiv  46036  limclner  46038  dvdivbd  46310  dvbdfbdioolem2  46316  dvbdfbdioo  46317  ioodvbdlimc1lem1  46318  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  stoweidlem1  46388  stoweidlem11  46398  stoweidlem13  46400  stoweidlem14  46401  stoweidlem16  46403  stoweidlem17  46404  stoweidlem22  46409  stoweidlem24  46411  stoweidlem25  46412  stoweidlem26  46413  stoweidlem30  46417  stoweidlem34  46421  stoweidlem36  46423  stoweidlem49  46436  stoweidlem59  46446  stoweidlem60  46447  wallispilem4  46455  wallispilem5  46456  wallispi  46457  wallispi2lem1  46458  wallispi2  46460  stirlinglem1  46461  stirlinglem3  46463  stirlinglem5  46465  stirlinglem6  46466  stirlinglem7  46467  stirlinglem10  46470  stirlinglem11  46471  stirlinglem12  46472  stirlinglem15  46475  stirlingr  46477  dirker2re  46479  dirkerval2  46481  dirkerre  46482  dirkertrigeqlem1  46485  dirkertrigeqlem2  46486  dirkeritg  46489  dirkercncflem2  46491  dirkercncflem4  46493  fourierdlem4  46498  fourierdlem5  46499  fourierdlem6  46500  fourierdlem7  46501  fourierdlem16  46510  fourierdlem18  46512  fourierdlem19  46513  fourierdlem21  46515  fourierdlem22  46516  fourierdlem26  46520  fourierdlem35  46529  fourierdlem39  46533  fourierdlem41  46535  fourierdlem42  46536  fourierdlem43  46537  fourierdlem48  46541  fourierdlem49  46542  fourierdlem51  46544  fourierdlem55  46548  fourierdlem56  46549  fourierdlem57  46550  fourierdlem58  46551  fourierdlem62  46555  fourierdlem63  46556  fourierdlem64  46557  fourierdlem65  46558  fourierdlem66  46559  fourierdlem67  46560  fourierdlem68  46561  fourierdlem71  46564  fourierdlem72  46565  fourierdlem73  46566  fourierdlem76  46569  fourierdlem77  46570  fourierdlem78  46571  fourierdlem83  46576  fourierdlem84  46577  fourierdlem87  46580  fourierdlem88  46581  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  fourierdlem94  46587  fourierdlem95  46588  fourierdlem97  46590  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  fourierdlem113  46606  sqwvfoura  46615  sqwvfourb  46616  fouriersw  46618  etransclem23  46644  etransclem48  46669  rrndistlt  46677  hoidmvlelem1  46982  hoidmvlelem2  46983  hoidmvlelem4  46985  smfmullem1  47178  smfmullem2  47179  smfmullem3  47180  smfmul  47182  fmtno4prmfac  47961  lighneallem4a  47997  requad01  48010  requad1  48011  requad2  48012  perfectALTVlem2  48111  gpg3kgrtriexlem1  48472  gpg3kgrtriexlem4  48475  gpg3kgrtriexlem6  48477  ply1mulgsumlem2  48776  digvalnn0  48988  dignn0fr  48990  dig2nn0  49000  affinecomb1  49091  rrx2linest2  49133  line2  49141  itsclc0lem1  49145  itsclc0lem2  49146  itsclc0lem3  49147  itscnhlc0yqe  49148  itsclc0yqsollem2  49152  itsclc0yqsol  49153  itscnhlc0xyqsol  49154  itsclc0xyqsolr  49158  itsclinecirc0  49162  itsclinecirc0b  49163  itsclinecirc0in  49164  itsclquadb  49165  itsclquadeu  49166  2itscp  49170  itscnhlinecirc02plem1  49171  itscnhlinecirc02p  49174  inlinecirc02plem  49175  amgmwlem  50190