Theorem remulcld 8320

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 8271	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 2205  (class class class)co 6058   RRcr 8142   x. cmul 8148

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

This theorem is referenced by:  rimul  8876  ltmul1a  8882  ltmul1  8883  lemul1  8884  reapmul1lem  8885  reapmul1  8886  remulext1  8890  mulext1  8903  recexaplem2  8943  redivclap  9022  prodgt0gt0  9142  prodgt0  9143  prodge0  9145  lemul1a  9149  ltmuldiv  9165  ledivmul  9168  lt2mul2div  9170  lemuldiv  9172  lt2msq1  9176  lt2msq  9177  ltdiv23  9183  lediv23  9184  le2msq  9192  msq11  9193  div4p1lem1div2  9509  mul2lt0rlt0  10110  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  qbtwnrelemcalc  10639  qbtwnre  10640  flhalf  10686  modqval  10710  modqge0  10718  modqmulnn  10728  bernneq  11047  bernneq3  11049  expnbnd  11050  nn0opthlem2d  11108  faclbnd  11128  faclbnd6  11131  remullem  11581  cvg1nlemres  11695  resqrexlemover  11720  resqrexlemnm  11728  resqrexlemglsq  11732  sqrtmul  11745  abstri  11814  maxabslemlub  11917  maxltsup  11928  bdtrilem  11949  mulcn2  12022  reccn2ap  12023  cvgratnnlembern  12234  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemabsle  12238  cvgratnnlemfm  12240  cvgratnnlemrate  12241  mertenslemi1  12246  fprodge1  12350  efcllem  12370  ege2le3  12382  eftlub  12401  sin02gt0  12475  cos12dec  12479  eirraplem  12488  dvdslelemd  12554  divalglemnqt  12631  bitsp1o  12664  2expltfac  13162  oddennn  13227  metss2lem  15488  dveflem  15717  sin0pilem1  15772  sin0pilem2  15773  tangtx  15829  logdivlti  15872  rpcxpcl  15894  cxpmul  15903  cxplt  15907  rpcxple2  15909  rpcxplt2  15910  apcxp2  15930  rpabscxpbnd  15931  pellexlem2  15972  perfectlem2  15994  lgsdilem  16026  gausslemma2dlem0c  16050  gausslemma2dlem2  16061  gausslemma2dlem3  16062  lgsquadlem1  16076  lgsquadlem2  16077  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  nconstwlpolemgt0  16976