Theorem remulcli 8347

Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	|- A e. RR
axri.2	|- B e. RR

Assertion

Ref	Expression
remulcli	|- ( A x. B ) e. RR

Proof of Theorem remulcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 |- A e. RR
2		axri.2	. 2 |- B e. RR
3		remulcl 8314	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	mp2an 430	1 |- ( A x. B ) e. RR

This proof depends on syntax axioms:   e. wcel 2209  (class class class)co 6088   RRcr 8185   x. cmul 8191

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8285

This theorem is used by:  addltmul  9554  nn0lele2xi  9626  numltc  9818  ef01bndlem  12548  cos2bnd  12552  sin4lt0  12559  sincosq3sgn  16088  sincosq4sgn  16089  cosq23lt0  16093  coseq0q4123  16094  coseq00topi  16095  coseq0negpitopi  16096  sincos4thpi  16100  cosq34lt1  16111  cos02pilt1  16112  cos0pilt1  16113  log2ublem1  16254  log2ublem2  16255  bpos1lem  16342  bposlem7  16350  bposlem8  16351  bposlem9  16352  taupi  17363