Theorem remulcli 11166

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043   · cmul 11049

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

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

This theorem is referenced by:  ledivp1i  12084  ltdivp1i  12085  addltmul  12394  nn0lele2xi  12474  10re  12644  numltc  12651  nn0opthlem2  14210  faclbnd4lem1  14234  ef01bndlem  16128  cos2bnd  16132  sin4lt0  16139  dvdslelem  16255  divalglem1  16340  divalglem6  16344  sincosq3sgn  26442  sincosq4sgn  26443  sincos4thpi  26455  cos02pilt1  26468  cosq34lt1  26469  cos0pilt1  26474  efif1olem1  26484  efif1olem2  26485  efif1olem4  26487  efif1o  26488  efifo  26489  ang180lem1  26752  ang180lem2  26753  log2ublem1  26889  log2ublem2  26890  bpos1lem  27226  bposlem7  27234  bposlem8  27235  bposlem9  27236  chebbnd1lem3  27415  chebbnd1  27416  chto1ub  27420  siilem1  30830  normlem6  31094  normlem7  31095  norm-ii-i  31116  bcsiALT  31158  nmopadjlem  32068  nmopcoi  32074  bdopcoi  32077  nmopcoadji  32080  unierri  32083  dpmul4  32884  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  problem5  35649  circum  35654  iexpire  35715  taupi  37304  sin2h  37597  tan2h  37599  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  47602  tgoldbach  47811