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  12541  cos2bnd  12545  sin4lt0  12552  sincosq3sgn  15982  sincosq4sgn  15983  cosq23lt0  15987  coseq0q4123  15988  coseq00topi  15989  coseq0negpitopi  15990  sincos4thpi  15994  cosq34lt1  16004  cos02pilt1  16005  cos0pilt1  16006  log2ublem1  16143  log2ublem2  16144  bpos1lem  16231  taupi  17245