Theorem remulcld 8362

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 8313	. 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 )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6088   RRcr 8184   x. cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8284

This theorem is used by:  rimul  8921  ltmul1a  8927  ltmul1  8928  lemul1  8929  reapmul1lem  8930  reapmul1  8931  remulext1  8935  mulext1  8948  recexaplem2  8988  redivclap  9069  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  lemul1a  9196  ltmuldiv  9212  ledivmul  9215  lt2mul2div  9217  lemuldiv  9219  lt2msq1  9223  lt2msq  9224  ltdiv23  9230  lediv23  9231  le2msq  9239  msq11  9240  div4p1lem1div2  9570  mul2lt0rlt0  10177  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  qbtwnrelemcalc  10707  qbtwnre  10708  flhalf  10758  modqval  10782  modqge0  10790  modqmulnn  10800  bernneq  11119  bernneq3  11121  expnbnd  11122  nn0opthlem2d  11181  faclbnd  11201  faclbnd6  11204  remullem  11658  sq01  11682  cvg1nlemres  11773  resqrexlemover  11798  resqrexlemnm  11806  resqrexlemglsq  11810  sqrtmul  11823  abstri  11893  maxabslemlub  11996  maxltsup  12007  bdtrilem  12030  mulcn2  12103  reccn2ap  12104  cvgratnnlembern  12315  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemabsle  12319  cvgratnnlemfm  12321  cvgratnnlemrate  12322  mertenslemi1  12327  fprodge1  12431  efcllem  12451  ege2le3  12463  eftlub  12482  sin02gt0  12556  cos12dec  12560  eirraplem  12569  dvdslelemd  12635  divalglemnqt  12712  bitsp1o  12745  2expltfac  13248  oddennn  13341  metss2lem  15723  dveflem  15952  sin0pilem1  16008  sin0pilem2  16009  tangtx  16065  logdivlti  16111  rpcxpcl  16136  cxpmul  16145  cxplt  16151  rpcxple2  16153  rpcxplt2  16154  apcxp2  16174  rpabscxpbnd  16175  log2tlbndlog2  16220  pellexlem2  16230  perfectlem2  16300  bclbnd  16307  prmefexple  16308  bposlem1  16311  bposlem2  16312  bposlem6  16316  bposlem9  16319  lgsdilem  16351  gausslemma2dlem0c  16375  gausslemma2dlem2  16386  gausslemma2dlem3  16387  lgsquadlem1  16401  lgsquadlem2  16402  dichmul0orlem1  16958  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  nconstwlpolemgt0  17321