Theorem remulcld 7937

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

Syntax hints:   -> wi 4   e. wcel 2141  (class class class)co 5850   RRcr 7760   x. cmul 7766

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

This theorem is referenced by:  rimul  8491  ltmul1a  8497  ltmul1  8498  lemul1  8499  reapmul1lem  8500  reapmul1  8501  remulext1  8505  mulext1  8518  recexaplem2  8557  redivclap  8635  prodgt0gt0  8754  prodgt0  8755  prodge0  8757  lemul1a  8761  ltmuldiv  8777  ledivmul  8780  lt2mul2div  8782  lemuldiv  8784  lt2msq1  8788  lt2msq  8789  ltdiv23  8795  lediv23  8796  le2msq  8804  msq11  8805  div4p1lem1div2  9118  mul2lt0rlt0  9703  lincmb01cmp  9947  iccf1o  9948  qbtwnrelemcalc  10199  qbtwnre  10200  flhalf  10245  modqval  10267  modqge0  10275  modqmulnn  10285  bernneq  10583  bernneq3  10585  expnbnd  10586  nn0opthlem2d  10642  faclbnd  10662  faclbnd6  10665  remullem  10822  cvg1nlemres  10936  resqrexlemover  10961  resqrexlemnm  10969  resqrexlemglsq  10973  sqrtmul  10986  abstri  11055  maxabslemlub  11158  maxltsup  11169  bdtrilem  11189  mulcn2  11262  reccn2ap  11263  cvgratnnlembern  11473  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  cvgratnnlemabsle  11477  cvgratnnlemfm  11479  cvgratnnlemrate  11480  mertenslemi1  11485  fprodge1  11589  efcllem  11609  ege2le3  11621  eftlub  11640  sin02gt0  11713  cos12dec  11717  eirraplem  11726  dvdslelemd  11790  divalglemnqt  11866  oddennn  12334  metss2lem  13212  dveflem  13402  sin0pilem1  13417  sin0pilem2  13418  tangtx  13474  logdivlti  13517  rpcxpcl  13539  cxpmul  13548  cxplt  13551  rpcxple2  13553  rpcxplt2  13554  apcxp2  13573  rpabscxpbnd  13574  lgsdilem  13643  trilpolemclim  13990  trilpolemcl  13991  trilpolemisumle  13992  trilpolemeq1  13994  trilpolemlt1  13995  nconstwlpolemgt0  14017