Theorem remulcli 11335

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

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209   · cmul 11215

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11273

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ledivp1i  12252  ltdivp1i  12253  addltmul  12592  nn0lele2xi  12672  10re  12847  numltc  12855  nn0opthlem2  14423  faclbnd4lem1  14447  ef01bndlem  16364  cos2bnd  16368  sin4lt0  16375  dvdslelem  16491  divalglem1  16576  divalglem6  16580  2pire  26796  sincosq3sgn  26841  sincosq4sgn  26842  sincos4thpi  26854  cos02pilt1  26866  cosq34lt1  26867  efif1olem1  26882  efif1olem2  26883  efif1o  26886  efifo  26887  ang180lem1  27149  ang180lem2  27150  log2ublem1  27286  log2ublem2  27287  bpos1lem  27621  bposlem7  27629  bposlem8  27630  bposlem9  27631  chebbnd1lem3  27810  chebbnd1  27811  chto1ub  27815  siilem1  31465  normlem6  31729  normlem7  31730  norm-ii-i  31751  bcsiALT  31793  nmopadjlem  32703  nmopcoi  32709  bdopcoi  32712  nmopcoadji  32715  unierri  32718  dpmul4  33533  hgt750lem  35333  hgt750lem2  35334  hgt750leme  35340  problem5  36555  circum  36560  iexpire  36627  taupi  38384  sin2h  38673  tan2h  38675  sumnnodd  46781  sinaover2ne0  47017  stirlinglem11  47233  dirkercncflem4  47255  fourierdlem24  47280  fourierdlem43  47299  fourierdlem44  47300  fourierdlem68  47323  fourierdlem94  47349  fourierdlem111  47366  sqwvfoura  47377  sqwvfourb  47378  fourierswlem  47379  fouriersw  47380  goldrarr  48067  goldratval  48075  lighneallem4a  48832  tgoldbach  49054