Theorem remulcli 10508

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

Syntax hints:   ∈ wcel 2081  (class class class)co 7021  ℝcr 10387   · cmul 10393

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

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

This theorem is referenced by:  ledivp1i  11418  ltdivp1i  11419  addltmul  11726  nn0lele2xi  11805  10re  11971  numltc  11978  nn0opthlem2  13484  faclbnd4lem1  13508  ef01bndlem  15375  cos2bnd  15379  sin4lt0  15386  dvdslelem  15497  divalglem1  15583  divalglem6  15587  sincosq3sgn  24774  sincosq4sgn  24775  sincos4thpi  24787  efif1olem1  24812  efif1olem2  24813  efif1olem4  24815  efif1o  24816  efifo  24817  ang180lem1  25073  ang180lem2  25074  log2ublem1  25211  log2ublem2  25212  bpos1lem  25545  bposlem7  25553  bposlem8  25554  bposlem9  25555  chebbnd1lem3  25734  chebbnd1  25735  chto1ub  25739  siilem1  28324  normlem6  28588  normlem7  28589  norm-ii-i  28610  bcsiALT  28652  nmopadjlem  29562  nmopcoi  29568  bdopcoi  29571  nmopcoadji  29574  unierri  29577  dpmul4  30279  hgt750lem  31544  hgt750lem2  31545  hgt750leme  31551  problem5  32526  circum  32531  iexpire  32581  taupi  34160  sin2h  34438  tan2h  34440  sumnnodd  41478  sinaover2ne0  41716  stirlinglem11  41937  dirkerper  41949  dirkercncflem2  41957  dirkercncflem4  41959  fourierdlem24  41984  fourierdlem43  42003  fourierdlem44  42004  fourierdlem68  42027  fourierdlem94  42053  fourierdlem111  42070  fourierdlem113  42072  sqwvfoura  42081  sqwvfourb  42082  fourierswlem  42083  fouriersw  42084  lighneallem4a  43281  tgoldbach  43490