Theorem remulcli 8305

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 8272	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	mp2an 426	1 |- ( A x. B ) e. RR

Syntax hints:   e. wcel 2205  (class class class)co 6059   RRcr 8143   x. cmul 8149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8243

This theorem is referenced by:  addltmul  9496  nn0lele2xi  9568  numltc  9756  ef01bndlem  12472  cos2bnd  12476  sin4lt0  12483  sincosq3sgn  15824  sincosq4sgn  15825  cosq23lt0  15829  coseq0q4123  15830  coseq00topi  15831  coseq0negpitopi  15832  sincos4thpi  15836  cosq34lt1  15846  cos02pilt1  15847  cos0pilt1  15848  taupi  16999