Theorem remulcl 11102

Description: Alias for ax-mulrcl 11080, for naming consistency with remulcli 11139. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
remulcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcl

Step	Hyp	Ref	Expression
1		ax-mulrcl 11080	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7355  ℝcr 11016   · cmul 11022

This theorem was proved from axioms:  ax-mulrcl 11080

This theorem is referenced by:  1re  11123  remulcli  11139  remulcld  11153  axmulgt0  11198  00id  11299  mul02lem1  11300  recextlem2  11759  recex  11760  lemul1  11984  ltmul12a  11988  lemul12b  11989  mulgt1OLD  11991  mulgt1  11994  mulge0b  12003  mulle0b  12004  ltdivmul  12008  ledivmul  12009  lt2mul2div  12011  lemuldiv  12013  ltdiv23  12024  lediv23  12025  supmullem2  12104  cju  12132  addltmul  12368  zmulcl  12531  irrmul  12878  rpnnen1lem2  12881  rpnnen1lem1  12882  rpnnen1lem3  12883  rpnnen1lem5  12885  rpmulcl  12921  xmulasslem3  13192  xadddilem  13200  ge0mulcl  13368  iccdil  13397  mulmod0  13788  modmulnn  13800  modcyc  13817  modmul1  13838  modaddmulmod  13852  moddi  13853  addmodlteq  13860  reexpcl  13992  reexpclz  13996  expge0  14012  expge1  14013  expubnd  14092  bernneq  14143  expmulnbnd  14149  digit2  14150  digit1  14151  discr  14154  faclbnd  14204  faclbnd3  14206  faclbnd5  14212  facavg  14215  cshweqrep  14735  crre  15028  remim  15031  mulre  15035  01sqrexlem6  15161  01sqrexlem7  15162  sqreulem  15274  amgm2  15284  o1mul  15529  caucvgrlem  15587  climcndslem2  15764  climcnds  15765  fprodrecl  15867  fprodreclf  15873  iprodrecl  15916  rerisefaccl  15931  refallfaccl  15932  efcllem  15991  ege2le3  16004  ef01bndlem  16100  cos01gt0  16107  modprm0  16724  prmreclem3  16837  4sqlem11  16874  resubdrg  21554  nmoco  24672  nghmco  24673  blcvx  24733  iihalf1  24872  iihalf2  24875  iimulcl  24880  pcoass  24971  tcphcphlem1  25182  csbren  25346  trirn  25347  minveclem2  25373  sca2rab  25460  uniioombllem5  25535  mbfmulc2lem  25595  i1fmul  25644  i1fmulclem  25650  i1fmulc  25651  dveflem  25930  cmvth  25942  cmvthOLD  25943  dvivthlem1  25960  dvfsumle  25973  dvfsumleOLD  25974  dvfsumlem2  25980  dvfsumlem2OLD  25981  pilem2  26409  tangtx  26461  sinq12gt0  26463  coskpi  26479  cosne0  26485  efif1olem2  26499  efif1olem4  26501  relogexp  26552  logcxp  26625  rpcxpcl  26632  abscxpbnd  26710  ang180lem1  26766  atantan  26880  atanbndlem  26882  o1cxp  26932  divsqrtsumlem  26937  jensenlem2  26945  jensen  26946  zetacvg  26972  regamcl  27018  basellem1  27038  basellem4  27041  basellem9  27046  chtublem  27169  chtub  27170  logfaclbnd  27180  bpos1lem  27240  bposlem1  27242  bposlem2  27243  bposlem6  27247  bposlem7  27248  bposlem9  27250  lgseisen  27337  chebbnd1lem2  27428  chebbnd1lem3  27429  chto1ub  27434  rplogsumlem1  27442  dchrisumlem3  27449  dchrvmasumlem2  27456  dchrisum0lem1b  27473  dchrisum0lem1  27474  dchrisum0lem2  27476  mulog2sumlem1  27492  mulog2sumlem2  27493  log2sumbnd  27502  selberglem2  27504  chpdifbndlem1  27511  logdivbnd  27514  pntrlog2bndlem4  27538  pntibndlem2  27549  pntibndlem3  27550  pntlemh  27557  pntlemr  27560  pntlemk  27564  pntlemo  27565  ostth2lem1  27576  ostth2lem3  27593  ostth3  27596  axcontlem2  28964  nmoub3i  30774  blocni  30806  ubthlem3  30873  minvecolem2  30876  bcs2  31183  nmopub2tALT  31910  nmfnleub2  31927  nmophmi  32032  bdophmi  32033  lnconi  32034  cnlnadjlem2  32069  cnlnadjlem7  32074  nmopadjlem  32090  nmopcoadji  32102  leopnmid  32139  cdj1i  32434  cdj3lem2b  32438  cdj3i  32442  addltmulALT  32447  sgnmul  32844  sgnmulsgn  32851  sgnmulsgp  32852  pnfinf  33193  rezh  34054  signshf  34673  knoppndvlem15  36642  knoppndvlem21  36648  itg2addnclem  37784  ftc1anclem3  37808  isbnd2  37896  isbnd3  37897  equivbnd  37903  aks6d1c7lem1  42346  resubdi  42566  pellexlem5  42990  pell1234qrmulcl  43012  pellfundex  43043  rmspecsqrtnq  43063  jm2.24nn  43116  jm2.17a  43117  jm2.17b  43118  jm2.17c  43119  acongrep  43137  acongeq  43140  jm3.1lem2  43175  mulltgt0  45183  ltdiv23neg  45554  fmul01  45742  fmuldfeq  45745  fmul01lt1lem1  45746  fmul01lt1lem2  45747  stoweidlem3  46163  stoweidlem13  46173  stoweidlem17  46177  stoweidlem34  46194  stoweidlem42  46202  stoweidlem48  46208  fourierdlem83  46349  hoidmvlelem2  46756  smfmullem1  46951  2leaddle2  47460  itsclc0lem1  48918  amgmwlem  49963