Theorem remulcld 8050

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 8000	. 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 2164  (class class class)co 5918   RRcr 7871   x. cmul 7877

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

This theorem is referenced by:  rimul  8604  ltmul1a  8610  ltmul1  8611  lemul1  8612  reapmul1lem  8613  reapmul1  8614  remulext1  8618  mulext1  8631  recexaplem2  8671  redivclap  8750  prodgt0gt0  8870  prodgt0  8871  prodge0  8873  lemul1a  8877  ltmuldiv  8893  ledivmul  8896  lt2mul2div  8898  lemuldiv  8900  lt2msq1  8904  lt2msq  8905  ltdiv23  8911  lediv23  8912  le2msq  8920  msq11  8921  div4p1lem1div2  9236  mul2lt0rlt0  9825  lincmb01cmp  10069  iccf1o  10070  qbtwnrelemcalc  10324  qbtwnre  10325  flhalf  10371  modqval  10395  modqge0  10403  modqmulnn  10413  bernneq  10731  bernneq3  10733  expnbnd  10734  nn0opthlem2d  10792  faclbnd  10812  faclbnd6  10815  remullem  11015  cvg1nlemres  11129  resqrexlemover  11154  resqrexlemnm  11162  resqrexlemglsq  11166  sqrtmul  11179  abstri  11248  maxabslemlub  11351  maxltsup  11362  bdtrilem  11382  mulcn2  11455  reccn2ap  11456  cvgratnnlembern  11666  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemabsle  11670  cvgratnnlemfm  11672  cvgratnnlemrate  11673  mertenslemi1  11678  fprodge1  11782  efcllem  11802  ege2le3  11814  eftlub  11833  sin02gt0  11907  cos12dec  11911  eirraplem  11920  dvdslelemd  11985  divalglemnqt  12061  oddennn  12549  metss2lem  14665  dveflem  14872  sin0pilem1  14916  sin0pilem2  14917  tangtx  14973  logdivlti  15016  rpcxpcl  15038  cxpmul  15047  cxplt  15050  rpcxple2  15052  rpcxplt2  15053  apcxp2  15072  rpabscxpbnd  15073  lgsdilem  15143  gausslemma2dlem0c  15167  gausslemma2dlem2  15178  gausslemma2dlem3  15179  lgsquadlem1  15191  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  nconstwlpolemgt0  15554