Theorem remulcli 11146

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023   · cmul 11029

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

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

This theorem is referenced by:  ledivp1i  12065  ltdivp1i  12066  addltmul  12375  nn0lele2xi  12455  10re  12624  numltc  12631  nn0opthlem2  14190  faclbnd4lem1  14214  ef01bndlem  16107  cos2bnd  16111  sin4lt0  16118  dvdslelem  16234  divalglem1  16319  divalglem6  16323  sincosq3sgn  26463  sincosq4sgn  26464  sincos4thpi  26476  cos02pilt1  26489  cosq34lt1  26490  cos0pilt1  26495  efif1olem1  26505  efif1olem2  26506  efif1olem4  26508  efif1o  26509  efifo  26510  ang180lem1  26773  ang180lem2  26774  log2ublem1  26910  log2ublem2  26911  bpos1lem  27247  bposlem7  27255  bposlem8  27256  bposlem9  27257  chebbnd1lem3  27436  chebbnd1  27437  chto1ub  27441  siilem1  30875  normlem6  31139  normlem7  31140  norm-ii-i  31161  bcsiALT  31203  nmopadjlem  32113  nmopcoi  32119  bdopcoi  32122  nmopcoadji  32125  unierri  32128  dpmul4  32944  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  problem5  35812  circum  35817  iexpire  35878  taupi  37467  sin2h  37750  tan2h  37752  sumnnodd  45818  sinaover2ne0  46054  stirlinglem11  46270  dirkerper  46282  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem24  46317  fourierdlem43  46336  fourierdlem44  46337  fourierdlem68  46360  fourierdlem94  46386  fourierdlem111  46403  fourierdlem113  46405  sqwvfoura  46414  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  lighneallem4a  47796  tgoldbach  48005