Theorem remulcld 7988

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 7939	. 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 2148  (class class class)co 5875   RRcr 7810   x. cmul 7816

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

This theorem is referenced by:  rimul  8542  ltmul1a  8548  ltmul1  8549  lemul1  8550  reapmul1lem  8551  reapmul1  8552  remulext1  8556  mulext1  8569  recexaplem2  8609  redivclap  8688  prodgt0gt0  8808  prodgt0  8809  prodge0  8811  lemul1a  8815  ltmuldiv  8831  ledivmul  8834  lt2mul2div  8836  lemuldiv  8838  lt2msq1  8842  lt2msq  8843  ltdiv23  8849  lediv23  8850  le2msq  8858  msq11  8859  div4p1lem1div2  9172  mul2lt0rlt0  9759  lincmb01cmp  10003  iccf1o  10004  qbtwnrelemcalc  10256  qbtwnre  10257  flhalf  10302  modqval  10324  modqge0  10332  modqmulnn  10342  bernneq  10641  bernneq3  10643  expnbnd  10644  nn0opthlem2d  10701  faclbnd  10721  faclbnd6  10724  remullem  10880  cvg1nlemres  10994  resqrexlemover  11019  resqrexlemnm  11027  resqrexlemglsq  11031  sqrtmul  11044  abstri  11113  maxabslemlub  11216  maxltsup  11227  bdtrilem  11247  mulcn2  11320  reccn2ap  11321  cvgratnnlembern  11531  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemabsle  11535  cvgratnnlemfm  11537  cvgratnnlemrate  11538  mertenslemi1  11543  fprodge1  11647  efcllem  11667  ege2le3  11679  eftlub  11698  sin02gt0  11771  cos12dec  11775  eirraplem  11784  dvdslelemd  11849  divalglemnqt  11925  oddennn  12393  metss2lem  14000  dveflem  14190  sin0pilem1  14205  sin0pilem2  14206  tangtx  14262  logdivlti  14305  rpcxpcl  14327  cxpmul  14336  cxplt  14339  rpcxple2  14341  rpcxplt2  14342  apcxp2  14361  rpabscxpbnd  14362  lgsdilem  14431  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  nconstwlpolemgt0  14814