Theorem remulcl 11153

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067   · cmul 11073

This theorem was proved from axioms:  ax-mulrcl 11131

This theorem is referenced by:  1re  11174  remulcli  11190  remulcld  11204  axmulgt0  11248  00id  11349  mul02lem1  11350  recextlem2  11809  recex  11810  lemul1  12034  ltmul12a  12038  lemul12b  12039  mulgt1OLD  12041  mulgt1  12044  mulge0b  12053  mulle0b  12054  ltdivmul  12058  ledivmul  12059  lt2mul2div  12061  lemuldiv  12063  ltdiv23  12074  lediv23  12075  supmullem2  12154  cju  12182  addltmul  12418  zmulcl  12582  irrmul  12933  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  rpmulcl  12976  xmulasslem3  13246  xadddilem  13254  ge0mulcl  13422  iccdil  13451  mulmod0  13839  modmulnn  13851  modcyc  13868  modmul1  13889  modaddmulmod  13903  moddi  13904  addmodlteq  13911  reexpcl  14043  reexpclz  14047  expge0  14063  expge1  14064  expubnd  14143  bernneq  14194  expmulnbnd  14200  digit2  14201  digit1  14202  discr  14205  faclbnd  14255  faclbnd3  14257  faclbnd5  14263  facavg  14266  cshweqrep  14786  crre  15080  remim  15083  mulre  15087  01sqrexlem6  15213  01sqrexlem7  15214  sqreulem  15326  amgm2  15336  o1mul  15581  caucvgrlem  15639  climcndslem2  15816  climcnds  15817  fprodrecl  15919  fprodreclf  15925  iprodrecl  15968  rerisefaccl  15983  refallfaccl  15984  efcllem  16043  ege2le3  16056  ef01bndlem  16152  cos01gt0  16159  modprm0  16776  prmreclem3  16889  4sqlem11  16926  resubdrg  21517  nmoco  24625  nghmco  24626  blcvx  24686  iihalf1  24825  iihalf2  24828  iimulcl  24833  pcoass  24924  tcphcphlem1  25135  csbren  25299  trirn  25300  minveclem2  25326  sca2rab  25413  uniioombllem5  25488  mbfmulc2lem  25548  i1fmul  25597  i1fmulclem  25603  i1fmulc  25604  dveflem  25883  cmvth  25895  cmvthOLD  25896  dvivthlem1  25913  dvfsumle  25926  dvfsumleOLD  25927  dvfsumlem2  25933  dvfsumlem2OLD  25934  pilem2  26362  tangtx  26414  sinq12gt0  26416  coskpi  26432  cosne0  26438  efif1olem2  26452  efif1olem4  26454  relogexp  26505  logcxp  26578  rpcxpcl  26585  abscxpbnd  26663  ang180lem1  26719  atantan  26833  atanbndlem  26835  o1cxp  26885  divsqrtsumlem  26890  jensenlem2  26898  jensen  26899  zetacvg  26925  regamcl  26971  basellem1  26991  basellem4  26994  basellem9  26999  chtublem  27122  chtub  27123  logfaclbnd  27133  bpos1lem  27193  bposlem1  27195  bposlem2  27196  bposlem6  27200  bposlem7  27201  bposlem9  27203  lgseisen  27290  chebbnd1lem2  27381  chebbnd1lem3  27382  chto1ub  27387  rplogsumlem1  27395  dchrisumlem3  27402  dchrvmasumlem2  27409  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2  27429  mulog2sumlem1  27445  mulog2sumlem2  27446  log2sumbnd  27455  selberglem2  27457  chpdifbndlem1  27464  logdivbnd  27467  pntrlog2bndlem4  27491  pntibndlem2  27502  pntibndlem3  27503  pntlemh  27510  pntlemr  27513  pntlemk  27517  pntlemo  27518  ostth2lem1  27529  ostth2lem3  27546  ostth3  27549  axcontlem2  28892  nmoub3i  30702  blocni  30734  ubthlem3  30801  minvecolem2  30804  bcs2  31111  nmopub2tALT  31838  nmfnleub2  31855  nmophmi  31960  bdophmi  31961  lnconi  31962  cnlnadjlem2  31997  cnlnadjlem7  32002  nmopadjlem  32018  nmopcoadji  32030  leopnmid  32067  cdj1i  32362  cdj3lem2b  32366  cdj3i  32370  addltmulALT  32375  sgnmul  32760  sgnmulsgn  32767  sgnmulsgp  32768  pnfinf  33137  rezh  33959  signshf  34579  knoppndvlem15  36514  knoppndvlem21  36520  itg2addnclem  37665  ftc1anclem3  37689  isbnd2  37777  isbnd3  37778  equivbnd  37784  aks6d1c7lem1  42168  resubdi  42384  pellexlem5  42821  pell1234qrmulcl  42843  pellfundex  42874  rmspecsqrtnq  42894  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  acongrep  42969  acongeq  42972  jm3.1lem2  43007  mulltgt0  45016  ltdiv23neg  45390  fmul01  45578  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  stoweidlem3  46001  stoweidlem13  46011  stoweidlem17  46015  stoweidlem34  46032  stoweidlem42  46040  stoweidlem48  46046  fourierdlem83  46187  hoidmvlelem2  46594  smfmullem1  46789  2leaddle2  47296  itsclc0lem1  48742  amgmwlem  49788