Theorem remulcli 7973

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 7941	. 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 2148  (class class class)co 5877   RRcr 7812   x. cmul 7818

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

This theorem is referenced by:  addltmul  9157  nn0lele2xi  9229  numltc  9411  ef01bndlem  11766  cos2bnd  11770  sin4lt0  11776  sincosq3sgn  14334  sincosq4sgn  14335  cosq23lt0  14339  coseq0q4123  14340  coseq00topi  14341  coseq0negpitopi  14342  sincos4thpi  14346  cosq34lt1  14356  cos02pilt1  14357  cos0pilt1  14358  taupi  14906