Theorem remulcl 10021

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  (class class class)co 6650  ℝcr 9935   · cmul 9941

This theorem was proved from axioms:  ax-mulrcl 9999

This theorem is referenced by:  1re  10039  remulcli  10054  remulcld  10070  axmulgt0  10112  00id  10211  mul02lem1  10212  recextlem2  10658  recex  10659  lemul1  10875  ltmul12a  10879  lemul12b  10880  mulgt1  10882  mulge0b  10893  mulle0b  10894  ltdivmul  10898  ledivmul  10899  lt2mul2div  10901  lemuldiv  10903  ltdiv23  10914  lediv23  10915  supmullem2  10994  cju  11016  addltmul  11268  zmulcl  11426  irrmul  11813  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  rpmulcl  11855  xmulasslem3  12116  xadddilem  12124  ge0mulcl  12285  iccdil  12310  mulmod0  12676  modmulnn  12688  modcyc  12705  modmul1  12723  modaddmulmod  12737  moddi  12738  addmodlteq  12745  reexpcl  12877  reexpclz  12880  expge0  12896  expge1  12897  expubnd  12921  bernneq  12990  expmulnbnd  12996  digit2  12997  digit1  12998  discr  13001  faclbnd  13077  faclbnd3  13079  faclbnd5  13085  facavg  13088  cshweqrep  13567  crre  13854  remim  13857  mulre  13861  sqrlem6  13988  sqrlem7  13989  sqreulem  14099  amgm2  14109  o1mul  14345  caucvgrlem  14403  climcndslem2  14582  climcnds  14583  fprodrecl  14683  fprodreclf  14689  iprodrecl  14733  rerisefaccl  14748  refallfaccl  14749  efcllem  14808  ege2le3  14820  ef01bndlem  14914  cos01gt0  14921  modprm0  15510  prmreclem3  15622  4sqlem11  15659  resubdrg  19954  nmoco  22541  nghmco  22542  blcvx  22601  iihalf1  22730  iihalf2  22732  iimulcl  22736  pcoass  22824  tchcphlem1  23034  csbren  23182  trirn  23183  minveclem2  23197  sca2rab  23280  uniioombllem5  23355  mbfmulc2lem  23414  i1fmul  23463  i1fmulclem  23469  i1fmulc  23470  dveflem  23742  cmvth  23754  dvivthlem1  23771  dvfsumle  23784  dvfsumlem2  23790  pilem2  24206  tangtx  24257  sinq12gt0  24259  coskpi  24272  cosne0  24276  efif1olem2  24289  efif1olem4  24291  relogexp  24342  logcxp  24415  rpcxpcl  24422  abscxpbnd  24494  ang180lem1  24539  atantan  24650  atanbndlem  24652  o1cxp  24701  divsqrtsumlem  24706  jensenlem2  24714  jensen  24715  zetacvg  24741  regamcl  24787  basellem1  24807  basellem4  24810  basellem9  24815  chtublem  24936  chtub  24937  logfaclbnd  24947  bpos1lem  25007  bposlem1  25009  bposlem2  25010  bposlem6  25014  bposlem7  25015  bposlem9  25017  lgseisen  25104  chebbnd1lem2  25159  chebbnd1lem3  25160  chto1ub  25165  rplogsumlem1  25173  dchrisumlem3  25180  dchrvmasumlem2  25187  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2  25207  mulog2sumlem1  25223  mulog2sumlem2  25224  log2sumbnd  25233  selberglem2  25235  chpdifbndlem1  25242  logdivbnd  25245  pntrlog2bndlem4  25269  pntibndlem2  25280  pntibndlem3  25281  pntlemh  25288  pntlemr  25291  pntlemk  25295  pntlemo  25296  ostth2lem1  25307  ostth2lem3  25324  ostth3  25327  axcontlem2  25845  nmoub3i  27628  blocni  27660  ubthlem3  27728  minvecolem2  27731  bcs2  28039  nmopub2tALT  28768  nmfnleub2  28785  nmophmi  28890  bdophmi  28891  lnconi  28892  cnlnadjlem2  28927  cnlnadjlem7  28932  nmopadjlem  28948  nmopcoadji  28960  leopnmid  28997  cdj1i  29292  cdj3lem2b  29296  cdj3i  29300  addltmulALT  29305  pnfinf  29737  rezh  30015  sgnmul  30604  sgnmulsgn  30611  sgnmulsgp  30612  signshf  30665  knoppndvlem15  32517  knoppndvlem21  32523  itg2addnclem  33461  ftc1anclem3  33487  isbnd2  33582  isbnd3  33583  equivbnd  33589  pellexlem5  37397  pell1234qrmulcl  37419  pellfundex  37450  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  acongrep  37547  acongeq  37550  jm3.1lem2  37585  mulltgt0  39181  ltdiv23neg  39617  fmul01  39812  fmuldfeq  39815  fmul01lt1lem1  39816  fmul01lt1lem2  39817  stoweidlem3  40220  stoweidlem13  40230  stoweidlem17  40234  stoweidlem34  40251  stoweidlem42  40259  stoweidlem48  40265  fourierdlem83  40406  hoidmvlelem2  40810  smfmullem1  40998  2leaddle2  41312  amgmwlem  42548