Theorem remulcld 11170

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

Syntax hints:   → wi 4   ∈ wcel 2121  (class class class)co 7360  ℝcr 11032   · cmul 11038

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

This theorem depends on definitions:  df-bi 209  df-an 398

This theorem is referenced by:  mulge0  11663  msqge0  11666  redivcl  11869  prodgt0  11997  ltmul1a  11999  ltmul1  12000  ltmuldiv  12024  lt2msq1  12035  lt2msq  12036  le2msq  12051  msq11  12052  supmul1  12120  supmullem2  12122  supmul  12123  div4p1lem1div2  12427  mul2lt0rlt0  13041  mul2lt0bi  13045  prodge0rd  13046  ge2halflem1  13054  qbtwnre  13146  xmulneg1  13216  xmulf  13219  lincmb01cmp  13443  iccf1o  13444  flmulnn0  13781  flhalf  13784  modcl  13827  mod0  13830  modge0  13833  modmulnn  13843  mulp1mod1  13868  muladdmod  13869  2txmodxeq0  13888  modaddmulmod  13895  moddi  13896  modsubdir  13897  modirr  13899  addmodlteq  13903  bernneq  14186  bernneq3  14188  expnbnd  14189  expmulnbnd  14192  discr1  14196  discr  14197  faclbnd  14247  faclbnd6  14256  remullem  15085  01sqrexlem7  15205  sqrtmul  15216  abstri  15288  sqreulem  15317  bhmafibid1  15425  mulcn2  15553  reccn2  15554  o1rlimmul  15576  lo1mul  15585  iseraltlem2  15640  iseraltlem3  15641  iseralt  15642  o1fsum  15771  cvgcmpce  15776  climcndslem1  15809  climcndslem2  15810  climcnds  15811  geomulcvg  15836  cvgrat  15843  mertenslem1  15844  fprodge1  15955  eftlub  16071  sin02gt0  16154  eirrlem  16166  bitsp1o  16397  2mulprm  16657  isprm5  16672  modprm0  16771  prmreclem3  16884  prmreclem4  16885  prmreclem5  16886  2expltfac  17058  metss2lem  24498  nlmvscnlem2  24672  nrginvrcnlem  24678  nmoco  24724  nmotri  24726  nghmcn  24732  icopnfhmeo  24932  nmoleub2lem3  25104  ipcau2  25223  tcphcphlem1  25224  ipcnlem2  25233  rrxcph  25381  csbren  25388  trirn  25389  pjthlem1  25426  opnmbllem  25590  vitalilem4  25600  itg1val2  25673  itg1cl  25674  itg1ge0  25675  itg1addlem4  25688  itg1mulc  25693  itg1ge0a  25700  itg1climres  25703  mbfi1fseqlem1  25704  mbfi1fseqlem3  25706  mbfi1fseqlem4  25707  mbfi1fseqlem5  25708  mbfi1fseqlem6  25709  itg2const2  25730  itg2mulclem  25735  itg2mulc  25736  itg2monolem1  25739  itg2monolem3  25741  itg2cnlem2  25751  iblconst  25807  iblmulc2  25820  itgmulc2lem1  25821  itgmulc2lem2  25822  bddmulibl  25828  bddiblnc  25831  dveflem  25968  cmvth  25980  dvlip  25982  dvlipcn  25983  dvivthlem1  25997  lhop1lem  26002  dvcvx  26009  dvfsumlem2  26016  dvfsumlem3  26017  dvfsumlem4  26018  dvfsum2  26023  ftc1lem4  26028  plyeq0lem  26197  aalioulem3  26322  aalioulem4  26323  aaliou3lem9  26338  ulmdvlem1  26387  itgulm  26395  radcnvlem1  26400  radcnvlem2  26401  dvradcnv  26408  abelthlem2  26419  abelthlem7  26425  tangtx  26491  tanregt0  26525  logdivlti  26606  logcnlem3  26630  logcnlem4  26631  logccv  26649  recxpcl  26661  cxpmul  26674  cxplt  26680  cxple2  26683  abscxpbnd  26739  lawcoslem1  26801  heron  26824  atans2  26917  efrlim  26955  o1cxp  26960  scvxcvx  26971  jensenlem2  26973  amgmlem  26975  fsumharmonic  26997  lgamgulmlem2  27015  lgamgulmlem3  27016  lgamgulmlem4  27017  lgamgulmlem5  27018  lgamgulmlem6  27019  relgamcl  27047  ftalem1  27058  ftalem2  27059  ftalem5  27062  basellem3  27068  basellem8  27073  chpub  27205  logfacubnd  27206  logfaclbnd  27207  logfacbnd3  27208  logexprlim  27210  perfectlem2  27215  bclbnd  27265  efexple  27266  bposlem1  27269  bposlem2  27270  bposlem6  27274  bposlem9  27277  lgsdilem  27309  gausslemma2dlem0c  27343  gausslemma2dlem2  27352  gausslemma2dlem3  27353  gausslemma2dlem6  27357  lgseisenlem4  27363  lgseisen  27364  lgsquadlem1  27365  lgsquadlem2  27366  2lgslem1a1  27374  2sqmod  27421  chebbnd1lem1  27454  chebbnd1lem3  27456  chtppilimlem1  27458  chpchtlim  27464  vmadivsum  27467  rplogsumlem1  27469  rpvmasumlem  27472  dchrisumlem2  27475  dchrisumlem3  27476  dchrmusum2  27479  dchrvmasumlem2  27483  dchrvmasumiflem1  27486  dchrisum0re  27498  dchrisum0lem1  27501  dirith2  27513  mulogsumlem  27516  mulogsum  27517  mulog2sumlem2  27520  vmalogdivsum2  27523  vmalogdivsum  27524  2vmadivsumlem  27525  logsqvma  27527  logsqvma2  27528  log2sumbnd  27529  selberglem2  27531  selberg  27533  selbergb  27534  selberg2lem  27535  selberg2b  27537  chpdifbndlem1  27538  chpdifbndlem2  27539  selberg3lem1  27542  selberg3lem2  27543  selberg3  27544  selberg4lem1  27545  selberg4  27546  pntrsumbnd2  27552  selberg3r  27554  selberg4r  27555  selberg34r  27556  pntsf  27558  pntsval2  27561  pntrlog2bndlem1  27562  pntrlog2bndlem2  27563  pntrlog2bndlem3  27564  pntrlog2bndlem4  27565  pntrlog2bndlem5  27566  pntrlog2bndlem6  27568  pntrlog2bnd  27569  pntpbnd1a  27570  pntpbnd1  27571  pntpbnd2  27572  pntibndlem2a  27575  pntibndlem2  27576  pntlemb  27582  pntlemr  27587  pntlemj  27588  pntlemf  27590  pntlemk  27591  pntlemo  27592  pntlem3  27594  ostth2lem1  27603  ostth2lem2  27619  ostth2lem3  27620  ostth2lem4  27621  ostth3  27623  ttgcontlem1  28975  brbtwn2  28996  colinearalglem4  29000  axsegconlem8  29015  axsegconlem9  29016  axsegconlem10  29017  ax5seglem3  29022  axpaschlem  29031  axpasch  29032  axeuclidlem  29053  numclwwlk5  30480  numclwwlk7  30483  smcnlem  30790  ubthlem2  30964  htthlem  31010  pjhthlem1  31484  cnlnadjlem7  32166  nmopcoadji  32194  branmfn  32198  leopnmid  32231  nexple  32940  constrremulcl  33963  constrmulcl  33967  cos9thpiminplylem1  33978  cos9thpinconstrlem1  33985  rmulccn  34124  xrge0iifhom  34133  dya2icoseg  34473  eulerpartlems  34556  eulerpartlemgc  34558  eulerpartlemb  34564  plymulx0  34743  signsvtp  34779  reprgt  34817  breprexplemc  34828  circlemethhgt  34839  hgt750lemd  34844  logdivsqrle  34846  hgt750lem  34847  hgt750lemf  34849  hgt750lemb  34852  hgt750lema  34853  hgt750leme  34854  tgoldbachgtde  34856  resconn  35489  knoppcnlem2  36815  knoppcnlem4  36817  knoppcnlem10  36823  unbdqndv2lem1  36830  unbdqndv2lem2  36831  knoppndvlem1  36833  knoppndvlem11  36843  knoppndvlem12  36844  knoppndvlem14  36846  knoppndvlem15  36847  knoppndvlem17  36849  knoppndvlem18  36850  knoppndvlem19  36851  knoppndvlem20  36852  knoppndvlem21  36853  opnmbllem0  38038  itg2addnclem2  38054  itg2addnclem3  38055  iblmulc2nc  38067  itgmulc2nclem1  38068  ftc1cnnclem  38073  ftc1anclem3  38077  areacirclem4  38093  geomcau  38141  equivbnd  38172  bfplem1  38204  bfplem2  38205  bfp  38206  rrnequiv  38217  rrntotbnd  38218  lcmineqlem19  42547  lcmineqlem20  42548  lcmineqlem21  42549  lcmineqlem22  42550  3lexlogpow2ineq2  42559  dvrelogpow2b  42568  aks4d1p1p2  42570  aks4d1p1p4  42571  aks4d1p1p6  42573  aks4d1p1p7  42574  aks4d1p1p5  42575  aks4d1p1  42576  aks4d1p8d2  42585  aks4d1p8  42587  posbezout  42600  aks6d1c2lem4  42627  2np3bcnp1  42644  2ap1caineq  42645  aks6d1c6lem4  42673  aks6d1c7lem1  42680  aks6d1c7lem2  42681  resubdi  42888  remul02  42897  remul01  42899  remulinvcom  42925  rediveud  42935  redivcan3d  42940  redivrec2d  42952  rediv23d  42953  sn-0tie0  42956  renegmulnnass  42970  mulgt0con1d  42975  mulgt0con2d  42976  mulgt0b1d  42977  sn-ltmul2d  42978  mulgt0b2d  42983  sn-mulgt1d  42984  mulltgt0d  42987  mullt0b1d  42988  mullt0b2d  42989  sn-mullt0d  42990  sn-itrere  42993  sn-retire  42994  fltnltalem  43127  fltnlta  43128  3cubeslem2  43149  3cubeslem3r  43151  3cubeslem4  43153  irrapxlem1  43282  irrapxlem2  43283  irrapxlem3  43284  irrapxlem4  43285  irrapxlem5  43286  pellexlem2  43290  pellexlem6  43294  pell14qrgt0  43319  pell1qrge1  43330  pell1qrgaplem  43333  pellqrexplicit  43337  pellqrex  43339  rmspecsqrtnq  43366  rmxycomplete  43377  rmxypos  43407  ltrmynn0  43408  ltrmxnn0  43409  jm2.24nn  43419  jm2.17a  43420  jm2.17b  43421  jm2.17c  43422  jm2.27c  43467  jm3.1lem2  43478  areaquad  43676  sqrtcval  44100  resqrtval  44102  imsqrtval  44103  imo72b2lem0  44624  cvgdvgrat  44772  nzprmdif  44778  lt3addmuld  45763  fperiodmullem  45765  fperiodmul  45766  lt4addmuld  45768  xralrple2  45813  xralrple3  45832  ltmulneg  45850  fmul01  46039  fmuldfeqlem1  46041  fmul01lt1lem1  46043  sumnnodd  46089  ltmod  46095  0ellimcdiv  46106  limclner  46108  dvdivbd  46380  dvbdfbdioolem2  46386  dvbdfbdioo  46387  ioodvbdlimc1lem1  46388  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  stoweidlem1  46458  stoweidlem11  46468  stoweidlem13  46470  stoweidlem14  46471  stoweidlem16  46473  stoweidlem17  46474  stoweidlem22  46479  stoweidlem24  46481  stoweidlem25  46482  stoweidlem26  46483  stoweidlem30  46487  stoweidlem34  46491  stoweidlem36  46493  stoweidlem49  46506  stoweidlem59  46516  stoweidlem60  46517  wallispilem4  46525  wallispilem5  46526  wallispi  46527  wallispi2lem1  46528  wallispi2  46530  stirlinglem1  46531  stirlinglem3  46533  stirlinglem5  46535  stirlinglem6  46536  stirlinglem7  46537  stirlinglem10  46540  stirlinglem11  46541  stirlinglem12  46542  stirlinglem15  46545  stirlingr  46547  dirker2re  46549  dirkerval2  46551  dirkerre  46552  dirkertrigeqlem1  46555  dirkertrigeqlem2  46556  dirkeritg  46559  dirkercncflem2  46561  dirkercncflem4  46563  fourierdlem4  46568  fourierdlem5  46569  fourierdlem6  46570  fourierdlem7  46571  fourierdlem16  46580  fourierdlem18  46582  fourierdlem19  46583  fourierdlem21  46585  fourierdlem22  46586  fourierdlem26  46590  fourierdlem35  46599  fourierdlem39  46603  fourierdlem41  46605  fourierdlem42  46606  fourierdlem43  46607  fourierdlem48  46611  fourierdlem49  46612  fourierdlem51  46614  fourierdlem55  46618  fourierdlem56  46619  fourierdlem57  46620  fourierdlem58  46621  fourierdlem62  46625  fourierdlem63  46626  fourierdlem64  46627  fourierdlem65  46628  fourierdlem66  46629  fourierdlem67  46630  fourierdlem68  46631  fourierdlem71  46634  fourierdlem72  46635  fourierdlem73  46636  fourierdlem76  46639  fourierdlem77  46640  fourierdlem78  46641  fourierdlem83  46646  fourierdlem84  46647  fourierdlem87  46650  fourierdlem88  46651  fourierdlem89  46652  fourierdlem90  46653  fourierdlem91  46654  fourierdlem94  46657  fourierdlem95  46658  fourierdlem97  46660  fourierdlem103  46666  fourierdlem104  46667  fourierdlem112  46675  fourierdlem113  46676  sqwvfoura  46685  sqwvfourb  46686  fouriersw  46688  etransclem23  46714  etransclem48  46739  rrndistlt  46747  hoidmvlelem1  47052  hoidmvlelem2  47053  hoidmvlelem4  47055  smfmullem1  47248  smfmullem2  47249  smfmullem3  47250  smfmul  47252  2timesltsqm1  47856  fmtno4prmfac  48064  lighneallem4a  48100  requad01  48126  requad1  48127  requad2  48128  perfectALTVlem2  48227  gpg3kgrtriexlem1  48588  gpg3kgrtriexlem4  48591  gpg3kgrtriexlem6  48593  ply1mulgsumlem2  48892  digvalnn0  49104  dignn0fr  49106  dig2nn0  49116  affinecomb1  49207  rrx2linest2  49249  line2  49257  itsclc0lem1  49261  itsclc0lem2  49262  itsclc0lem3  49263  itscnhlc0yqe  49264  itsclc0yqsollem2  49268  itsclc0yqsol  49269  itscnhlc0xyqsol  49270  itsclc0xyqsolr  49274  itsclinecirc0  49278  itsclinecirc0b  49279  itsclinecirc0in  49280  itsclquadb  49281  itsclquadeu  49282  2itscp  49286  itscnhlinecirc02plem1  49287  itscnhlinecirc02p  49290  inlinecirc02plem  49291  amgmwlem  50306