Theorem remulcld 8057

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 8007	. 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 2167  (class class class)co 5922   RRcr 7878   x. cmul 7884

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

This theorem is referenced by:  rimul  8612  ltmul1a  8618  ltmul1  8619  lemul1  8620  reapmul1lem  8621  reapmul1  8622  remulext1  8626  mulext1  8639  recexaplem2  8679  redivclap  8758  prodgt0gt0  8878  prodgt0  8879  prodge0  8881  lemul1a  8885  ltmuldiv  8901  ledivmul  8904  lt2mul2div  8906  lemuldiv  8908  lt2msq1  8912  lt2msq  8913  ltdiv23  8919  lediv23  8920  le2msq  8928  msq11  8929  div4p1lem1div2  9245  mul2lt0rlt0  9834  lincmb01cmp  10078  iccf1o  10079  qbtwnrelemcalc  10345  qbtwnre  10346  flhalf  10392  modqval  10416  modqge0  10424  modqmulnn  10434  bernneq  10752  bernneq3  10754  expnbnd  10755  nn0opthlem2d  10813  faclbnd  10833  faclbnd6  10836  remullem  11036  cvg1nlemres  11150  resqrexlemover  11175  resqrexlemnm  11183  resqrexlemglsq  11187  sqrtmul  11200  abstri  11269  maxabslemlub  11372  maxltsup  11383  bdtrilem  11404  mulcn2  11477  reccn2ap  11478  cvgratnnlembern  11688  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemabsle  11692  cvgratnnlemfm  11694  cvgratnnlemrate  11695  mertenslemi1  11700  fprodge1  11804  efcllem  11824  ege2le3  11836  eftlub  11855  sin02gt0  11929  cos12dec  11933  eirraplem  11942  dvdslelemd  12008  divalglemnqt  12085  bitsp1o  12117  2expltfac  12608  oddennn  12609  metss2lem  14733  dveflem  14962  sin0pilem1  15017  sin0pilem2  15018  tangtx  15074  logdivlti  15117  rpcxpcl  15139  cxpmul  15148  cxplt  15152  rpcxple2  15154  rpcxplt2  15155  apcxp2  15175  rpabscxpbnd  15176  perfectlem2  15236  lgsdilem  15268  gausslemma2dlem0c  15292  gausslemma2dlem2  15303  gausslemma2dlem3  15304  lgsquadlem1  15318  lgsquadlem2  15319  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  nconstwlpolemgt0  15708