Theorem remulcld 8210

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 8160	. 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 6018   RRcr 8031   x. cmul 8037

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

This theorem is referenced by:  rimul  8765  ltmul1a  8771  ltmul1  8772  lemul1  8773  reapmul1lem  8774  reapmul1  8775  remulext1  8779  mulext1  8792  recexaplem2  8832  redivclap  8911  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemul1a  9038  ltmuldiv  9054  ledivmul  9057  lt2mul2div  9059  lemuldiv  9061  lt2msq1  9065  lt2msq  9066  ltdiv23  9072  lediv23  9073  le2msq  9081  msq11  9082  div4p1lem1div2  9398  mul2lt0rlt0  9994  lincmb01cmp  10238  iccf1o  10239  qbtwnrelemcalc  10516  qbtwnre  10517  flhalf  10563  modqval  10587  modqge0  10595  modqmulnn  10605  bernneq  10923  bernneq3  10925  expnbnd  10926  nn0opthlem2d  10984  faclbnd  11004  faclbnd6  11007  remullem  11449  cvg1nlemres  11563  resqrexlemover  11588  resqrexlemnm  11596  resqrexlemglsq  11600  sqrtmul  11613  abstri  11682  maxabslemlub  11785  maxltsup  11796  bdtrilem  11817  mulcn2  11890  reccn2ap  11891  cvgratnnlembern  12102  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemabsle  12106  cvgratnnlemfm  12108  cvgratnnlemrate  12109  mertenslemi1  12114  fprodge1  12218  efcllem  12238  ege2le3  12250  eftlub  12269  sin02gt0  12343  cos12dec  12347  eirraplem  12356  dvdslelemd  12422  divalglemnqt  12499  bitsp1o  12532  2expltfac  13030  oddennn  13031  metss2lem  15240  dveflem  15469  sin0pilem1  15524  sin0pilem2  15525  tangtx  15581  logdivlti  15624  rpcxpcl  15646  cxpmul  15655  cxplt  15659  rpcxple2  15661  rpcxplt2  15662  apcxp2  15682  rpabscxpbnd  15683  perfectlem2  15743  lgsdilem  15775  gausslemma2dlem0c  15799  gausslemma2dlem2  15810  gausslemma2dlem3  15811  lgsquadlem1  15825  lgsquadlem2  15826  trilpolemclim  16691  trilpolemcl  16692  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  nconstwlpolemgt0  16720