Theorem remulcli 8347

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 8314	. 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 6088   RRcr 8185   x. cmul 8191

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

This theorem is used by:  addltmul  9554  nn0lele2xi  9626  numltc  9819  ef01bndlem  12549  cos2bnd  12553  sin4lt0  12560  sincosq3sgn  16067  sincosq4sgn  16068  cosq23lt0  16072  coseq0q4123  16073  coseq00topi  16074  coseq0negpitopi  16075  sincos4thpi  16079  cosq34lt1  16090  cos02pilt1  16091  cos0pilt1  16092  log2ublem1  16233  log2ublem2  16234  bpos1lem  16321  bposlem7  16329  bposlem8  16330  bposlem9  16331  taupi  17342