Theorem remulcli 9631

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 9598	. 2
4	1, 2, 3	mp2an 672	1

Syntax hints:  e.wcel 1818  (class class class)co 6296  cr 9512  cmul 9518

This theorem is referenced by:  ledivp1i  10496  ltdivp1i  10497  addltmul  10799  nn0lele2xi  10873  numltc  11024  nn0opthlem2  12349  faclbnd4lem1  12371  ef01bndlem  13919  cos2bnd  13923  sin4lt0  13930  dvdslelem  14030  divalglem1  14052  divalglem6  14056  sincosq3sgn  22893  sincosq4sgn  22894  sincos4thpi  22906  efif1olem1  22929  efif1olem2  22930  efif1olem4  22932  efif1o  22933  efifo  22934  ang180lem1  23141  ang180lem2  23142  log2ublem1  23277  log2ublem2  23278  bpos1lem  23557  bposlem7  23565  bposlem8  23566  bposlem9  23567  chebbnd1lem3  23656  chebbnd1  23657  chto1ub  23661  siilem1  25766  normlem6  26032  normlem7  26033  norm-ii-i  26054  bcsiALT  26096  nmopadjlem  27008  nmopcoi  27014  bdopcoi  27017  nmopcoadji  27020  unierri  27023  problem5  29023  circum  29040  iexpire  29122  sin2h  30045  tan2h  30047  sumnnodd  31636  sinaover2ne0  31668  stirlinglem11  31866  dirkerper  31878  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem24  31913  fourierdlem43  31932  fourierdlem44  31933  fourierdlem68  31957  fourierdlem94  31983  fourierdlem111  32000  fourierdlem113  32002  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  taupi  37698

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

This theorem depends on definitions:  df-bi 185  df-an 371