Theorem remulcli 8340

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 8307	. 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 6085   RRcr 8178   x. cmul 8184

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

This theorem is used by:  addltmul  9544  nn0lele2xi  9616  numltc  9804  ef01bndlem  12525  cos2bnd  12529  sin4lt0  12536  sincosq3sgn  15932  sincosq4sgn  15933  cosq23lt0  15937  coseq0q4123  15938  coseq00topi  15939  coseq0negpitopi  15940  sincos4thpi  15944  cosq34lt1  15954  cos02pilt1  15955  cos0pilt1  15956  log2ublem1  16089  log2ublem2  16090  taupi  17135