Theorem remulcli 11199

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

Syntax hints:   ∈ wcel 2143  (class class class)co 7397  ℝcr 11073   · cmul 11079

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  ledivp1i  12118  ltdivp1i  12119  addltmul  12458  nn0lele2xi  12538  10re  12712  numltc  12720  nn0opthlem2  14283  faclbnd4lem1  14307  ef01bndlem  16217  cos2bnd  16221  sin4lt0  16228  dvdslelem  16344  divalglem1  16429  divalglem6  16433  2pire  26521  sincosq3sgn  26566  sincosq4sgn  26567  sincos4thpi  26579  cos02pilt1  26592  cosq34lt1  26593  cos0pilt1  26598  efif1olem1  26608  efif1olem2  26609  efif1olem4  26611  efif1o  26612  efifo  26613  ang180lem1  26875  ang180lem2  26876  log2ublem1  27012  log2ublem2  27013  bpos1lem  27347  bposlem7  27355  bposlem8  27356  bposlem9  27357  chebbnd1lem3  27536  chebbnd1  27537  chto1ub  27541  siilem1  31055  normlem6  31319  normlem7  31320  norm-ii-i  31341  bcsiALT  31383  nmopadjlem  32293  nmopcoi  32299  bdopcoi  32302  nmopcoadji  32305  unierri  32308  dpmul4  33092  hgt750lem  34946  hgt750lem2  34947  hgt750leme  34953  problem5  36020  circum  36025  iexpire  36086  taupi  37816  sin2h  38110  tan2h  38112  sumnnodd  46207  sinaover2ne0  46443  stirlinglem11  46659  dirkercncflem4  46681  fourierdlem24  46706  fourierdlem43  46725  fourierdlem44  46726  fourierdlem68  46749  fourierdlem94  46775  fourierdlem111  46792  sqwvfoura  46803  sqwvfourb  46804  fourierswlem  46805  fouriersw  46806  goldrarr  47476  lighneallem4a  48218  tgoldbach  48440