Theorem remulcld 8200

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 8150	. 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 2200  (class class class)co 6013   RRcr 8021   x. cmul 8027

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

This theorem is referenced by:  rimul  8755  ltmul1a  8761  ltmul1  8762  lemul1  8763  reapmul1lem  8764  reapmul1  8765  remulext1  8769  mulext1  8782  recexaplem2  8822  redivclap  8901  prodgt0gt0  9021  prodgt0  9022  prodge0  9024  lemul1a  9028  ltmuldiv  9044  ledivmul  9047  lt2mul2div  9049  lemuldiv  9051  lt2msq1  9055  lt2msq  9056  ltdiv23  9062  lediv23  9063  le2msq  9071  msq11  9072  div4p1lem1div2  9388  mul2lt0rlt0  9984  lincmb01cmp  10228  iccf1o  10229  qbtwnrelemcalc  10505  qbtwnre  10506  flhalf  10552  modqval  10576  modqge0  10584  modqmulnn  10594  bernneq  10912  bernneq3  10914  expnbnd  10915  nn0opthlem2d  10973  faclbnd  10993  faclbnd6  10996  remullem  11422  cvg1nlemres  11536  resqrexlemover  11561  resqrexlemnm  11569  resqrexlemglsq  11573  sqrtmul  11586  abstri  11655  maxabslemlub  11758  maxltsup  11769  bdtrilem  11790  mulcn2  11863  reccn2ap  11864  cvgratnnlembern  12074  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemabsle  12078  cvgratnnlemfm  12080  cvgratnnlemrate  12081  mertenslemi1  12086  fprodge1  12190  efcllem  12210  ege2le3  12222  eftlub  12241  sin02gt0  12315  cos12dec  12319  eirraplem  12328  dvdslelemd  12394  divalglemnqt  12471  bitsp1o  12504  2expltfac  13002  oddennn  13003  metss2lem  15211  dveflem  15440  sin0pilem1  15495  sin0pilem2  15496  tangtx  15552  logdivlti  15595  rpcxpcl  15617  cxpmul  15626  cxplt  15630  rpcxple2  15632  rpcxplt2  15633  apcxp2  15653  rpabscxpbnd  15654  perfectlem2  15714  lgsdilem  15746  gausslemma2dlem0c  15770  gausslemma2dlem2  15781  gausslemma2dlem3  15782  lgsquadlem1  15796  lgsquadlem2  15797  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  nconstwlpolemgt0  16604