Theorem remulcld 8346

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 8297	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 2209  (class class class)co 6075   RRcr 8168   x. cmul 8174

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

This theorem is referenced by:  rimul  8903  ltmul1a  8909  ltmul1  8910  lemul1  8911  reapmul1lem  8912  reapmul1  8913  remulext1  8917  mulext1  8930  recexaplem2  8970  redivclap  9051  prodgt0gt0  9171  prodgt0  9172  prodge0  9174  lemul1a  9178  ltmuldiv  9194  ledivmul  9197  lt2mul2div  9199  lemuldiv  9201  lt2msq1  9205  lt2msq  9206  ltdiv23  9212  lediv23  9213  le2msq  9221  msq11  9222  div4p1lem1div2  9538  mul2lt0rlt0  10139  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  qbtwnrelemcalc  10668  qbtwnre  10669  flhalf  10715  modqval  10739  modqge0  10747  modqmulnn  10757  bernneq  11076  bernneq3  11078  expnbnd  11079  nn0opthlem2d  11137  faclbnd  11157  faclbnd6  11160  remullem  11614  sq01  11638  cvg1nlemres  11729  resqrexlemover  11754  resqrexlemnm  11762  resqrexlemglsq  11766  sqrtmul  11779  abstri  11848  maxabslemlub  11951  maxltsup  11962  bdtrilem  11983  mulcn2  12056  reccn2ap  12057  cvgratnnlembern  12268  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemabsle  12272  cvgratnnlemfm  12274  cvgratnnlemrate  12275  mertenslemi1  12280  fprodge1  12384  efcllem  12404  ege2le3  12416  eftlub  12435  sin02gt0  12509  cos12dec  12513  eirraplem  12522  dvdslelemd  12588  divalglemnqt  12665  bitsp1o  12698  2expltfac  13196  oddennn  13261  metss2lem  15521  dveflem  15750  sin0pilem1  15805  sin0pilem2  15806  tangtx  15862  logdivlti  15905  rpcxpcl  15928  cxpmul  15937  cxplt  15941  rpcxple2  15943  rpcxplt2  15944  apcxp2  15964  rpabscxpbnd  15965  pellexlem2  16006  perfectlem2  16028  lgsdilem  16060  gausslemma2dlem0c  16084  gausslemma2dlem2  16095  gausslemma2dlem3  16096  lgsquadlem1  16110  lgsquadlem2  16111  dichmul0orlem1  16667  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  nconstwlpolemgt0  17019