Theorem remulcli 11150

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11027   · cmul 11033

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

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

This theorem is referenced by:  ledivp1i  12069  ltdivp1i  12070  addltmul  12379  nn0lele2xi  12459  10re  12628  numltc  12635  nn0opthlem2  14194  faclbnd4lem1  14218  ef01bndlem  16111  cos2bnd  16115  sin4lt0  16122  dvdslelem  16238  divalglem1  16323  divalglem6  16327  sincosq3sgn  26467  sincosq4sgn  26468  sincos4thpi  26480  cos02pilt1  26493  cosq34lt1  26494  cos0pilt1  26499  efif1olem1  26509  efif1olem2  26510  efif1olem4  26512  efif1o  26513  efifo  26514  ang180lem1  26777  ang180lem2  26778  log2ublem1  26914  log2ublem2  26915  bpos1lem  27251  bposlem7  27259  bposlem8  27260  bposlem9  27261  chebbnd1lem3  27440  chebbnd1  27441  chto1ub  27445  siilem1  30928  normlem6  31192  normlem7  31193  norm-ii-i  31214  bcsiALT  31256  nmopadjlem  32166  nmopcoi  32172  bdopcoi  32175  nmopcoadji  32178  unierri  32181  dpmul4  32997  hgt750lem  34810  hgt750lem2  34811  hgt750leme  34817  problem5  35865  circum  35870  iexpire  35931  taupi  37530  sin2h  37813  tan2h  37815  sumnnodd  45897  sinaover2ne0  46133  stirlinglem11  46349  dirkerper  46361  dirkercncflem2  46369  dirkercncflem4  46371  fourierdlem24  46396  fourierdlem43  46415  fourierdlem44  46416  fourierdlem68  46439  fourierdlem94  46465  fourierdlem111  46482  fourierdlem113  46484  sqwvfoura  46493  sqwvfourb  46494  fourierswlem  46495  fouriersw  46496  lighneallem4a  47875  tgoldbach  48084