Theorem remulcli 8176

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 8143	. 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 2200  (class class class)co 6010   RRcr 8014   x. cmul 8020

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

This theorem is referenced by:  addltmul  9364  nn0lele2xi  9436  numltc  9619  ef01bndlem  12288  cos2bnd  12292  sin4lt0  12299  sincosq3sgn  15523  sincosq4sgn  15524  cosq23lt0  15528  coseq0q4123  15529  coseq00topi  15530  coseq0negpitopi  15531  sincos4thpi  15535  cosq34lt1  15545  cos02pilt1  15546  cos0pilt1  15547  taupi  16555