Theorem remulcli 11161

Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ
axri.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
remulcli	⊢ (𝐴 · 𝐵) ∈ ℝ

Proof of Theorem remulcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
2		axri.2	. 2 ⊢ 𝐵 ∈ ℝ
3		remulcl 11123	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴 · 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11101

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  ledivp1i  12081  ltdivp1i  12082  addltmul  12413  nn0lele2xi  12493  10re  12663  numltc  12670  nn0opthlem2  14231  faclbnd4lem1  14255  ef01bndlem  16151  cos2bnd  16155  sin4lt0  16162  dvdslelem  16278  divalglem1  16363  divalglem6  16367  sincosq3sgn  26464  sincosq4sgn  26465  sincos4thpi  26477  cos02pilt1  26490  cosq34lt1  26491  cos0pilt1  26496  efif1olem1  26506  efif1olem2  26507  efif1olem4  26509  efif1o  26510  efifo  26511  ang180lem1  26773  ang180lem2  26774  log2ublem1  26910  log2ublem2  26911  bpos1lem  27245  bposlem7  27253  bposlem8  27254  bposlem9  27255  chebbnd1lem3  27434  chebbnd1  27435  chto1ub  27439  siilem1  30922  normlem6  31186  normlem7  31187  norm-ii-i  31208  bcsiALT  31250  nmopadjlem  32160  nmopcoi  32166  bdopcoi  32169  nmopcoadji  32172  unierri  32175  dpmul4  32973  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  problem5  35851  circum  35856  iexpire  35917  taupi  37637  sin2h  37931  tan2h  37933  sumnnodd  46060  sinaover2ne0  46296  stirlinglem11  46512  dirkerper  46524  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem24  46559  fourierdlem43  46578  fourierdlem44  46579  fourierdlem68  46602  fourierdlem94  46628  fourierdlem111  46645  fourierdlem113  46647  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  goldrarr  47329  lighneallem4a  48071  tgoldbach  48293