Theorem remulcli 7984

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 7952	. 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 2158  (class class class)co 5888   RRcr 7823   x. cmul 7829

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

This theorem is referenced by:  addltmul  9168  nn0lele2xi  9240  numltc  9422  ef01bndlem  11777  cos2bnd  11781  sin4lt0  11787  sincosq3sgn  14520  sincosq4sgn  14521  cosq23lt0  14525  coseq0q4123  14526  coseq00topi  14527  coseq0negpitopi  14528  sincos4thpi  14532  cosq34lt1  14542  cos02pilt1  14543  cos0pilt1  14544  taupi  15093