Theorem remulcli 11256

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133   · cmul 11139

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

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

This theorem is referenced by:  ledivp1i  12172  ltdivp1i  12173  addltmul  12482  nn0lele2xi  12562  10re  12732  numltc  12739  nn0opthlem2  14292  faclbnd4lem1  14316  ef01bndlem  16207  cos2bnd  16211  sin4lt0  16218  dvdslelem  16333  divalglem1  16418  divalglem6  16422  sincosq3sgn  26466  sincosq4sgn  26467  sincos4thpi  26479  cos02pilt1  26492  cosq34lt1  26493  cos0pilt1  26498  efif1olem1  26508  efif1olem2  26509  efif1olem4  26511  efif1o  26512  efifo  26513  ang180lem1  26776  ang180lem2  26777  log2ublem1  26913  log2ublem2  26914  bpos1lem  27250  bposlem7  27258  bposlem8  27259  bposlem9  27260  chebbnd1lem3  27439  chebbnd1  27440  chto1ub  27444  siilem1  30837  normlem6  31101  normlem7  31102  norm-ii-i  31123  bcsiALT  31165  nmopadjlem  32075  nmopcoi  32081  bdopcoi  32084  nmopcoadji  32087  unierri  32090  dpmul4  32893  hgt750lem  34688  hgt750lem2  34689  hgt750leme  34695  problem5  35696  circum  35701  iexpire  35757  taupi  37346  sin2h  37639  tan2h  37641  sumnnodd  45639  sinaover2ne0  45877  stirlinglem11  46093  dirkerper  46105  dirkercncflem2  46113  dirkercncflem4  46115  fourierdlem24  46140  fourierdlem43  46159  fourierdlem44  46160  fourierdlem68  46183  fourierdlem94  46209  fourierdlem111  46226  fourierdlem113  46228  sqwvfoura  46237  sqwvfourb  46238  fourierswlem  46239  fouriersw  46240  lighneallem4a  47602  tgoldbach  47811