Theorem remulcli 11270

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

Syntax hints:   ∈ wcel 2098  (class class class)co 7426  ℝcr 11147   · cmul 11153

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

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

This theorem is referenced by:  ledivp1i  12179  ltdivp1i  12180  addltmul  12488  nn0lele2xi  12567  10re  12736  numltc  12743  nn0opthlem2  14270  faclbnd4lem1  14294  ef01bndlem  16170  cos2bnd  16174  sin4lt0  16181  dvdslelem  16295  divalglem1  16380  divalglem6  16384  sincosq3sgn  26463  sincosq4sgn  26464  sincos4thpi  26476  cos02pilt1  26488  cosq34lt1  26489  cos0pilt1  26494  efif1olem1  26504  efif1olem2  26505  efif1olem4  26507  efif1o  26508  efifo  26509  ang180lem1  26769  ang180lem2  26770  log2ublem1  26906  log2ublem2  26907  bpos1lem  27243  bposlem7  27251  bposlem8  27252  bposlem9  27253  chebbnd1lem3  27432  chebbnd1  27433  chto1ub  27437  siilem1  30689  normlem6  30953  normlem7  30954  norm-ii-i  30975  bcsiALT  31017  nmopadjlem  31927  nmopcoi  31933  bdopcoi  31936  nmopcoadji  31939  unierri  31942  dpmul4  32666  hgt750lem  34324  hgt750lem2  34325  hgt750leme  34331  problem5  35314  circum  35319  iexpire  35370  taupi  36843  sin2h  37124  tan2h  37126  sumnnodd  45065  sinaover2ne0  45303  stirlinglem11  45519  dirkerper  45531  dirkercncflem2  45539  dirkercncflem4  45541  fourierdlem24  45566  fourierdlem43  45585  fourierdlem44  45586  fourierdlem68  45609  fourierdlem94  45635  fourierdlem111  45652  fourierdlem113  45654  sqwvfoura  45663  sqwvfourb  45664  fourierswlem  45665  fouriersw  45666  lighneallem4a  46995  tgoldbach  47204