Theorem remulcli 8236

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 8203	. 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 6028   RRcr 8074   x. cmul 8080

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

This theorem is referenced by:  addltmul  9424  nn0lele2xi  9496  numltc  9679  ef01bndlem  12378  cos2bnd  12382  sin4lt0  12389  sincosq3sgn  15619  sincosq4sgn  15620  cosq23lt0  15624  coseq0q4123  15625  coseq00topi  15626  coseq0negpitopi  15627  sincos4thpi  15631  cosq34lt1  15641  cos02pilt1  15642  cos0pilt1  15643  taupi  16786