Theorem remulcld 7149

Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	|- ( ph -> A e. RR )
readdcld.2	|- ( ph -> B e. RR )

Assertion

Ref	Expression
remulcld	|- ( ph -> ( A x. B ) e. RR )

Proof of Theorem remulcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		readdcld.2	. 2 |- ( ph -> B e. RR )
3		remulcl 7101	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	syl2anc 403	1 |- ( ph -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1433  (class class class)co 5532   RRcr 6980   x. cmul 6986

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

This theorem is referenced by:  rimul  7685  ltmul1a  7691  ltmul1  7692  lemul1  7693  reapmul1lem  7694  reapmul1  7695  remulext1  7699  mulext1  7712  recexaplem2  7742  redivclap  7819  prodgt0gt0  7929  prodgt0  7930  prodge0  7932  lemul1a  7936  ltmuldiv  7952  ledivmul  7955  lt2mul2div  7957  lemuldiv  7959  lt2msq1  7963  lt2msq  7964  ltdiv23  7970  lediv23  7971  le2msq  7979  msq11  7980  div4p1lem1div2  8284  lincmb01cmp  9025  iccf1o  9026  qbtwnrelemcalc  9264  qbtwnre  9265  flhalf  9304  modqval  9326  modqge0  9334  modqmulnn  9344  bernneq  9593  bernneq3  9595  expnbnd  9596  nn0opthlem2d  9648  faclbnd  9668  faclbnd6  9671  remullem  9758  cvg1nlemres  9871  resqrexlemover  9896  resqrexlemnm  9904  resqrexlemglsq  9908  sqrtmul  9921  abstri  9990  maxabslemlub  10093  maxltsup  10104  mulcn2  10151  dvdslelemd  10243  divalglemnqt  10320