Theorem remulcld 10070

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

Syntax hints:   -> wi 4   e. wcel 1990  (class class class)co 6650   RRcr 9935   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9999

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mulge0  10546  msqge0  10549  redivcl  10744  prodgt0  10868  prodge0  10870  ltmul1a  10872  ltmul1  10873  ltmuldiv  10896  lt2msq1  10907  lt2msq  10908  le2msq  10923  msq11  10924  supmul1  10992  supmullem2  10994  supmul  10995  div4p1lem1div2  11287  mul2lt0rlt0  11932  mul2lt0bi  11936  qbtwnre  12030  xmulneg1  12099  xmulf  12102  lincmb01cmp  12315  iccf1o  12316  flmulnn0  12628  flhalf  12631  modcl  12672  mod0  12675  modge0  12678  modmulnn  12688  mulp1mod1  12711  2txmodxeq0  12730  modaddmulmod  12737  moddi  12738  modsubdir  12739  modirr  12741  addmodlteq  12745  bernneq  12990  bernneq3  12992  expnbnd  12993  expmulnbnd  12996  discr1  13000  discr  13001  faclbnd  13077  faclbnd6  13086  remullem  13868  sqrlem7  13989  sqrtmul  14000  abstri  14070  sqreulem  14099  mulcn2  14326  reccn2  14327  o1rlimmul  14349  lo1mul  14358  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  o1fsum  14545  cvgcmpce  14550  climcndslem1  14581  climcndslem2  14582  climcnds  14583  geomulcvg  14607  cvgrat  14615  mertenslem1  14616  fprodge1  14726  eftlub  14839  sin02gt0  14922  eirrlem  14932  bitsp1o  15155  isprm5  15419  modprm0  15510  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  2expltfac  15799  metss2lem  22316  nlmvscnlem2  22489  nrginvrcnlem  22495  nmoco  22541  nmotri  22543  nghmcn  22549  icopnfhmeo  22742  nmoleub2lem3  22915  ipcau2  23033  tchcphlem1  23034  ipcnlem2  23043  rrxcph  23180  csbren  23182  trirn  23183  pjthlem1  23208  opnmbllem  23369  vitalilem4  23380  itg1val2  23451  itg1cl  23452  itg1ge0  23453  itg1addlem4  23466  itg1mulc  23471  itg1ge0a  23478  itg1climres  23481  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2const2  23508  itg2mulclem  23513  itg2mulc  23514  itg2monolem1  23517  itg2monolem3  23519  itg2cnlem2  23529  iblconst  23584  iblmulc2  23597  itgmulc2lem1  23598  itgmulc2lem2  23599  bddmulibl  23605  dveflem  23742  cmvth  23754  dvlip  23756  dvlipcn  23757  dvivthlem1  23771  lhop1lem  23776  dvcvx  23783  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsum2  23797  ftc1lem4  23802  plyeq0lem  23966  aalioulem3  24089  aalioulem4  24090  aaliou3lem9  24105  ulmdvlem1  24154  itgulm  24162  radcnvlem1  24167  radcnvlem2  24168  dvradcnv  24175  abelthlem2  24186  abelthlem7  24192  tangtx  24257  tanregt0  24285  logdivlti  24366  logcnlem3  24390  logcnlem4  24391  logccv  24409  recxpcl  24421  cxpmul  24434  cxplt  24440  cxple2  24443  abscxpbnd  24494  lawcoslem1  24545  heron  24565  atans2  24658  efrlim  24696  o1cxp  24701  scvxcvx  24712  jensenlem2  24714  amgmlem  24716  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  relgamcl  24788  ftalem1  24799  ftalem2  24800  ftalem5  24803  basellem3  24809  basellem8  24814  chpub  24945  logfacubnd  24946  logfaclbnd  24947  logfacbnd3  24948  logexprlim  24950  perfectlem2  24955  bclbnd  25005  efexple  25006  bposlem1  25009  bposlem2  25010  bposlem6  25014  bposlem9  25017  lgsdilem  25049  gausslemma2dlem0c  25083  gausslemma2dlem2  25092  gausslemma2dlem3  25093  gausslemma2dlem6  25097  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1a1  25114  chebbnd1lem1  25158  chebbnd1lem3  25160  chtppilimlem1  25162  chpchtlim  25168  vmadivsum  25171  rplogsumlem1  25173  rpvmasumlem  25176  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0re  25202  dchrisum0lem1  25205  dirith2  25217  mulogsumlem  25220  mulogsum  25221  mulog2sumlem2  25224  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  logsqvma  25231  logsqvma2  25232  log2sumbnd  25233  selberglem2  25235  selberg  25237  selbergb  25238  selberg2lem  25239  selberg2b  25241  chpdifbndlem1  25242  chpdifbndlem2  25243  selberg3lem1  25246  selberg3lem2  25247  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrsumbnd2  25256  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntsf  25262  pntsval2  25265  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2a  25279  pntibndlem2  25280  pntlemb  25286  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntlem3  25298  ostth2lem1  25307  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth3  25327  ttgcontlem1  25765  brbtwn2  25785  colinearalglem4  25789  axsegconlem8  25804  axsegconlem9  25805  axsegconlem10  25806  ax5seglem3  25811  axpaschlem  25820  axpasch  25821  axeuclidlem  25842  numclwwlk5  27246  numclwwlk7  27249  smcnlem  27552  ubthlem2  27727  htthlem  27774  pjhthlem1  28250  cnlnadjlem7  28932  nmopcoadji  28960  branmfn  28964  leopnmid  28997  bhmafibid1  29644  2sqmod  29648  rmulccn  29974  xrge0iifhom  29983  nexple  30071  dya2icoseg  30339  eulerpartlems  30422  eulerpartlemgc  30424  eulerpartlemb  30430  plymulx0  30624  signsvtp  30660  reprgt  30699  breprexplemc  30710  circlemethhgt  30721  hgt750lemd  30726  logdivsqrle  30728  hgt750lem  30729  hgt750lemf  30731  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  tgoldbachgtde  30738  resconn  31228  knoppcnlem2  32484  knoppcnlem4  32486  knoppcnlem10  32492  unbdqndv2lem1  32500  unbdqndv2lem2  32501  knoppndvlem1  32503  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem19  32521  knoppndvlem20  32522  knoppndvlem21  32523  opnmbllem0  33445  itg2addnclem2  33462  itg2addnclem3  33463  iblmulc2nc  33475  itgmulc2nclem1  33476  bddiblnc  33480  ftc1cnnclem  33483  ftc1anclem3  33487  areacirclem4  33503  geomcau  33555  equivbnd  33589  bfplem1  33621  bfplem2  33622  bfp  33623  rrnequiv  33634  rrntotbnd  33635  irrapxlem1  37386  irrapxlem2  37387  irrapxlem3  37388  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pell14qrgt0  37423  pell1qrge1  37434  pell1qrgaplem  37437  pellqrexplicit  37441  pellqrex  37443  rmspecsqrtnq  37470  rmxycomplete  37482  rmxypos  37514  ltrmynn0  37515  ltrmxnn0  37516  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  jm2.27c  37574  jm3.1lem2  37585  areaquad  37802  imo72b2lem0  38465  cvgdvgrat  38512  nzprmdif  38518  lt3addmuld  39515  fperiodmullem  39517  fperiodmul  39518  lt4addmuld  39520  xralrple2  39570  xralrple3  39590  ltmulneg  39615  fmul01  39812  fmuldfeqlem1  39814  fmul01lt1lem1  39816  sumnnodd  39862  ltmod  39870  0ellimcdiv  39881  limclner  39883  dvdivbd  40138  dvbdfbdioolem2  40144  dvbdfbdioo  40145  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem1  40218  stoweidlem11  40228  stoweidlem13  40230  stoweidlem14  40231  stoweidlem16  40233  stoweidlem17  40234  stoweidlem22  40239  stoweidlem24  40241  stoweidlem25  40242  stoweidlem26  40243  stoweidlem30  40247  stoweidlem34  40251  stoweidlem36  40253  stoweidlem49  40266  stoweidlem59  40276  stoweidlem60  40277  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem15  40305  stirlingr  40307  dirker2re  40309  dirkerval2  40311  dirkerre  40312  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem4  40328  fourierdlem5  40329  fourierdlem6  40330  fourierdlem7  40331  fourierdlem16  40340  fourierdlem18  40342  fourierdlem19  40343  fourierdlem21  40345  fourierdlem22  40346  fourierdlem26  40350  fourierdlem35  40359  fourierdlem39  40363  fourierdlem41  40365  fourierdlem42  40366  fourierdlem43  40367  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem55  40378  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem66  40389  fourierdlem67  40390  fourierdlem68  40391  fourierdlem71  40394  fourierdlem72  40395  fourierdlem73  40396  fourierdlem76  40399  fourierdlem77  40400  fourierdlem78  40401  fourierdlem83  40406  fourierdlem84  40407  fourierdlem87  40410  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem94  40417  fourierdlem95  40418  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem23  40474  etransclem48  40499  rrndistlt  40510  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem4  40812  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  smfmul  41002  fmtno4prmfac  41484  lighneallem4a  41525  perfectALTVlem2  41631  ply1mulgsumlem2  42175  digvalnn0  42393  dignn0fr  42395  dig2nn0  42405  amgmwlem  42548