Theorem remulcl 11269

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183   · cmul 11189

This theorem was proved from axioms:  ax-mulrcl 11247

This theorem is referenced by:  1re  11290  remulcli  11306  remulcld  11320  axmulgt0  11364  00id  11465  mul02lem1  11466  recextlem2  11921  recex  11922  lemul1  12146  ltmul12a  12150  lemul12b  12151  mulgt1OLD  12153  mulgt1  12156  mulge0b  12165  mulle0b  12166  ltdivmul  12170  ledivmul  12171  lt2mul2div  12173  lemuldiv  12175  ltdiv23  12186  lediv23  12187  supmullem2  12266  cju  12289  addltmul  12529  zmulcl  12692  irrmul  13039  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  rpmulcl  13080  xmulasslem3  13348  xadddilem  13356  ge0mulcl  13521  iccdil  13550  mulmod0  13928  modmulnn  13940  modcyc  13957  modmul1  13975  modaddmulmod  13989  moddi  13990  addmodlteq  13997  reexpcl  14129  reexpclz  14133  expge0  14149  expge1  14150  expubnd  14227  bernneq  14278  expmulnbnd  14284  digit2  14285  digit1  14286  discr  14289  faclbnd  14339  faclbnd3  14341  faclbnd5  14347  facavg  14350  cshweqrep  14869  crre  15163  remim  15166  mulre  15170  01sqrexlem6  15296  01sqrexlem7  15297  sqreulem  15408  amgm2  15418  o1mul  15661  caucvgrlem  15721  climcndslem2  15898  climcnds  15899  fprodrecl  16001  fprodreclf  16007  iprodrecl  16050  rerisefaccl  16065  refallfaccl  16066  efcllem  16125  ege2le3  16138  ef01bndlem  16232  cos01gt0  16239  modprm0  16852  prmreclem3  16965  4sqlem11  17002  resubdrg  21649  nmoco  24779  nghmco  24780  blcvx  24839  iihalf1  24977  iihalf2  24980  iimulcl  24985  pcoass  25076  tcphcphlem1  25288  csbren  25452  trirn  25453  minveclem2  25479  sca2rab  25566  uniioombllem5  25641  mbfmulc2lem  25701  i1fmul  25750  i1fmulclem  25757  i1fmulc  25758  dveflem  26037  cmvth  26049  cmvthOLD  26050  dvivthlem1  26067  dvfsumle  26080  dvfsumleOLD  26081  dvfsumlem2  26087  dvfsumlem2OLD  26088  pilem2  26514  tangtx  26565  sinq12gt0  26567  coskpi  26583  cosne0  26589  efif1olem2  26603  efif1olem4  26605  relogexp  26656  logcxp  26729  rpcxpcl  26736  abscxpbnd  26814  ang180lem1  26870  atantan  26984  atanbndlem  26986  o1cxp  27036  divsqrtsumlem  27041  jensenlem2  27049  jensen  27050  zetacvg  27076  regamcl  27122  basellem1  27142  basellem4  27145  basellem9  27150  chtublem  27273  chtub  27274  logfaclbnd  27284  bpos1lem  27344  bposlem1  27346  bposlem2  27347  bposlem6  27351  bposlem7  27352  bposlem9  27354  lgseisen  27441  chebbnd1lem2  27532  chebbnd1lem3  27533  chto1ub  27538  rplogsumlem1  27546  dchrisumlem3  27553  dchrvmasumlem2  27560  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2  27580  mulog2sumlem1  27596  mulog2sumlem2  27597  log2sumbnd  27606  selberglem2  27608  chpdifbndlem1  27615  logdivbnd  27618  pntrlog2bndlem4  27642  pntibndlem2  27653  pntibndlem3  27654  pntlemh  27661  pntlemr  27664  pntlemk  27668  pntlemo  27669  ostth2lem1  27680  ostth2lem3  27697  ostth3  27700  axcontlem2  28998  nmoub3i  30805  blocni  30837  ubthlem3  30904  minvecolem2  30907  bcs2  31214  nmopub2tALT  31941  nmfnleub2  31958  nmophmi  32063  bdophmi  32064  lnconi  32065  cnlnadjlem2  32100  cnlnadjlem7  32105  nmopadjlem  32121  nmopcoadji  32133  leopnmid  32170  cdj1i  32465  cdj3lem2b  32469  cdj3i  32473  addltmulALT  32478  pnfinf  33163  rezh  33917  sgnmul  34507  sgnmulsgn  34514  sgnmulsgp  34515  signshf  34565  knoppndvlem15  36492  knoppndvlem21  36498  itg2addnclem  37631  ftc1anclem3  37655  isbnd2  37743  isbnd3  37744  equivbnd  37750  aks6d1c7lem1  42137  2xp3dxp2ge1d  42198  resubdi  42372  pellexlem5  42789  pell1234qrmulcl  42811  pellfundex  42842  rmspecsqrtnq  42862  jm2.24nn  42916  jm2.17a  42917  jm2.17b  42918  jm2.17c  42919  acongrep  42937  acongeq  42940  jm3.1lem2  42975  mulltgt0  44922  ltdiv23neg  45309  fmul01  45501  fmuldfeq  45504  fmul01lt1lem1  45505  fmul01lt1lem2  45506  stoweidlem3  45924  stoweidlem13  45934  stoweidlem17  45938  stoweidlem34  45955  stoweidlem42  45963  stoweidlem48  45969  fourierdlem83  46110  hoidmvlelem2  46517  smfmullem1  46712  2leaddle2  47213  itsclc0lem1  48490  amgmwlem  48896