Theorem remulcld 8253

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 8203	. 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 2202  (class class class)co 6028   RRcr 8074   x. cmul 8080

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

This theorem is referenced by:  rimul  8808  ltmul1a  8814  ltmul1  8815  lemul1  8816  reapmul1lem  8817  reapmul1  8818  remulext1  8822  mulext1  8835  recexaplem2  8875  redivclap  8954  prodgt0gt0  9074  prodgt0  9075  prodge0  9077  lemul1a  9081  ltmuldiv  9097  ledivmul  9100  lt2mul2div  9102  lemuldiv  9104  lt2msq1  9108  lt2msq  9109  ltdiv23  9115  lediv23  9116  le2msq  9124  msq11  9125  div4p1lem1div2  9441  mul2lt0rlt0  10039  lincmb01cmp  10283  iccf1o  10284  qbtwnrelemcalc  10561  qbtwnre  10562  flhalf  10608  modqval  10632  modqge0  10640  modqmulnn  10650  bernneq  10968  bernneq3  10970  expnbnd  10971  nn0opthlem2d  11029  faclbnd  11049  faclbnd6  11052  remullem  11494  cvg1nlemres  11608  resqrexlemover  11633  resqrexlemnm  11641  resqrexlemglsq  11645  sqrtmul  11658  abstri  11727  maxabslemlub  11830  maxltsup  11841  bdtrilem  11862  mulcn2  11935  reccn2ap  11936  cvgratnnlembern  12147  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemabsle  12151  cvgratnnlemfm  12153  cvgratnnlemrate  12154  mertenslemi1  12159  fprodge1  12263  efcllem  12283  ege2le3  12295  eftlub  12314  sin02gt0  12388  cos12dec  12392  eirraplem  12401  dvdslelemd  12467  divalglemnqt  12544  bitsp1o  12577  2expltfac  13075  oddennn  13076  metss2lem  15291  dveflem  15520  sin0pilem1  15575  sin0pilem2  15576  tangtx  15632  logdivlti  15675  rpcxpcl  15697  cxpmul  15706  cxplt  15710  rpcxple2  15712  rpcxplt2  15713  apcxp2  15733  rpabscxpbnd  15734  pellexlem2  15775  perfectlem2  15797  lgsdilem  15829  gausslemma2dlem0c  15853  gausslemma2dlem2  15864  gausslemma2dlem3  15865  lgsquadlem1  15879  lgsquadlem2  15880  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  nconstwlpolemgt0  16780