Theorem remulcli 11134

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 11097	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 · 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7352  ℝcr 11011   · cmul 11017

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

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

This theorem is referenced by:  ledivp1i  12053  ltdivp1i  12054  addltmul  12363  nn0lele2xi  12443  10re  12613  numltc  12620  nn0opthlem2  14182  faclbnd4lem1  14206  ef01bndlem  16099  cos2bnd  16103  sin4lt0  16110  dvdslelem  16226  divalglem1  16311  divalglem6  16315  sincosq3sgn  26442  sincosq4sgn  26443  sincos4thpi  26455  cos02pilt1  26468  cosq34lt1  26469  cos0pilt1  26474  efif1olem1  26484  efif1olem2  26485  efif1olem4  26487  efif1o  26488  efifo  26489  ang180lem1  26752  ang180lem2  26753  log2ublem1  26889  log2ublem2  26890  bpos1lem  27226  bposlem7  27234  bposlem8  27235  bposlem9  27236  chebbnd1lem3  27415  chebbnd1  27416  chto1ub  27420  siilem1  30838  normlem6  31102  normlem7  31103  norm-ii-i  31124  bcsiALT  31166  nmopadjlem  32076  nmopcoi  32082  bdopcoi  32085  nmopcoadji  32088  unierri  32091  dpmul4  32901  hgt750lem  34671  hgt750lem2  34672  hgt750leme  34678  problem5  35720  circum  35725  iexpire  35786  taupi  37374  sin2h  37656  tan2h  37658  sumnnodd  45735  sinaover2ne0  45971  stirlinglem11  46187  dirkerper  46199  dirkercncflem2  46207  dirkercncflem4  46209  fourierdlem24  46234  fourierdlem43  46253  fourierdlem44  46254  fourierdlem68  46277  fourierdlem94  46303  fourierdlem111  46320  fourierdlem113  46322  sqwvfoura  46331  sqwvfourb  46332  fourierswlem  46333  fouriersw  46334  lighneallem4a  47713  tgoldbach  47922