Theorem remulcli 7967

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 7935	. 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 5871   RRcr 7806   x. cmul 7812

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

This theorem is referenced by:  addltmul  9150  nn0lele2xi  9222  numltc  9404  ef01bndlem  11756  cos2bnd  11760  sin4lt0  11766  sincosq3sgn  14111  sincosq4sgn  14112  cosq23lt0  14116  coseq0q4123  14117  coseq00topi  14118  coseq0negpitopi  14119  sincos4thpi  14123  cosq34lt1  14133  cos02pilt1  14134  cos0pilt1  14135  taupi  14671