Theorem remulcli 8033

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 8000	. 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 2164  (class class class)co 5918   RRcr 7871   x. cmul 7877

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

This theorem is referenced by:  addltmul  9219  nn0lele2xi  9291  numltc  9473  ef01bndlem  11899  cos2bnd  11903  sin4lt0  11910  sincosq3sgn  14963  sincosq4sgn  14964  cosq23lt0  14968  coseq0q4123  14969  coseq00topi  14970  coseq0negpitopi  14971  sincos4thpi  14975  cosq34lt1  14985  cos02pilt1  14986  cos0pilt1  14987  taupi  15563