Theorem remulcli 11306

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183   · cmul 11189

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

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

This theorem is referenced by:  ledivp1i  12220  ltdivp1i  12221  addltmul  12529  nn0lele2xi  12608  10re  12777  numltc  12784  nn0opthlem2  14318  faclbnd4lem1  14342  ef01bndlem  16232  cos2bnd  16236  sin4lt0  16243  dvdslelem  16357  divalglem1  16442  divalglem6  16446  sincosq3sgn  26560  sincosq4sgn  26561  sincos4thpi  26573  cos02pilt1  26586  cosq34lt1  26587  cos0pilt1  26592  efif1olem1  26602  efif1olem2  26603  efif1olem4  26605  efif1o  26606  efifo  26607  ang180lem1  26870  ang180lem2  26871  log2ublem1  27007  log2ublem2  27008  bpos1lem  27344  bposlem7  27352  bposlem8  27353  bposlem9  27354  chebbnd1lem3  27533  chebbnd1  27534  chto1ub  27538  siilem1  30883  normlem6  31147  normlem7  31148  norm-ii-i  31169  bcsiALT  31211  nmopadjlem  32121  nmopcoi  32127  bdopcoi  32130  nmopcoadji  32133  unierri  32136  dpmul4  32878  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  problem5  35637  circum  35642  iexpire  35697  taupi  37289  sin2h  37570  tan2h  37572  sumnnodd  45551  sinaover2ne0  45789  stirlinglem11  46005  dirkerper  46017  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem24  46052  fourierdlem43  46071  fourierdlem44  46072  fourierdlem68  46095  fourierdlem94  46121  fourierdlem111  46138  fourierdlem113  46140  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  lighneallem4a  47482  tgoldbach  47691