Theorem remulcld 8105

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 8055	. 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 2176  (class class class)co 5946   RRcr 7926   x. cmul 7932

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

This theorem is referenced by:  rimul  8660  ltmul1a  8666  ltmul1  8667  lemul1  8668  reapmul1lem  8669  reapmul1  8670  remulext1  8674  mulext1  8687  recexaplem2  8727  redivclap  8806  prodgt0gt0  8926  prodgt0  8927  prodge0  8929  lemul1a  8933  ltmuldiv  8949  ledivmul  8952  lt2mul2div  8954  lemuldiv  8956  lt2msq1  8960  lt2msq  8961  ltdiv23  8967  lediv23  8968  le2msq  8976  msq11  8977  div4p1lem1div2  9293  mul2lt0rlt0  9883  lincmb01cmp  10127  iccf1o  10128  qbtwnrelemcalc  10400  qbtwnre  10401  flhalf  10447  modqval  10471  modqge0  10479  modqmulnn  10489  bernneq  10807  bernneq3  10809  expnbnd  10810  nn0opthlem2d  10868  faclbnd  10888  faclbnd6  10891  remullem  11215  cvg1nlemres  11329  resqrexlemover  11354  resqrexlemnm  11362  resqrexlemglsq  11366  sqrtmul  11379  abstri  11448  maxabslemlub  11551  maxltsup  11562  bdtrilem  11583  mulcn2  11656  reccn2ap  11657  cvgratnnlembern  11867  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratnnlemabsle  11871  cvgratnnlemfm  11873  cvgratnnlemrate  11874  mertenslemi1  11879  fprodge1  11983  efcllem  12003  ege2le3  12015  eftlub  12034  sin02gt0  12108  cos12dec  12112  eirraplem  12121  dvdslelemd  12187  divalglemnqt  12264  bitsp1o  12297  2expltfac  12795  oddennn  12796  metss2lem  15002  dveflem  15231  sin0pilem1  15286  sin0pilem2  15287  tangtx  15343  logdivlti  15386  rpcxpcl  15408  cxpmul  15417  cxplt  15421  rpcxple2  15423  rpcxplt2  15424  apcxp2  15444  rpabscxpbnd  15445  perfectlem2  15505  lgsdilem  15537  gausslemma2dlem0c  15561  gausslemma2dlem2  15572  gausslemma2dlem3  15573  lgsquadlem1  15587  lgsquadlem2  15588  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  nconstwlpolemgt0  16040