Theorem remulcld 7925

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 7877	. 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 2136  (class class class)co 5841   RRcr 7748   x. cmul 7754

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

This theorem is referenced by:  rimul  8479  ltmul1a  8485  ltmul1  8486  lemul1  8487  reapmul1lem  8488  reapmul1  8489  remulext1  8493  mulext1  8506  recexaplem2  8545  redivclap  8623  prodgt0gt0  8742  prodgt0  8743  prodge0  8745  lemul1a  8749  ltmuldiv  8765  ledivmul  8768  lt2mul2div  8770  lemuldiv  8772  lt2msq1  8776  lt2msq  8777  ltdiv23  8783  lediv23  8784  le2msq  8792  msq11  8793  div4p1lem1div2  9106  mul2lt0rlt0  9691  lincmb01cmp  9935  iccf1o  9936  qbtwnrelemcalc  10187  qbtwnre  10188  flhalf  10233  modqval  10255  modqge0  10263  modqmulnn  10273  bernneq  10571  bernneq3  10573  expnbnd  10574  nn0opthlem2d  10630  faclbnd  10650  faclbnd6  10653  remullem  10809  cvg1nlemres  10923  resqrexlemover  10948  resqrexlemnm  10956  resqrexlemglsq  10960  sqrtmul  10973  abstri  11042  maxabslemlub  11145  maxltsup  11156  bdtrilem  11176  mulcn2  11249  reccn2ap  11250  cvgratnnlembern  11460  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemabsle  11464  cvgratnnlemfm  11466  cvgratnnlemrate  11467  mertenslemi1  11472  fprodge1  11576  efcllem  11596  ege2le3  11608  eftlub  11627  sin02gt0  11700  cos12dec  11704  eirraplem  11713  dvdslelemd  11777  divalglemnqt  11853  oddennn  12321  metss2lem  13097  dveflem  13287  sin0pilem1  13302  sin0pilem2  13303  tangtx  13359  logdivlti  13402  rpcxpcl  13424  cxpmul  13433  cxplt  13436  rpcxple2  13438  rpcxplt2  13439  apcxp2  13458  rpabscxpbnd  13459  lgsdilem  13528  trilpolemclim  13875  trilpolemcl  13876  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  nconstwlpolemgt0  13902