Theorem remulcld 8357

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6085   RRcr 8179   x. cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8279

This theorem is used by:  rimul  8916  ltmul1a  8922  ltmul1  8923  lemul1  8924  reapmul1lem  8925  reapmul1  8926  remulext1  8930  mulext1  8943  recexaplem2  8983  redivclap  9064  prodgt0gt0  9184  prodgt0  9185  prodge0  9187  lemul1a  9191  ltmuldiv  9207  ledivmul  9210  lt2mul2div  9212  lemuldiv  9214  lt2msq1  9218  lt2msq  9219  ltdiv23  9225  lediv23  9226  le2msq  9234  msq11  9235  div4p1lem1div2  9564  mul2lt0rlt0  10171  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  qbtwnrelemcalc  10701  qbtwnre  10702  flhalf  10752  modqval  10776  modqge0  10784  modqmulnn  10794  bernneq  11113  bernneq3  11115  expnbnd  11116  nn0opthlem2d  11175  faclbnd  11195  faclbnd6  11198  remullem  11652  sq01  11676  cvg1nlemres  11767  resqrexlemover  11792  resqrexlemnm  11800  resqrexlemglsq  11804  sqrtmul  11817  abstri  11887  maxabslemlub  11990  maxltsup  12001  bdtrilem  12024  mulcn2  12097  reccn2ap  12098  cvgratnnlembern  12309  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemabsle  12313  cvgratnnlemfm  12315  cvgratnnlemrate  12316  mertenslemi1  12321  fprodge1  12425  efcllem  12445  ege2le3  12457  eftlub  12476  sin02gt0  12550  cos12dec  12554  eirraplem  12563  dvdslelemd  12629  divalglemnqt  12706  bitsp1o  12739  2expltfac  13242  oddennn  13335  metss2lem  15689  dveflem  15918  sin0pilem1  15974  sin0pilem2  15975  tangtx  16031  logdivlti  16075  rpcxpcl  16100  cxpmul  16109  cxplt  16113  rpcxple2  16115  rpcxplt2  16116  apcxp2  16136  rpabscxpbnd  16137  log2tlbndlog2  16181  pellexlem2  16191  perfectlem2  16261  bclbnd  16268  prmefexple  16269  bposlem1  16272  bposlem2  16273  bposlem6  16277  bposlem9  16280  lgsdilem  16312  gausslemma2dlem0c  16336  gausslemma2dlem2  16347  gausslemma2dlem3  16348  lgsquadlem1  16362  lgsquadlem2  16363  dichmul0orlem1  16919  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  nconstwlpolemgt0  17281