Theorem remulcli 11155

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031   · cmul 11037

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

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

This theorem is referenced by:  ledivp1i  12075  ltdivp1i  12076  addltmul  12407  nn0lele2xi  12487  10re  12657  numltc  12664  nn0opthlem2  14225  faclbnd4lem1  14249  ef01bndlem  16145  cos2bnd  16149  sin4lt0  16156  dvdslelem  16272  divalglem1  16357  divalglem6  16361  sincosq3sgn  26480  sincosq4sgn  26481  sincos4thpi  26493  cos02pilt1  26506  cosq34lt1  26507  cos0pilt1  26512  efif1olem1  26522  efif1olem2  26523  efif1olem4  26525  efif1o  26526  efifo  26527  ang180lem1  26789  ang180lem2  26790  log2ublem1  26926  log2ublem2  26927  bpos1lem  27262  bposlem7  27270  bposlem8  27271  bposlem9  27272  chebbnd1lem3  27451  chebbnd1  27452  chto1ub  27456  siilem1  30940  normlem6  31204  normlem7  31205  norm-ii-i  31226  bcsiALT  31268  nmopadjlem  32178  nmopcoi  32184  bdopcoi  32187  nmopcoadji  32190  unierri  32193  dpmul4  32991  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  problem5  35870  circum  35875  iexpire  35936  taupi  37656  sin2h  37948  tan2h  37950  sumnnodd  46081  sinaover2ne0  46317  stirlinglem11  46533  dirkerper  46545  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem24  46580  fourierdlem43  46599  fourierdlem44  46600  fourierdlem68  46623  fourierdlem94  46649  fourierdlem111  46666  fourierdlem113  46668  sqwvfoura  46677  sqwvfourb  46678  fourierswlem  46679  fouriersw  46680  goldrarr  47346  lighneallem4a  48086  tgoldbach  48308