Theorem remulcld 8362

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 8313	. 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 6088   RRcr 8184   x. cmul 8190

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

This theorem is used by:  rimul  8921  ltmul1a  8927  ltmul1  8928  lemul1  8929  reapmul1lem  8930  reapmul1  8931  remulext1  8935  mulext1  8948  recexaplem2  8988  redivclap  9069  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  lemul1a  9196  ltmuldiv  9212  ledivmul  9215  lt2mul2div  9217  lemuldiv  9219  lt2msq1  9223  lt2msq  9224  ltdiv23  9230  lediv23  9231  le2msq  9239  msq11  9240  div4p1lem1div2  9570  mul2lt0rlt0  10176  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  qbtwnrelemcalc  10706  qbtwnre  10707  flhalf  10757  modqval  10781  modqge0  10789  modqmulnn  10799  bernneq  11118  bernneq3  11120  expnbnd  11121  nn0opthlem2d  11180  faclbnd  11200  faclbnd6  11203  remullem  11657  sq01  11681  cvg1nlemres  11772  resqrexlemover  11797  resqrexlemnm  11805  resqrexlemglsq  11809  sqrtmul  11822  abstri  11892  maxabslemlub  11995  maxltsup  12006  bdtrilem  12029  mulcn2  12102  reccn2ap  12103  cvgratnnlembern  12314  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemabsle  12318  cvgratnnlemfm  12320  cvgratnnlemrate  12321  mertenslemi1  12326  fprodge1  12430  efcllem  12450  ege2le3  12462  eftlub  12481  sin02gt0  12555  cos12dec  12559  eirraplem  12568  dvdslelemd  12634  divalglemnqt  12711  bitsp1o  12744  2expltfac  13247  oddennn  13340  metss2lem  15740  dveflem  15969  sin0pilem1  16025  sin0pilem2  16026  tangtx  16082  logdivlti  16128  rpcxpcl  16153  cxpmul  16162  cxplt  16168  rpcxple2  16170  rpcxplt2  16171  apcxp2  16191  rpabscxpbnd  16192  log2tlbndlog2  16237  pellexlem2  16247  perfectlem2  16317  bclbnd  16324  prmefexple  16325  bposlem1  16328  bposlem2  16329  bposlem6  16333  bposlem9  16336  lgsdilem  16368  gausslemma2dlem0c  16392  gausslemma2dlem2  16403  gausslemma2dlem3  16404  lgsquadlem1  16418  lgsquadlem2  16419  dichmul0orlem1  16975  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  nconstwlpolemgt0  17338