Theorem remulcli 11275

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℝcr 11152   · cmul 11158

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

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

This theorem is referenced by:  ledivp1i  12191  ltdivp1i  12192  addltmul  12500  nn0lele2xi  12580  10re  12750  numltc  12757  nn0opthlem2  14305  faclbnd4lem1  14329  ef01bndlem  16217  cos2bnd  16221  sin4lt0  16228  dvdslelem  16343  divalglem1  16428  divalglem6  16432  sincosq3sgn  26557  sincosq4sgn  26558  sincos4thpi  26570  cos02pilt1  26583  cosq34lt1  26584  cos0pilt1  26589  efif1olem1  26599  efif1olem2  26600  efif1olem4  26602  efif1o  26603  efifo  26604  ang180lem1  26867  ang180lem2  26868  log2ublem1  27004  log2ublem2  27005  bpos1lem  27341  bposlem7  27349  bposlem8  27350  bposlem9  27351  chebbnd1lem3  27530  chebbnd1  27531  chto1ub  27535  siilem1  30880  normlem6  31144  normlem7  31145  norm-ii-i  31166  bcsiALT  31208  nmopadjlem  32118  nmopcoi  32124  bdopcoi  32127  nmopcoadji  32130  unierri  32133  dpmul4  32881  hgt750lem  34645  hgt750lem2  34646  hgt750leme  34652  problem5  35654  circum  35659  iexpire  35715  taupi  37306  sin2h  37597  tan2h  37599  sumnnodd  45586  sinaover2ne0  45824  stirlinglem11  46040  dirkerper  46052  dirkercncflem2  46060  dirkercncflem4  46062  fourierdlem24  46087  fourierdlem43  46106  fourierdlem44  46107  fourierdlem68  46130  fourierdlem94  46156  fourierdlem111  46173  fourierdlem113  46175  sqwvfoura  46184  sqwvfourb  46185  fourierswlem  46186  fouriersw  46187  lighneallem4a  47533  tgoldbach  47742