Theorem remulcli 10922

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801   · cmul 10807

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

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

This theorem is referenced by:  ledivp1i  11830  ltdivp1i  11831  addltmul  12139  nn0lele2xi  12218  10re  12385  numltc  12392  nn0opthlem2  13911  faclbnd4lem1  13935  ef01bndlem  15821  cos2bnd  15825  sin4lt0  15832  dvdslelem  15946  divalglem1  16031  divalglem6  16035  sincosq3sgn  25562  sincosq4sgn  25563  sincos4thpi  25575  cos02pilt1  25587  cosq34lt1  25588  cos0pilt1  25593  efif1olem1  25603  efif1olem2  25604  efif1olem4  25606  efif1o  25607  efifo  25608  ang180lem1  25864  ang180lem2  25865  log2ublem1  26001  log2ublem2  26002  bpos1lem  26335  bposlem7  26343  bposlem8  26344  bposlem9  26345  chebbnd1lem3  26524  chebbnd1  26525  chto1ub  26529  siilem1  29114  normlem6  29378  normlem7  29379  norm-ii-i  29400  bcsiALT  29442  nmopadjlem  30352  nmopcoi  30358  bdopcoi  30361  nmopcoadji  30364  unierri  30367  dpmul4  31090  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  problem5  33527  circum  33532  iexpire  33607  taupi  35421  sin2h  35694  tan2h  35696  sumnnodd  43061  sinaover2ne0  43299  stirlinglem11  43515  dirkerper  43527  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem24  43562  fourierdlem43  43581  fourierdlem44  43582  fourierdlem68  43605  fourierdlem94  43631  fourierdlem111  43648  fourierdlem113  43650  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  lighneallem4a  44948  tgoldbach  45157