Theorem remulcld 8138

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 8088	. 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 2178  (class class class)co 5967   RRcr 7959   x. cmul 7965

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

This theorem is referenced by:  rimul  8693  ltmul1a  8699  ltmul1  8700  lemul1  8701  reapmul1lem  8702  reapmul1  8703  remulext1  8707  mulext1  8720  recexaplem2  8760  redivclap  8839  prodgt0gt0  8959  prodgt0  8960  prodge0  8962  lemul1a  8966  ltmuldiv  8982  ledivmul  8985  lt2mul2div  8987  lemuldiv  8989  lt2msq1  8993  lt2msq  8994  ltdiv23  9000  lediv23  9001  le2msq  9009  msq11  9010  div4p1lem1div2  9326  mul2lt0rlt0  9916  lincmb01cmp  10160  iccf1o  10161  qbtwnrelemcalc  10435  qbtwnre  10436  flhalf  10482  modqval  10506  modqge0  10514  modqmulnn  10524  bernneq  10842  bernneq3  10844  expnbnd  10845  nn0opthlem2d  10903  faclbnd  10923  faclbnd6  10926  remullem  11297  cvg1nlemres  11411  resqrexlemover  11436  resqrexlemnm  11444  resqrexlemglsq  11448  sqrtmul  11461  abstri  11530  maxabslemlub  11633  maxltsup  11644  bdtrilem  11665  mulcn2  11738  reccn2ap  11739  cvgratnnlembern  11949  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemabsle  11953  cvgratnnlemfm  11955  cvgratnnlemrate  11956  mertenslemi1  11961  fprodge1  12065  efcllem  12085  ege2le3  12097  eftlub  12116  sin02gt0  12190  cos12dec  12194  eirraplem  12203  dvdslelemd  12269  divalglemnqt  12346  bitsp1o  12379  2expltfac  12877  oddennn  12878  metss2lem  15084  dveflem  15313  sin0pilem1  15368  sin0pilem2  15369  tangtx  15425  logdivlti  15468  rpcxpcl  15490  cxpmul  15499  cxplt  15503  rpcxple2  15505  rpcxplt2  15506  apcxp2  15526  rpabscxpbnd  15527  perfectlem2  15587  lgsdilem  15619  gausslemma2dlem0c  15643  gausslemma2dlem2  15654  gausslemma2dlem3  15655  lgsquadlem1  15669  lgsquadlem2  15670  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  nconstwlpolemgt0  16205