Theorem remulcli 8186

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 8153	. 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 6013   RRcr 8024   x. cmul 8030

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

This theorem is referenced by:  addltmul  9374  nn0lele2xi  9446  numltc  9629  ef01bndlem  12310  cos2bnd  12314  sin4lt0  12321  sincosq3sgn  15545  sincosq4sgn  15546  cosq23lt0  15550  coseq0q4123  15551  coseq00topi  15552  coseq0negpitopi  15553  sincos4thpi  15557  cosq34lt1  15567  cos02pilt1  15568  cos0pilt1  15569  taupi  16627