Theorem remulcl 11278

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

Assertion

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

Proof of Theorem remulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7418  ℝcr 11192   · cmul 11198

This proof depends on axioms:  ax-mulrcl 11256

This theorem is used by:  1re  11301  remulcli  11318  remulcld  11332  axmulgt0  11377  00id  11478  mul02lem1  11479  recextlem2  11940  recex  11941  lemul1  12162  ltmul12a  12166  lemul12b  12167  mulgt1  12171  mulge0b  12180  mulle0b  12181  ltdivmul  12185  ledivmul  12186  lt2mul2div  12188  lemuldiv  12190  ltdiv23  12201  lediv23  12202  supmullem2  12281  cju  12309  addltmul  12575  zmulcl  12738  irrmul  13095  rpnnen1lem2  13098  rpnnen1lem1  13099  rpnnen1lem3  13100  rpnnen1lem5  13102  rpmulcl  13138  xmulasslem3  13409  xadddilem  13417  ge0mulcl  13585  iccdil  13614  mulmod0  14010  modmulnn  14022  modcyc  14039  modmul1  14060  modaddmulmod  14074  moddi  14075  addmodlteq  14082  reexpcl  14214  reexpclz  14218  expge0  14234  expge1  14235  expubnd  14314  bernneq  14366  expmulnbnd  14372  digit2  14373  digit1  14374  discr  14377  faclbnd  14427  faclbnd3  14429  faclbnd5  14435  facavg  14438  cshweqrep  14965  sgnmul  15253  sgnmulsgn  15255  crre  15274  remim  15277  mulre  15281  01sqrexlem6  15407  01sqrexlem7  15408  sqreulem  15520  amgm2  15530  o1mul  15775  caucvgrlem  15833  climcndslem2  16012  climcnds  16013  fprodrecl  16113  fprodreclf  16119  iprodrecl  16162  rerisefaccl  16177  refallfaccl  16178  efcllem  16236  ege2le3  16249  ef01bndlem  16345  cos01gt0  16352  modprm0  16976  prmreclem3  17089  4sqlem11  17126  resubdrg  21907  nmoco  25049  nghmco  25050  blcvx  25110  iihalf1  25245  iihalf2  25247  iimulcl  25251  pcoass  25338  tcphcphlem1  25549  csbren  25713  trirn  25714  minveclem2  25740  sca2rab  25826  uniioombllem5  25901  mbfmulc2lem  25961  i1fmul  26010  i1fmulclem  26016  i1fmulc  26017  dveflem  26292  cmvth  26304  dvivthlem1  26321  dvfsumle  26334  dvfsumlem2  26340  pilem2  26772  tangtx  26827  sinq12gt0  26829  coskpi  26844  cosne0  26850  efif1olem2  26864  efif1olem4  26866  relogexp  26917  logcxp  26990  rpcxpcl  26997  abscxpbnd  27074  ang180lem1  27130  atantan  27244  atanbndlem  27246  o1cxp  27295  divsqrtsumlem  27300  jensenlem2  27308  jensen  27309  zetacvg  27335  regamcl  27381  basellem1  27401  basellem4  27404  basellem9  27409  chtublem  27531  chtub  27532  logfaclbnd  27542  bpos1lem  27602  bposlem1  27604  bposlem2  27605  bposlem6  27609  bposlem7  27610  bposlem9  27612  lgseisen  27699  chebbnd1lem2  27790  chebbnd1lem3  27791  chto1ub  27796  rplogsumlem1  27804  dchrisumlem3  27811  dchrvmasumlem2  27818  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2  27838  mulog2sumlem1  27854  mulog2sumlem2  27855  log2sumbnd  27864  selberglem2  27866  chpdifbndlem1  27873  logdivbnd  27876  pntrlog2bndlem4  27900  pntibndlem2  27911  pntibndlem3  27912  pntlemh  27919  pntlemr  27922  pntlemk  27926  pntlemo  27927  ostth2lem1  27938  ostth2lem3  27955  ostth3  27958  axcontlem2  29536  nmoub3i  31368  blocni  31400  ubthlem3  31467  minvecolem2  31470  bcs2  31777  nmopub2tALT  32504  nmfnleub2  32521  nmophmi  32626  bdophmi  32627  lnconi  32628  cnlnadjlem2  32663  cnlnadjlem7  32668  nmopadjlem  32684  nmopcoadji  32696  leopnmid  32733  cdj1i  33028  cdj3lem2b  33032  cdj3i  33036  addltmulALT  33041  sgnmulsgp  33416  pnfinf  33737  rezh  34594  signshf  35210  knoppndvlem15  37372  knoppndvlem21  37378  itg2addnclem  38569  ftc1anclem3  38593  isbnd2  38697  isbnd3  38698  equivbnd  38704  aks6d1c7lem1  43210  resubdi  43427  pellexlem5  43819  pell1234qrmulcl  43841  pellfundex  43872  rmspecsqrtnq  43892  jm2.24nn  43945  jm2.17a  43946  jm2.17b  43947  jm2.17c  43948  acongrep  43966  acongeq  43969  jm3.1lem2  44004  mulltgt0  46008  ltdiv23neg  46374  fmul01  46561  fmuldfeq  46564  fmul01lt1lem1  46565  fmul01lt1lem2  46566  stoweidlem3  46982  stoweidlem13  46992  stoweidlem17  46996  stoweidlem34  47013  stoweidlem42  47021  stoweidlem48  47027  fourierdlem83  47168  hoidmvlelem2  47575  smfmullem1  47770  2leaddle2  48337  itsclc0lem1  49837  crosspaltd  50935  amgmwlem  50956