Theorem remulcli 8287

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 8254	. 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 2203  (class class class)co 6049   RRcr 8125   x. cmul 8131

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

This theorem is referenced by:  addltmul  9474  nn0lele2xi  9546  numltc  9733  ef01bndlem  12438  cos2bnd  12442  sin4lt0  12449  sincosq3sgn  15685  sincosq4sgn  15686  cosq23lt0  15690  coseq0q4123  15691  coseq00topi  15692  coseq0negpitopi  15693  sincos4thpi  15697  cosq34lt1  15707  cos02pilt1  15708  cos0pilt1  15709  taupi  16850