Theorem remulcli 11196

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 692	1 ⊢ (𝐴 · 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7389  ℝ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 207  df-an 396

This theorem is referenced by:  ledivp1i  12114  ltdivp1i  12115  addltmul  12424  nn0lele2xi  12504  10re  12674  numltc  12681  nn0opthlem2  14240  faclbnd4lem1  14264  ef01bndlem  16158  cos2bnd  16162  sin4lt0  16169  dvdslelem  16285  divalglem1  16370  divalglem6  16374  sincosq3sgn  26415  sincosq4sgn  26416  sincos4thpi  26428  cos02pilt1  26441  cosq34lt1  26442  cos0pilt1  26447  efif1olem1  26457  efif1olem2  26458  efif1olem4  26460  efif1o  26461  efifo  26462  ang180lem1  26725  ang180lem2  26726  log2ublem1  26862  log2ublem2  26863  bpos1lem  27199  bposlem7  27207  bposlem8  27208  bposlem9  27209  chebbnd1lem3  27388  chebbnd1  27389  chto1ub  27393  siilem1  30786  normlem6  31050  normlem7  31051  norm-ii-i  31072  bcsiALT  31114  nmopadjlem  32024  nmopcoi  32030  bdopcoi  32033  nmopcoadji  32036  unierri  32039  dpmul4  32840  hgt750lem  34648  hgt750lem2  34649  hgt750leme  34655  problem5  35656  circum  35661  iexpire  35717  taupi  37306  sin2h  37599  tan2h  37601  sumnnodd  45621  sinaover2ne0  45859  stirlinglem11  46075  dirkerper  46087  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem24  46122  fourierdlem43  46141  fourierdlem44  46142  fourierdlem68  46165  fourierdlem94  46191  fourierdlem111  46208  fourierdlem113  46210  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  lighneallem4a  47599  tgoldbach  47808