Theorem remulcld 11288

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151   · cmul 11157

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

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

This theorem is referenced by:  mulge0  11778  msqge0  11781  redivcl  11983  prodgt0  12111  ltmul1a  12113  ltmul1  12114  ltmuldiv  12138  lt2msq1  12149  lt2msq  12150  le2msq  12165  msq11  12166  supmul1  12234  supmullem2  12236  supmul  12237  div4p1lem1div2  12518  mul2lt0rlt0  13134  mul2lt0bi  13138  prodge0rd  13139  ge2halflem1  13147  qbtwnre  13237  xmulneg1  13307  xmulf  13310  lincmb01cmp  13531  iccf1o  13532  flmulnn0  13863  flhalf  13866  modcl  13909  mod0  13912  modge0  13915  modmulnn  13925  mulp1mod1  13948  muladdmod  13949  2txmodxeq0  13968  modaddmulmod  13975  moddi  13976  modsubdir  13977  modirr  13979  addmodlteq  13983  bernneq  14264  bernneq3  14266  expnbnd  14267  expmulnbnd  14270  discr1  14274  discr  14275  faclbnd  14325  faclbnd6  14334  remullem  15163  01sqrexlem7  15283  sqrtmul  15294  abstri  15365  sqreulem  15394  bhmafibid1  15500  mulcn2  15628  reccn2  15629  o1rlimmul  15651  lo1mul  15660  iseraltlem2  15715  iseraltlem3  15716  iseralt  15717  o1fsum  15845  cvgcmpce  15850  climcndslem1  15881  climcndslem2  15882  climcnds  15883  geomulcvg  15908  cvgrat  15915  mertenslem1  15916  fprodge1  16027  eftlub  16141  sin02gt0  16224  eirrlem  16236  bitsp1o  16466  2mulprm  16726  isprm5  16740  modprm0  16838  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  2expltfac  17126  metss2lem  24539  nlmvscnlem2  24721  nrginvrcnlem  24727  nmoco  24773  nmotri  24775  nghmcn  24781  icopnfhmeo  24987  nmoleub2lem3  25161  ipcau2  25281  tcphcphlem1  25282  ipcnlem2  25291  rrxcph  25439  csbren  25446  trirn  25447  pjthlem1  25484  opnmbllem  25649  vitalilem4  25659  itg1val2  25732  itg1cl  25733  itg1ge0  25734  itg1addlem4  25747  itg1addlem4OLD  25748  itg1mulc  25753  itg1ge0a  25760  itg1climres  25763  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2const2  25790  itg2mulclem  25795  itg2mulc  25796  itg2monolem1  25799  itg2monolem3  25801  itg2cnlem2  25811  iblconst  25867  iblmulc2  25880  itgmulc2lem1  25881  itgmulc2lem2  25882  bddmulibl  25888  bddiblnc  25891  dveflem  26031  cmvth  26043  cmvthOLD  26044  dvlip  26046  dvlipcn  26047  dvivthlem1  26061  lhop1lem  26066  dvcvx  26073  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  ftc1lem4  26094  plyeq0lem  26263  aalioulem3  26390  aalioulem4  26391  aaliou3lem9  26406  ulmdvlem1  26457  itgulm  26465  radcnvlem1  26470  radcnvlem2  26471  dvradcnv  26478  abelthlem2  26490  abelthlem7  26496  tangtx  26561  tanregt0  26595  logdivlti  26676  logcnlem3  26700  logcnlem4  26701  logccv  26719  recxpcl  26731  cxpmul  26744  cxplt  26750  cxple2  26753  abscxpbnd  26810  lawcoslem1  26872  heron  26895  atans2  26988  efrlim  27026  efrlimOLD  27027  o1cxp  27032  scvxcvx  27043  jensenlem2  27045  amgmlem  27047  fsumharmonic  27069  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  relgamcl  27119  ftalem1  27130  ftalem2  27131  ftalem5  27134  basellem3  27140  basellem8  27145  chpub  27278  logfacubnd  27279  logfaclbnd  27280  logfacbnd3  27281  logexprlim  27283  perfectlem2  27288  bclbnd  27338  efexple  27339  bposlem1  27342  bposlem2  27343  bposlem6  27347  bposlem9  27350  lgsdilem  27382  gausslemma2dlem0c  27416  gausslemma2dlem2  27425  gausslemma2dlem3  27426  gausslemma2dlem6  27430  lgseisenlem4  27436  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  2lgslem1a1  27447  2sqmod  27494  chebbnd1lem1  27527  chebbnd1lem3  27529  chtppilimlem1  27531  chpchtlim  27537  vmadivsum  27540  rplogsumlem1  27542  rpvmasumlem  27545  dchrisumlem2  27548  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0re  27571  dchrisum0lem1  27574  dirith2  27586  mulogsumlem  27589  mulogsum  27590  mulog2sumlem2  27593  vmalogdivsum2  27596  vmalogdivsum  27597  2vmadivsumlem  27598  logsqvma  27600  logsqvma2  27601  log2sumbnd  27602  selberglem2  27604  selberg  27606  selbergb  27607  selberg2lem  27608  selberg2b  27610  chpdifbndlem1  27611  chpdifbndlem2  27612  selberg3lem1  27615  selberg3lem2  27616  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrsumbnd2  27625  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntsf  27631  pntsval2  27634  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2a  27648  pntibndlem2  27649  pntlemb  27655  pntlemr  27660  pntlemj  27661  pntlemf  27663  pntlemk  27664  pntlemo  27665  pntlem3  27667  ostth2lem1  27676  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ostth3  27696  ttgcontlem1  28913  brbtwn2  28934  colinearalglem4  28938  axsegconlem8  28953  axsegconlem9  28954  axsegconlem10  28955  ax5seglem3  28960  axpaschlem  28969  axpasch  28970  axeuclidlem  28991  numclwwlk5  30416  numclwwlk7  30419  smcnlem  30725  ubthlem2  30899  htthlem  30945  pjhthlem1  31419  cnlnadjlem7  32101  nmopcoadji  32129  branmfn  32133  leopnmid  32166  rmulccn  33888  xrge0iifhom  33897  nexple  33989  dya2icoseg  34258  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemb  34349  plymulx0  34540  signsvtp  34576  reprgt  34614  breprexplemc  34625  circlemethhgt  34636  hgt750lemd  34641  logdivsqrle  34643  hgt750lem  34644  hgt750lemf  34646  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  resconn  35230  knoppcnlem2  36476  knoppcnlem4  36478  knoppcnlem10  36484  unbdqndv2lem1  36491  unbdqndv2lem2  36492  knoppndvlem1  36494  knoppndvlem11  36504  knoppndvlem12  36505  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem18  36511  knoppndvlem19  36512  knoppndvlem20  36513  knoppndvlem21  36514  opnmbllem0  37642  itg2addnclem2  37658  itg2addnclem3  37659  iblmulc2nc  37671  itgmulc2nclem1  37672  ftc1cnnclem  37677  ftc1anclem3  37681  areacirclem4  37697  geomcau  37745  equivbnd  37776  bfplem1  37808  bfplem2  37809  bfp  37810  rrnequiv  37821  rrntotbnd  37822  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem21  42030  lcmineqlem22  42031  3lexlogpow2ineq2  42040  dvrelogpow2b  42049  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p8d2  42066  aks4d1p8  42068  posbezout  42081  aks6d1c2lem4  42108  2np3bcnp1  42125  2ap1caineq  42126  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7lem2  42162  resubdi  42402  remul02  42411  remul01  42413  remulinvcom  42438  sn-0tie0  42445  renegmulnnass  42459  mulgt0con1d  42464  mulgt0con2d  42465  mulgt0b2d  42466  sn-ltmul2d  42467  sn-mulgt1d  42471  sn-inelr  42473  sn-itrere  42474  sn-retire  42475  fltnltalem  42648  fltnlta  42649  3cubeslem2  42672  3cubeslem3r  42674  3cubeslem4  42676  irrapxlem1  42809  irrapxlem2  42810  irrapxlem3  42811  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  pell14qrgt0  42846  pell1qrge1  42857  pell1qrgaplem  42860  pellqrexplicit  42864  pellqrex  42866  rmspecsqrtnq  42893  rmxycomplete  42905  rmxypos  42935  ltrmynn0  42936  ltrmxnn0  42937  jm2.24nn  42947  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  jm2.27c  42995  jm3.1lem2  43006  areaquad  43204  sqrtcval  43630  resqrtval  43632  imsqrtval  43633  imo72b2lem0  44154  cvgdvgrat  44308  nzprmdif  44314  lt3addmuld  45251  fperiodmullem  45253  fperiodmul  45254  lt4addmuld  45256  xralrple2  45303  xralrple3  45323  ltmulneg  45341  fmul01  45535  fmuldfeqlem1  45537  fmul01lt1lem1  45539  sumnnodd  45585  ltmod  45593  0ellimcdiv  45604  limclner  45606  dvdivbd  45878  dvbdfbdioolem2  45884  dvbdfbdioo  45885  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem1  45956  stoweidlem11  45966  stoweidlem13  45968  stoweidlem14  45969  stoweidlem16  45971  stoweidlem17  45972  stoweidlem22  45977  stoweidlem24  45979  stoweidlem25  45980  stoweidlem26  45981  stoweidlem30  45985  stoweidlem34  45989  stoweidlem36  45991  stoweidlem49  46004  stoweidlem59  46014  stoweidlem60  46015  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem15  46043  stirlingr  46045  dirker2re  46047  dirkerval2  46049  dirkerre  46050  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkeritg  46057  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem4  46066  fourierdlem5  46067  fourierdlem6  46068  fourierdlem7  46069  fourierdlem16  46078  fourierdlem18  46080  fourierdlem19  46081  fourierdlem21  46083  fourierdlem22  46084  fourierdlem26  46088  fourierdlem35  46097  fourierdlem39  46101  fourierdlem41  46103  fourierdlem42  46104  fourierdlem43  46105  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem55  46116  fourierdlem56  46117  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem66  46127  fourierdlem67  46128  fourierdlem68  46129  fourierdlem71  46132  fourierdlem72  46133  fourierdlem73  46134  fourierdlem76  46137  fourierdlem77  46138  fourierdlem78  46139  fourierdlem83  46144  fourierdlem84  46145  fourierdlem87  46148  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem94  46155  fourierdlem95  46156  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  etransclem23  46212  etransclem48  46237  rrndistlt  46245  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem4  46553  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  smfmul  46750  fmtno4prmfac  47496  lighneallem4a  47532  requad01  47545  requad1  47546  requad2  47547  perfectALTVlem2  47646  ply1mulgsumlem2  48232  digvalnn0  48448  dignn0fr  48450  dig2nn0  48460  affinecomb1  48551  rrx2linest2  48593  line2  48601  itsclc0lem1  48605  itsclc0lem2  48606  itsclc0lem3  48607  itscnhlc0yqe  48608  itsclc0yqsollem2  48612  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itsclc0xyqsolr  48618  itsclinecirc0  48622  itsclinecirc0b  48623  itsclinecirc0in  48624  itsclquadb  48625  itsclquadeu  48626  2itscp  48630  itscnhlinecirc02plem1  48631  itscnhlinecirc02p  48634  inlinecirc02plem  48635  amgmwlem  49032