Theorem remulcl 11324

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

Assertion

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

Proof of Theorem remulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238   · cmul 11244

This proof depends on axioms:  ax-mulrcl 11302

This theorem is used by:  1re  11347  remulcli  11364  remulcld  11378  axmulgt0  11423  00id  11524  mul02lem1  11525  recextlem2  11987  recex  11988  lemul1  12209  ltmul12a  12213  lemul12b  12214  mulgt1  12218  mulge0b  12227  mulle0b  12228  ltdivmul  12232  ledivmul  12233  lt2mul2div  12235  lemuldiv  12237  ltdiv23  12248  lediv23  12249  supmullem2  12328  cju  12356  addltmul  12622  zmulcl  12785  irrmul  13142  rpnnen1lem2  13145  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  rpmulcl  13185  xmulasslem3  13456  xadddilem  13464  ge0mulcl  13632  iccdil  13661  mulmod0  14057  modmulnn  14069  modcyc  14086  modmul1  14107  modaddmulmod  14121  moddi  14122  addmodlteq  14129  reexpcl  14261  reexpclz  14265  expge0  14281  expge1  14282  expubnd  14361  bernneq  14414  expmulnbnd  14420  digit2  14421  digit1  14422  discr  14425  faclbnd  14475  faclbnd3  14477  faclbnd5  14483  facavg  14486  cshweqrep  15014  sgnmul  15303  sgnmulsgn  15305  crre  15324  remim  15327  mulre  15331  01sqrexlem6  15457  01sqrexlem7  15458  sqreulem  15571  amgm2  15581  o1mul  15826  caucvgrlem  15884  climcndslem2  16063  climcnds  16064  fprodrecl  16164  fprodreclf  16170  iprodrecl  16213  rerisefaccl  16228  refallfaccl  16229  efcllem  16287  ege2le3  16300  ef01bndlem  16396  cos01gt0  16403  modprm0  17027  prmreclem3  17140  4sqlem11  17177  resubdrg  21969  nmoco  25111  nghmco  25112  blcvx  25172  iihalf1  25307  iihalf2  25309  iimulcl  25313  pcoass  25400  tcphcphlem1  25611  csbren  25775  trirn  25776  minveclem2  25802  sca2rab  25888  uniioombllem5  25963  mbfmulc2lem  26023  i1fmul  26072  i1fmulclem  26078  i1fmulc  26079  dveflem  26354  cmvth  26366  dvivthlem1  26383  dvfsumle  26396  dvfsumlem2  26402  pilem2  26836  tangtx  26891  sinq12gt0  26893  coskpi  26908  cosne0  26914  efif1olem2  26928  efif1olem4  26930  relogexp  26981  logcxp  27054  rpcxpcl  27061  abscxpbnd  27138  ang180lem1  27194  atantan  27308  atanbndlem  27310  o1cxp  27359  divsqrtsumlem  27364  jensenlem2  27372  jensen  27373  zetacvg  27399  regamcl  27445  basellem1  27465  basellem4  27468  basellem9  27473  chtublem  27595  chtub  27596  logfaclbnd  27606  bpos1lem  27666  bposlem1  27668  bposlem2  27669  bposlem6  27673  bposlem7  27674  bposlem9  27676  lgseisen  27763  chebbnd1lem2  27854  chebbnd1lem3  27855  chto1ub  27860  rplogsumlem1  27868  dchrisumlem3  27875  dchrvmasumlem2  27882  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2  27902  mulog2sumlem1  27918  mulog2sumlem2  27919  log2sumbnd  27928  selberglem2  27930  chpdifbndlem1  27937  logdivbnd  27940  pntrlog2bndlem4  27964  pntibndlem2  27975  pntibndlem3  27976  pntlemh  27983  pntlemr  27986  pntlemk  27990  pntlemo  27991  ostth2lem1  28002  ostth2lem3  28019  ostth3  28022  axcontlem2  29600  nmoub3i  31432  blocni  31464  ubthlem3  31531  minvecolem2  31534  bcs2  31841  nmopub2tALT  32568  nmfnleub2  32585  nmophmi  32690  bdophmi  32691  lnconi  32692  cnlnadjlem2  32727  cnlnadjlem7  32732  nmopadjlem  32748  nmopcoadji  32760  leopnmid  32797  cdj1i  33092  cdj3lem2b  33096  cdj3i  33100  addltmulALT  33147  sgnmulsgp  33519  pnfinf  33843  rezh  34712  signshf  35328  knoppndvlem15  37607  knoppndvlem21  37613  itg2addnclem  38857  ftc1anclem3  38881  isbnd2  38983  isbnd3  38984  equivbnd  38990  aks6d1c7lem1  43496  resubdi  43713  pellexlem5  44106  pell1234qrmulcl  44128  pellfundex  44159  rmspecsqrtnq  44179  jm2.24nn  44232  jm2.17a  44233  jm2.17b  44234  jm2.17c  44235  acongrep  44253  acongeq  44256  jm3.1lem2  44291  mulltgt0  46313  ltdiv23neg  46678  fmul01  46865  fmuldfeq  46868  fmul01lt1lem1  46869  fmul01lt1lem2  46870  stoweidlem3  47286  stoweidlem13  47296  stoweidlem17  47300  stoweidlem34  47317  stoweidlem42  47325  stoweidlem48  47331  fourierdlem83  47472  hoidmvlelem2  47879  smfmullem1  48074  2leaddle2  48641  itsclc0lem1  50199  crosspaltd  51394  amgmwlem  51415