Theorem remulcli 8341

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 8308	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	mp2an 430	1 |- ( A x. B ) e. RR

This proof depends on syntax axioms:   e. wcel 2209  (class class class)co 6085   RRcr 8179   x. cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8279

This theorem is used by:  addltmul  9547  nn0lele2xi  9619  numltc  9812  ef01bndlem  12542  cos2bnd  12546  sin4lt0  12553  sincosq3sgn  16021  sincosq4sgn  16022  cosq23lt0  16026  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  sincos4thpi  16033  cosq34lt1  16044  cos02pilt1  16045  cos0pilt1  16046  log2ublem1  16187  log2ublem2  16188  bpos1lem  16275  bposlem7  16283  bposlem8  16284  bposlem9  16285  taupi  17295