Theorem mulcld 10060

Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	|- ( ph -> A e. CC )
addcld.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
mulcld	|- ( ph -> ( A x. B ) e. CC )

Proof of Theorem mulcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		mulcl 10020	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( A x. B ) e. CC )

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

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

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

This theorem is referenced by:  mul02lem1  10212  addid1  10216  cnegex  10217  kcnktkm1cn  10461  receu  10672  divrec  10701  divcan3  10711  muldivdir  10720  divdivdiv  10726  divsubdiv  10741  cru  11012  mul2lt0rlt0  11932  lincmb01cmp  12315  iccf1o  12316  flpmodeq  12673  moddiffl  12681  modvalp1  12689  modcyc  12705  modadd1  12707  modmuladdnn0  12714  modmul1  12723  modaddmulmod  12737  mulexpz  12900  expmulz  12906  binom3  12985  bernneq  12990  mulsubdivbinom2  13046  muldivbinom2  13047  remullem  13868  cjreim2  13901  absimle  14049  abstri  14070  sqreulem  14099  sqreu  14100  mulcn2  14326  reccn2  14327  o1rlimmul  14349  isummulc2  14493  fsummulc2  14516  fsumparts  14538  binomlem  14561  binom1dif  14565  incexclem  14568  incexc  14569  incexc2  14570  geomulcvg  14607  mertenslem1  14616  mertens  14618  fprodmul  14690  fprodn0f  14722  iprodmul  14734  binomfallfaclem1  14770  binomfallfaclem2  14771  binomrisefac  14773  bpolycl  14783  bpolysum  14784  bpolydiflem  14785  bpoly4  14790  efaddlem  14823  sinadd  14894  cosadd  14895  tanaddlem  14896  tanadd  14897  addsin  14900  sincossq  14906  sin2t  14907  dvds2ln  15014  oddm1even  15067  pwp1fsum  15114  flodddiv4  15137  sadadd2lem2  15172  bezoutlem2  15257  bezoutlem3  15258  bezoutlem4  15259  lcmgcdlem  15319  phiprmpw  15481  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem16  15535  pcpremul  15548  pcaddlem  15592  fldivp1  15601  mul4sqlem  15657  4sqlem14  15662  vdwapun  15678  vdwlem2  15686  vdwlem6  15690  zringlpirlem3  19834  znunit  19912  blcvx  22601  icopnfcnv  22741  cphipipcj  23000  cphipval2  23040  4cphipval2  23041  cphipval  23042  mbfmulc2re  23415  mbfmulc2  23430  itg1addlem4  23466  itg1addlem5  23467  itg1mulc  23471  mbfmul  23493  itgcl  23550  itgcnlem  23556  iblmulc2  23597  itgmulc2  23600  itgabs  23601  itgsplit  23602  dvmulbr  23702  dvcmul  23707  dvcmulf  23708  dvexp  23716  dvmptcmul  23727  dvmptdiv  23737  dvexp3  23741  dvsincos  23744  cmvth  23754  dvlipcn  23757  dvfsumabs  23786  dvfsumlem1  23789  ftc1lem4  23802  itgparts  23810  plyf  23954  ply1termlem  23959  plyeq0lem  23966  plypf1  23968  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coeidlem  23993  coeid3  23996  plyco  23997  coemullem  24006  coemulhi  24010  coemulc  24011  dgrcolem2  24030  plycjlem  24032  plyrecj  24035  dvply1  24039  vieta1lem2  24066  vieta1  24067  elqaalem3  24076  aareccl  24081  aalioulem1  24087  taylfvallem1  24111  tayl0  24116  dvtaylp  24124  taylthlem2  24128  psergf  24166  radcnvlem1  24167  dvradcnv  24175  psercn2  24177  pserdvlem2  24182  pserdv2  24184  abelthlem4  24188  abelthlem5  24189  abelthlem6  24190  abelthlem7  24192  abelthlem9  24194  tanregt0  24285  efgh  24287  efabl  24296  efsubm  24297  cosargd  24354  abslogle  24364  tanarg  24365  advlogexp  24401  logtayllem  24405  logtayl  24406  cxpadd  24425  mulcxp  24431  cxpmul  24434  cxpmul2  24435  cxpmul2z  24437  abscxp  24438  abscxp2  24439  dvcxp2  24482  abscxpbnd  24494  root1eq1  24496  cxpeq  24498  angcan  24532  pythag  24547  ssscongptld  24552  affineequiv  24553  affineequiv2  24554  chordthmlem2  24560  chordthmlem3  24561  chordthmlem4  24562  chordthmlem5  24563  heron  24565  quad2  24566  quad  24567  dcubic1lem  24570  dcubic2  24571  dcubic1  24572  dcubic  24573  mcubic  24574  cubic2  24575  cubic  24576  binom4  24577  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1cl  24581  quart1lem  24582  quart1  24583  quartlem1  24584  quartlem2  24585  atantayl3  24666  leibpi  24669  birthdaylem2  24679  divsqrtsumo1  24710  cvxcl  24711  jensenlem2  24714  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  wilthlem2  24795  ftalem1  24799  ftalem2  24800  ftalem4  24802  ftalem5  24803  basellem2  24808  basellem3  24809  basellem8  24814  muinv  24919  fsumdvdsmul  24921  logfacrlim  24949  logexprlim  24950  perfectlem2  24955  bposlem9  25017  gausslemma2dlem4  25094  lgsquad2lem1  25109  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2sqlem3  25145  rplogsumlem1  25173  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasum2if  25186  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  rpvmasum2  25201  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrmusumlem  25211  dchrvmasumlem  25212  rplogsum  25216  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem1  25223  mulog2sumlem2  25224  mulog2sumlem3  25225  vmalogdivsum  25228  logsqvma  25231  log2sumbnd  25233  selberglem1  25234  selberglem2  25235  selberglem3  25236  selberg  25237  selberg2lem  25239  selberg2  25240  selberg3lem1  25246  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  selbergr  25257  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntsval2  25265  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntlemb  25286  pntlemf  25294  pntlemo  25296  ostth2lem2  25323  ostth2lem3  25324  ttgcontlem1  25765  brbtwn2  25785  colinearalg  25790  ax5seglem2  25809  ax5seglem9  25817  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  finsumvtxdg2ssteplem4  26444  ex-ind-dvds  27318  ipval2  27562  dipcl  27567  riesz3i  28921  dpfrac1  29599  bhmafibid1  29644  bhmafibid2  29645  2sqmod  29648  cnre2csqima  29957  rmulccn  29974  indsum  30083  indsumin  30084  dya2icoseg  30339  oddpwdc  30416  eulerpartlems  30422  eulerpartlemsv3  30423  eulerpartlemgs2  30442  signsplypnf  30627  itgexpif  30684  breprexplemc  30710  breprexp  30711  vtscl  30716  vtsprod  30717  circlemeth  30718  logdivsqrle  30728  hgt750lemf  30731  hgt750leme  30736  subfacval2  31169  subfaclim  31170  resconn  31228  subdivcomb1  31611  subdivcomb2  31612  iprodgam  31628  fwddifnp1  32272  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem9  32511  knoppndvlem11  32513  knoppndvlem14  32516  knoppndvlem16  32518  knoppndvlem17  32519  bj-subcom  33154  bj-lineq  33158  bj-bary1lem  33160  bj-bary1lem1  33161  bj-bary1  33162  iblmulc2nc  33475  itgmulc2nc  33478  itgabsnc  33479  ftc1cnnclem  33483  ftc1anclem3  33487  dvasin  33496  areacirclem1  33500  areacirclem4  33503  areacirc  33505  cntotbnd  33595  pellexlem1  37393  pellexlem2  37394  pellexlem6  37398  pell1234qrne0  37417  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell1234qrdich  37425  pell14qrdich  37433  pell1qrge1  37434  pell1qrgaplem  37437  rmspecsqrtnq  37470  qirropth  37473  rmxyneg  37485  rmxyadd  37486  rmxm1  37499  rmym1  37500  rmxluc  37501  rmyluc  37502  rmxdbl  37504  rmydbl  37505  jm2.18  37555  jm2.19lem1  37556  jm2.19lem2  37557  jm2.19lem4  37559  jm2.19  37560  jm2.22  37562  jm2.23  37563  jm2.25  37566  jm2.27c  37574  jm3.1lem2  37585  flcidc  37744  itgpowd  37800  areaquad  37802  inductionexd  38453  imo72b2lem0  38465  int-leftdistd  38482  radcnvrat  38513  expgrowth  38534  binomcxplemwb  38547  binomcxplemnn0  38548  binomcxplemfrat  38550  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  sineq0ALT  39173  mul13d  39491  fperiodmullem  39517  fperiodmul  39518  divcan8d  39527  dmmcand  39528  ltdiv23neg  39617  mulc1cncfg  39821  mccllem  39829  clim1fr1  39833  mullimc  39848  mullimcf  39855  sumnnodd  39862  reclimc  39885  sinmulcos  40076  coskpi2  40077  cosknegpi  40080  dvsinexp  40125  dvasinbx  40135  dvdivf  40137  dvdivbd  40138  dvdivcncf  40142  dvbdfbdioolem2  40144  dvxpaek  40155  dvnxpaek  40157  dvnmul  40158  dvmptfprodlem  40159  dvnprodlem2  40162  itgsinexplem1  40169  itgsinexp  40170  itgcoscmulx  40185  itgsincmulx  40190  itgiccshift  40196  itgperiod  40197  stoweidlem1  40218  stoweidlem11  40228  stoweidlem13  40230  stoweidlem14  40231  stoweidlem17  40234  stoweidlem25  40242  stoweidlem26  40243  stoweidlem42  40259  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  dirker2re  40309  dirkerdenne0  40310  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem26  40350  fourierdlem30  40354  fourierdlem39  40363  fourierdlem42  40366  fourierdlem47  40370  fourierdlem48  40371  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem65  40388  fourierdlem66  40389  fourierdlem68  40391  fourierdlem72  40395  fourierdlem73  40396  fourierdlem76  40399  fourierdlem80  40403  fourierdlem83  40406  fourierdlem85  40408  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem95  40418  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  elaa2lem  40450  etransclem8  40459  etransclem18  40469  etransclem20  40471  etransclem21  40472  etransclem23  40474  etransclem24  40475  etransclem31  40482  etransclem33  40484  etransclem35  40486  etransclem45  40496  etransclem46  40497  etransclem47  40498  etransclem48  40499  hoicvrrex  40770  hoidmvlelem2  40810  smfmullem1  40998  sigarim  41040  sigarac  41041  sigaraf  41042  sigarmf  41043  sigarls  41046  sigardiv  41050  sigarcol  41053  cevathlem1  41056  fmtnorec2lem  41454  fmtnorec3  41460  fmtnorec4  41461  fmtnoprmfac1  41477  fmtnoprmfac2  41479  fmtnofac2lem  41480  pwdif  41501  sfprmdvdsmersenne  41520  lighneallem3  41524  opeoALTV  41595  perfectALTVlem2  41631  0nodd  41810  2nodd  41812  2zlidl  41934  2zrngnmlid  41949  altgsumbcALT  42131  fldivmod  42313  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem2  42416  nn0mullong  42419  i2linesd  42525  aacllem  42547  amgmwlem  42548  amgmlemALT  42549