Theorem remulcli 11220

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

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094   · cmul 11100

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  ledivp1i  12135  ltdivp1i  12136  addltmul  12475  nn0lele2xi  12555  10re  12729  numltc  12737  nn0opthlem2  14301  faclbnd4lem1  14325  ef01bndlem  16235  cos2bnd  16239  sin4lt0  16246  dvdslelem  16362  divalglem1  16447  divalglem6  16451  2pire  26620  sincosq3sgn  26665  sincosq4sgn  26666  sincos4thpi  26678  cos02pilt1  26691  cosq34lt1  26692  cos0pilt1  26697  efif1olem1  26707  efif1olem2  26708  efif1olem4  26710  efif1o  26711  efifo  26712  ang180lem1  26974  ang180lem2  26975  log2ublem1  27111  log2ublem2  27112  bpos1lem  27446  bposlem7  27454  bposlem8  27455  bposlem9  27456  chebbnd1lem3  27635  chebbnd1  27636  chto1ub  27640  siilem1  31203  normlem6  31467  normlem7  31468  norm-ii-i  31489  bcsiALT  31531  nmopadjlem  32441  nmopcoi  32447  bdopcoi  32450  nmopcoadji  32453  unierri  32456  dpmul4  33233  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  problem5  36161  circum  36166  iexpire  36227  taupi  37987  sin2h  38281  tan2h  38283  sumnnodd  46366  sinaover2ne0  46602  stirlinglem11  46818  dirkercncflem4  46840  fourierdlem24  46865  fourierdlem43  46884  fourierdlem44  46885  fourierdlem68  46908  fourierdlem94  46934  fourierdlem111  46951  sqwvfoura  46962  sqwvfourb  46963  fourierswlem  46964  fouriersw  46965  goldrarr  47638  lighneallem4a  48380  tgoldbach  48602  crosspcle1i  50656  crosspcle2i  50657  crosspcle3i  50658  crosspdotsumi  50665  crosspdoti  50666  crosspalti  50667  crossp3i  50668