Theorem remulcld 8209

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 8159	. 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 2202  (class class class)co 6017   RRcr 8030   x. cmul 8036

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

This theorem is referenced by:  rimul  8764  ltmul1a  8770  ltmul1  8771  lemul1  8772  reapmul1lem  8773  reapmul1  8774  remulext1  8778  mulext1  8791  recexaplem2  8831  redivclap  8910  prodgt0gt0  9030  prodgt0  9031  prodge0  9033  lemul1a  9037  ltmuldiv  9053  ledivmul  9056  lt2mul2div  9058  lemuldiv  9060  lt2msq1  9064  lt2msq  9065  ltdiv23  9071  lediv23  9072  le2msq  9080  msq11  9081  div4p1lem1div2  9397  mul2lt0rlt0  9993  lincmb01cmp  10237  iccf1o  10238  qbtwnrelemcalc  10514  qbtwnre  10515  flhalf  10561  modqval  10585  modqge0  10593  modqmulnn  10603  bernneq  10921  bernneq3  10923  expnbnd  10924  nn0opthlem2d  10982  faclbnd  11002  faclbnd6  11005  remullem  11431  cvg1nlemres  11545  resqrexlemover  11570  resqrexlemnm  11578  resqrexlemglsq  11582  sqrtmul  11595  abstri  11664  maxabslemlub  11767  maxltsup  11778  bdtrilem  11799  mulcn2  11872  reccn2ap  11873  cvgratnnlembern  12083  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemabsle  12087  cvgratnnlemfm  12089  cvgratnnlemrate  12090  mertenslemi1  12095  fprodge1  12199  efcllem  12219  ege2le3  12231  eftlub  12250  sin02gt0  12324  cos12dec  12328  eirraplem  12337  dvdslelemd  12403  divalglemnqt  12480  bitsp1o  12513  2expltfac  13011  oddennn  13012  metss2lem  15220  dveflem  15449  sin0pilem1  15504  sin0pilem2  15505  tangtx  15561  logdivlti  15604  rpcxpcl  15626  cxpmul  15635  cxplt  15639  rpcxple2  15641  rpcxplt2  15642  apcxp2  15662  rpabscxpbnd  15663  perfectlem2  15723  lgsdilem  15755  gausslemma2dlem0c  15779  gausslemma2dlem2  15790  gausslemma2dlem3  15791  lgsquadlem1  15805  lgsquadlem2  15806  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  nconstwlpolemgt0  16668