Theorem remulcli 11000

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7284  ℝcr 10879   · cmul 10885

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

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

This theorem is referenced by:  ledivp1i  11909  ltdivp1i  11910  addltmul  12218  nn0lele2xi  12297  10re  12465  numltc  12472  nn0opthlem2  13992  faclbnd4lem1  14016  ef01bndlem  15902  cos2bnd  15906  sin4lt0  15913  dvdslelem  16027  divalglem1  16112  divalglem6  16116  sincosq3sgn  25666  sincosq4sgn  25667  sincos4thpi  25679  cos02pilt1  25691  cosq34lt1  25692  cos0pilt1  25697  efif1olem1  25707  efif1olem2  25708  efif1olem4  25710  efif1o  25711  efifo  25712  ang180lem1  25968  ang180lem2  25969  log2ublem1  26105  log2ublem2  26106  bpos1lem  26439  bposlem7  26447  bposlem8  26448  bposlem9  26449  chebbnd1lem3  26628  chebbnd1  26629  chto1ub  26633  siilem1  29222  normlem6  29486  normlem7  29487  norm-ii-i  29508  bcsiALT  29550  nmopadjlem  30460  nmopcoi  30466  bdopcoi  30469  nmopcoadji  30472  unierri  30475  dpmul4  31197  hgt750lem  32640  hgt750lem2  32641  hgt750leme  32647  problem5  33636  circum  33641  iexpire  33710  taupi  35503  sin2h  35776  tan2h  35778  sumnnodd  43178  sinaover2ne0  43416  stirlinglem11  43632  dirkerper  43644  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem24  43679  fourierdlem43  43698  fourierdlem44  43699  fourierdlem68  43722  fourierdlem94  43748  fourierdlem111  43765  fourierdlem113  43767  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  lighneallem4a  45071  tgoldbach  45280