Theorem remulcli 11131

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008   · cmul 11014

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

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

This theorem is referenced by:  ledivp1i  12050  ltdivp1i  12051  addltmul  12360  nn0lele2xi  12440  10re  12610  numltc  12617  nn0opthlem2  14176  faclbnd4lem1  14200  ef01bndlem  16093  cos2bnd  16097  sin4lt0  16104  dvdslelem  16220  divalglem1  16305  divalglem6  16309  sincosq3sgn  26407  sincosq4sgn  26408  sincos4thpi  26420  cos02pilt1  26433  cosq34lt1  26434  cos0pilt1  26439  efif1olem1  26449  efif1olem2  26450  efif1olem4  26452  efif1o  26453  efifo  26454  ang180lem1  26717  ang180lem2  26718  log2ublem1  26854  log2ublem2  26855  bpos1lem  27191  bposlem7  27199  bposlem8  27200  bposlem9  27201  chebbnd1lem3  27380  chebbnd1  27381  chto1ub  27385  siilem1  30795  normlem6  31059  normlem7  31060  norm-ii-i  31081  bcsiALT  31123  nmopadjlem  32033  nmopcoi  32039  bdopcoi  32042  nmopcoadji  32045  unierri  32048  dpmul4  32855  hgt750lem  34625  hgt750lem2  34626  hgt750leme  34632  problem5  35652  circum  35657  iexpire  35718  taupi  37307  sin2h  37600  tan2h  37602  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