Theorem remulcli 10659

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7158  ℝcr 10538   · cmul 10544

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  ledivp1i  11567  ltdivp1i  11568  addltmul  11876  nn0lele2xi  11955  10re  12120  numltc  12127  nn0opthlem2  13632  faclbnd4lem1  13656  ef01bndlem  15539  cos2bnd  15543  sin4lt0  15550  dvdslelem  15661  divalglem1  15747  divalglem6  15751  sincosq3sgn  25088  sincosq4sgn  25089  sincos4thpi  25101  cos02pilt1  25113  cosq34lt1  25114  efif1olem1  25128  efif1olem2  25129  efif1olem4  25131  efif1o  25132  efifo  25133  ang180lem1  25389  ang180lem2  25390  log2ublem1  25526  log2ublem2  25527  bpos1lem  25860  bposlem7  25868  bposlem8  25869  bposlem9  25870  chebbnd1lem3  26049  chebbnd1  26050  chto1ub  26054  siilem1  28630  normlem6  28894  normlem7  28895  norm-ii-i  28916  bcsiALT  28958  nmopadjlem  29868  nmopcoi  29874  bdopcoi  29877  nmopcoadji  29880  unierri  29883  dpmul4  30592  hgt750lem  31924  hgt750lem2  31925  hgt750leme  31931  problem5  32914  circum  32919  iexpire  32969  taupi  34606  sin2h  34884  tan2h  34886  sumnnodd  41918  sinaover2ne0  42156  stirlinglem11  42376  dirkerper  42388  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem24  42423  fourierdlem43  42442  fourierdlem44  42443  fourierdlem68  42466  fourierdlem94  42492  fourierdlem111  42509  fourierdlem113  42511  sqwvfoura  42520  sqwvfourb  42521  fourierswlem  42522  fouriersw  42523  lighneallem4a  43780  tgoldbach  43989