Theorem remulcli 8193

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 8160	. 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 2202  (class class class)co 6018   RRcr 8031   x. cmul 8037

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

This theorem is referenced by:  addltmul  9381  nn0lele2xi  9453  numltc  9636  ef01bndlem  12322  cos2bnd  12326  sin4lt0  12333  sincosq3sgn  15558  sincosq4sgn  15559  cosq23lt0  15563  coseq0q4123  15564  coseq00topi  15565  coseq0negpitopi  15566  sincos4thpi  15570  cosq34lt1  15580  cos02pilt1  15581  cos0pilt1  15582  taupi  16703