Theorem remulcli 11232

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7411  ℝcr 11111   · cmul 11117

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

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  ledivp1i  12141  ltdivp1i  12142  addltmul  12450  nn0lele2xi  12529  10re  12698  numltc  12705  nn0opthlem2  14231  faclbnd4lem1  14255  ef01bndlem  16129  cos2bnd  16133  sin4lt0  16140  dvdslelem  16254  divalglem1  16339  divalglem6  16343  sincosq3sgn  26017  sincosq4sgn  26018  sincos4thpi  26030  cos02pilt1  26042  cosq34lt1  26043  cos0pilt1  26048  efif1olem1  26058  efif1olem2  26059  efif1olem4  26061  efif1o  26062  efifo  26063  ang180lem1  26321  ang180lem2  26322  log2ublem1  26458  log2ublem2  26459  bpos1lem  26792  bposlem7  26800  bposlem8  26801  bposlem9  26802  chebbnd1lem3  26981  chebbnd1  26982  chto1ub  26986  siilem1  30142  normlem6  30406  normlem7  30407  norm-ii-i  30428  bcsiALT  30470  nmopadjlem  31380  nmopcoi  31386  bdopcoi  31389  nmopcoadji  31392  unierri  31395  dpmul4  32118  hgt750lem  33732  hgt750lem2  33733  hgt750leme  33739  problem5  34723  circum  34728  iexpire  34774  taupi  36290  sin2h  36564  tan2h  36566  sumnnodd  44425  sinaover2ne0  44663  stirlinglem11  44879  dirkerper  44891  dirkercncflem2  44899  dirkercncflem4  44901  fourierdlem24  44926  fourierdlem43  44945  fourierdlem44  44946  fourierdlem68  44969  fourierdlem94  44995  fourierdlem111  45012  fourierdlem113  45014  sqwvfoura  45023  sqwvfourb  45024  fourierswlem  45025  fouriersw  45026  lighneallem4a  46355  tgoldbach  46564