Theorem remulcld 7950

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 7902	. 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 5853   RRcr 7773   x. cmul 7779

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

This theorem is referenced by:  rimul  8504  ltmul1a  8510  ltmul1  8511  lemul1  8512  reapmul1lem  8513  reapmul1  8514  remulext1  8518  mulext1  8531  recexaplem2  8570  redivclap  8648  prodgt0gt0  8767  prodgt0  8768  prodge0  8770  lemul1a  8774  ltmuldiv  8790  ledivmul  8793  lt2mul2div  8795  lemuldiv  8797  lt2msq1  8801  lt2msq  8802  ltdiv23  8808  lediv23  8809  le2msq  8817  msq11  8818  div4p1lem1div2  9131  mul2lt0rlt0  9716  lincmb01cmp  9960  iccf1o  9961  qbtwnrelemcalc  10212  qbtwnre  10213  flhalf  10258  modqval  10280  modqge0  10288  modqmulnn  10298  bernneq  10596  bernneq3  10598  expnbnd  10599  nn0opthlem2d  10655  faclbnd  10675  faclbnd6  10678  remullem  10835  cvg1nlemres  10949  resqrexlemover  10974  resqrexlemnm  10982  resqrexlemglsq  10986  sqrtmul  10999  abstri  11068  maxabslemlub  11171  maxltsup  11182  bdtrilem  11202  mulcn2  11275  reccn2ap  11276  cvgratnnlembern  11486  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemabsle  11490  cvgratnnlemfm  11492  cvgratnnlemrate  11493  mertenslemi1  11498  fprodge1  11602  efcllem  11622  ege2le3  11634  eftlub  11653  sin02gt0  11726  cos12dec  11730  eirraplem  11739  dvdslelemd  11803  divalglemnqt  11879  oddennn  12347  metss2lem  13291  dveflem  13481  sin0pilem1  13496  sin0pilem2  13497  tangtx  13553  logdivlti  13596  rpcxpcl  13618  cxpmul  13627  cxplt  13630  rpcxple2  13632  rpcxplt2  13633  apcxp2  13652  rpabscxpbnd  13653  lgsdilem  13722  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  nconstwlpolemgt0  14095