Theorem remulcli 11226

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7405  ℝcr 11105   · cmul 11111

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

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

This theorem is referenced by:  ledivp1i  12135  ltdivp1i  12136  addltmul  12444  nn0lele2xi  12523  10re  12692  numltc  12699  nn0opthlem2  14225  faclbnd4lem1  14249  ef01bndlem  16123  cos2bnd  16127  sin4lt0  16134  dvdslelem  16248  divalglem1  16333  divalglem6  16337  sincosq3sgn  26001  sincosq4sgn  26002  sincos4thpi  26014  cos02pilt1  26026  cosq34lt1  26027  cos0pilt1  26032  efif1olem1  26042  efif1olem2  26043  efif1olem4  26045  efif1o  26046  efifo  26047  ang180lem1  26303  ang180lem2  26304  log2ublem1  26440  log2ublem2  26441  bpos1lem  26774  bposlem7  26782  bposlem8  26783  bposlem9  26784  chebbnd1lem3  26963  chebbnd1  26964  chto1ub  26968  siilem1  30091  normlem6  30355  normlem7  30356  norm-ii-i  30377  bcsiALT  30419  nmopadjlem  31329  nmopcoi  31335  bdopcoi  31338  nmopcoadji  31341  unierri  31344  dpmul4  32067  hgt750lem  33651  hgt750lem2  33652  hgt750leme  33658  problem5  34642  circum  34647  iexpire  34693  taupi  36192  sin2h  36466  tan2h  36468  sumnnodd  44332  sinaover2ne0  44570  stirlinglem11  44786  dirkerper  44798  dirkercncflem2  44806  dirkercncflem4  44808  fourierdlem24  44833  fourierdlem43  44852  fourierdlem44  44853  fourierdlem68  44876  fourierdlem94  44902  fourierdlem111  44919  fourierdlem113  44921  sqwvfoura  44930  sqwvfourb  44931  fourierswlem  44932  fouriersw  44933  lighneallem4a  46262  tgoldbach  46471