Theorem mulcld 11228

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

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
mulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulcl 11183	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  ℂcc 11097   · cmul 11104

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mul02lem1  11385  addrid  11389  cnegex  11390  kcnktkm1cn  11644  subaddmulsub  11676  mulsubaddmulsub  11677  receu  11858  divrec  11887  divcan3  11897  muldivdir  11906  subdivcomb1  11909  subdivcomb2  11910  divdivdiv  11915  divsubdiv  11930  lineq  12051  cru  12209  mul2lt0rlt0  13119  lincmb01cmp  13521  iccf1o  13522  flpmodeq  13906  moddiffl  13914  modvalp1  13922  modcyc  13938  modadd1  13940  modmuladdnn0  13950  modmul1  13959  modaddmulmod  13973  mulexpz  14137  expmulz  14143  binom3  14259  bernneq  14264  mulsubdivbinom2  14297  muldivbinom2  14298  remullem  15178  cjreim2  15211  absimle  15359  abstri  15381  sqreulem  15410  sqreu  15411  bhmafibid1cn  15516  bhmafibid2cn  15517  bhmafibid1  15518  bhmafibid2  15519  mulcn2  15646  reccn2  15647  o1rlimmul  15669  rlimmul  15695  isummulc2  15812  fsummulc2  15834  fsumparts  15857  indsum  15879  binomlem  15882  binom1dif  15886  incexclem  15889  incexc  15890  incexc2  15891  pwdif  15921  geomulcvg  15929  mertenslem1  15937  mertens  15939  fprodmul  16013  fprodn0f  16044  iprodmul  16056  binomfallfaclem1  16092  binomfallfaclem2  16093  binomrisefac  16095  bpolycl  16105  bpolysum  16106  bpolydiflem  16107  bpoly4  16112  efaddlem  16146  sinadd  16219  cosadd  16220  tanaddlem  16221  tanadd  16222  addsin  16225  sincossq  16231  sin2t  16232  dvds2ln  16346  oddm1even  16400  pwp1fsum  16448  flodddiv4  16472  sadadd2lem2  16507  bezoutlem2  16597  bezoutlem3  16598  bezoutlem4  16599  lcmgcdlem  16663  phiprmpw  16834  pythagtriplem12  16885  pythagtriplem14  16887  pythagtriplem16  16889  pcpremul  16902  pcaddlem  16947  fldivp1  16956  mul4sqlem  17012  4sqlem14  17017  vdwapun  17033  vdwlem2  17041  vdwlem6  17045  ablsimpgfindlem1  20178  zringlpirlem3  21582  znunit  21681  blcvx  24923  icopnfcnv  25069  cphipipcj  25327  cphipval2  25368  4cphipval2  25369  cphipval  25370  mbfmulc2re  25775  mbfmulc2  25790  itg1addlem4  25826  itg1addlem5  25827  itg1mulc  25831  mbfmul  25853  itgcl  25911  itgcnlem  25917  iblmulc2  25958  itgmulc2  25961  itgabs  25962  itgsplit  25963  dvmulbr  26066  dvcmul  26071  dvcmulf  26072  dvexp  26080  dvmptcmul  26091  dvmptdiv  26101  dvexp3  26105  dvsincos  26108  cmvth  26118  dvlipcn  26121  dvfsumabs  26150  dvfsumlem1  26153  ftc1lem4  26166  itgparts  26174  itgpowd  26177  plyf  26323  ply1termlem  26328  plyeq0lem  26335  plypf1  26337  plyaddlem1  26338  plymullem1  26339  coeeulem  26349  coeidlem  26362  coeid3  26365  plyco  26366  coemullem  26375  coemulhi  26379  coemulc  26380  dgrcolem2  26399  plycjlem  26401  plyrecj  26406  dvply1  26413  vieta1lem2  26440  vieta1  26441  elqaalem3  26450  aareccl  26455  aalioulem1  26461  taylfvallem1  26485  tayl0  26490  dvtaylp  26498  taylthlem2  26502  psergf  26540  radcnvlem1  26541  dvradcnv  26549  psercn2  26551  pserdvlem2  26556  pserdv2  26558  abelthlem4  26562  abelthlem5  26563  abelthlem6  26564  abelthlem7  26566  abelthlem9  26568  tanregt0  26669  efgh  26671  efabl  26680  efsubm  26681  cosargd  26738  abslogle  26748  tanarg  26749  advlogexp  26785  logtayllem  26789  logtayl  26790  cxpadd  26809  mulcxp  26815  cxpmul  26818  cxpmul2  26819  cxpmul2z  26821  abscxp  26822  abscxp2  26823  dvcxp2  26871  abscxpbnd  26883  root1eq1  26885  cxpeq  26887  angcan  26932  pythag  26947  ssscongptld  26952  affineequiv  26953  affineequiv2  26954  affineequiv3  26955  affineequiv4  26956  chordthmlem2  26963  chordthmlem3  26964  chordthmlem4  26965  chordthmlem5  26966  heron  26968  quad2  26969  quad  26970  dcubic1lem  26973  dcubic2  26974  dcubic1  26975  dcubic  26976  mcubic  26977  cubic2  26978  cubic  26979  binom4  26980  dquartlem1  26981  dquartlem2  26982  dquart  26983  quart1cl  26984  quart1lem  26985  quart1  26986  quartlem1  26987  quartlem2  26988  atantayl3  27069  leibpi  27072  birthdaylem2  27082  divsqrtsumo1  27113  cvxcl  27114  jensenlem2  27117  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamgulmlem4  27161  lgamgulmlem5  27162  lgamgulmlem6  27163  lgamgulm2  27165  lgamcvg2  27184  gamcvg  27185  gamcvg2lem  27188  wilthlem2  27198  ftalem1  27202  ftalem2  27203  ftalem4  27205  ftalem5  27206  basellem2  27211  basellem3  27212  basellem8  27217  muinv  27322  fsumdvdsmul  27324  logfacrlim  27353  logexprlim  27354  perfectlem2  27359  bposlem9  27421  gausslemma2dlem4  27498  lgsquad2lem1  27513  2lgslem3b  27526  2lgslem3c  27527  2lgslem3d  27528  2sqlem3  27549  2sqmod  27565  rplogsumlem1  27613  dchrisumlem2  27619  dchrisumlem3  27620  dchrmusum2  27623  dchrvmasumlem1  27624  dchrvmasum2lem  27625  dchrvmasum2if  27626  dchrvmasumlem3  27628  dchrvmasumiflem1  27630  dchrvmasumiflem2  27631  rpvmasum2  27641  dchrisum0lem1  27645  dchrisum0lem2a  27646  dchrisum0lem2  27647  dchrmusumlem  27651  dchrvmasumlem  27652  rplogsum  27656  mudivsum  27659  mulogsumlem  27660  mulogsum  27661  mulog2sumlem1  27663  mulog2sumlem2  27664  mulog2sumlem3  27665  vmalogdivsum  27668  logsqvma  27671  log2sumbnd  27673  selberglem1  27674  selberglem2  27675  selberglem3  27676  selberg  27677  selberg2lem  27679  selberg2  27680  selberg3lem1  27686  selberg3  27688  selberg4lem1  27689  selberg4  27690  pntrsumo1  27694  selbergr  27697  selberg3r  27698  selberg4r  27699  selberg34r  27700  pntsval2  27705  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntlemb  27726  pntlemf  27734  pntlemo  27736  ostth2lem2  27763  ostth2lem3  27764  ttgcontlem1  29174  brbtwn2  29195  colinearalg  29200  ax5seglem2  29219  ax5seglem9  29227  axeuclidlem  29252  axcontlem2  29255  axcontlem4  29257  axcontlem7  29260  axcontlem8  29261  finsumvtxdg2ssteplem4  29838  ex-ind-dvds  30752  nrt2irr  30764  ipval2  30999  dipcl  31004  riesz3i  32354  re0cj  33028  pythagreim  33030  quad3d  33034  indsumin  33121  dpfrac1  33151  wrdt2ind  33213  zringfrac  33788  ccfldsrarelvec  34005  ccfldextdgrr  34006  constrrtll  34065  constrrtlc1  34066  constrrtcclem  34068  constrrtcc  34069  constrconj  34079  constrfin  34080  constrelextdg2  34081  nn0constr  34095  constraddcl  34096  constrnegcl  34097  constrdircl  34099  iconstr  34100  constrremulcl  34101  constrrecl  34103  constrimcl  34104  constrmulcl  34105  constrreinvcl  34106  constrinvcl  34107  constrresqrtcl  34111  constrabscl  34112  constrsqrtcl  34113  cos9thpiminplylem1  34116  cos9thpiminplylem2  34117  cos9thpiminplylem3  34118  cos9thpiminply  34122  cos9thpinconstrlem1  34123  cos9thpinconstrlem2  34124  cos9thpinconstr  34125  cnre2csqima  34245  rmulccn  34262  dya2icoseg  34611  oddpwdc  34688  eulerpartlems  34694  eulerpartlemsv3  34695  eulerpartlemgs2  34714  signsplypnf  34881  itgexpif  34937  breprexplemc  34963  breprexp  34964  vtscl  34969  vtsprod  34970  circlemeth  34971  logdivsqrle  34981  hgt750lemf  34984  hgt750leme  34989  subfacval2  35577  subfaclim  35578  resconn  35636  iprodgam  36132  fwddifnp1  36555  knoppcnlem10  36979  knoppndvlem2  36990  knoppndvlem7  36995  knoppndvlem9  36997  knoppndvlem11  36999  knoppndvlem14  37002  knoppndvlem16  37004  knoppndvlem17  37005  bj-subcom  37839  bj-bary1lem  37841  bj-bary1lem1  37842  bj-bary1  37843  qdiff  37858  iblmulc2nc  38223  itgmulc2nc  38226  itgabsnc  38227  ftc1cnnclem  38229  ftc1anclem3  38233  dvasin  38242  areacirclem1  38246  areacirclem4  38249  areacirc  38251  cntotbnd  38334  3factsumint1  42677  3factsumint3  42679  3factsumint4  42680  lcmineqlem2  42686  lcmineqlem6  42690  lcmineqlem8  42692  lcmineqlem10  42694  lcmineqlem11  42695  lcmineqlem12  42696  lcmineqlem16  42700  lcmineqlem18  42702  lcmineqlem23  42707  3lexlogpow5ineq5  42716  aks4d1p1p1  42719  dvrelogpow2b  42724  aks4d1p1p6  42729  aks4d1p1p7  42730  aks4d1p1p5  42731  primrootscoprmpow  42755  posbezout  42756  primrootscoprbij  42758  primrootspoweq0  42762  2np3bcnp1  42800  2ap1caineq  42801  quadfac  42861  oddnumth  42961  nicomachus  42962  sumcubes  42963  ef11d  42989  cxp112d  42991  cxp111d  42992  readvrec2  43011  sn-addlid  43054  sn-it0e0  43066  sn-negex12  43067  sn-mul01  43076  sn-mullid  43086  sn-0tie0  43114  sn-mul02  43115  cnreeu  43153  fltnltalem  43285  fltnlta  43286  cu3addd  43303  3cubeslem2  43307  3cubeslem3l  43308  3cubeslem3r  43309  3cubeslem4  43311  pellexlem1  43447  pellexlem2  43448  pellexlem6  43452  pell1234qrne0  43471  pell1234qrreccl  43472  pell1234qrmulcl  43473  pell1234qrdich  43479  pell14qrdich  43487  pell1qrge1  43488  pell1qrgaplem  43491  rmspecsqrtnq  43524  qirropth  43526  rmxyneg  43538  rmxyadd  43539  rmxm1  43552  rmym1  43553  rmxluc  43554  rmyluc  43555  rmxdbl  43557  rmydbl  43558  jm2.18  43606  jm2.19lem1  43607  jm2.19lem2  43608  jm2.19lem4  43610  jm2.19  43611  jm2.22  43613  jm2.23  43614  jm2.25  43617  jm2.27c  43625  jm3.1lem2  43636  flcidc  43788  areaquad  43834  sqrtcval  44258  inductionexd  44772  imo72b2lem0  44782  int-leftdistd  44796  radcnvrat  44915  expgrowth  44936  binomcxplemwb  44949  binomcxplemnn0  44950  binomcxplemfrat  44952  binomcxplemdvbinom  44954  binomcxplemnotnn0  44957  sineq0ALT  45536  mul13d  45890  fperiodmullem  45913  fperiodmul  45914  divcan8d  45922  dmmcand  45923  ltdiv23neg  46000  mulc1cncfg  46196  mccllem  46204  clim1fr1  46208  mullimc  46223  mullimcf  46230  sumnnodd  46237  reclimc  46258  sinmulcos  46470  coskpi2  46471  cosknegpi  46474  dvsinexp  46516  dvasinbx  46525  dvdivf  46527  dvdivbd  46528  dvdivcncf  46532  dvbdfbdioolem2  46534  dvxpaek  46545  dvnxpaek  46547  dvnmul  46548  dvmptfprodlem  46549  dvnprodlem2  46552  itgsinexplem1  46559  itgsinexp  46560  itgcoscmulx  46574  itgsincmulx  46579  itgiccshift  46585  itgperiod  46586  stoweidlem1  46606  stoweidlem11  46616  stoweidlem13  46618  stoweidlem14  46619  stoweidlem17  46622  stoweidlem25  46630  stoweidlem26  46631  stoweidlem42  46647  wallispilem4  46673  wallispilem5  46674  wallispi  46675  wallispi2lem1  46676  wallispi2lem2  46677  wallispi2  46678  stirlinglem1  46679  stirlinglem3  46681  stirlinglem4  46682  stirlinglem5  46683  stirlinglem6  46684  stirlinglem7  46685  stirlinglem8  46686  stirlinglem10  46688  stirlinglem11  46689  stirlinglem12  46690  stirlinglem13  46691  stirlinglem14  46692  stirlinglem15  46693  dirker2re  46697  dirkerdenne0  46698  dirkerper  46701  dirkertrigeqlem1  46703  dirkertrigeqlem2  46704  dirkertrigeqlem3  46705  dirkertrigeq  46706  dirkeritg  46707  dirkercncflem2  46709  dirkercncflem4  46711  fourierdlem26  46738  fourierdlem30  46742  fourierdlem39  46751  fourierdlem42  46754  fourierdlem47  46758  fourierdlem48  46759  fourierdlem56  46767  fourierdlem57  46768  fourierdlem58  46769  fourierdlem62  46773  fourierdlem65  46776  fourierdlem66  46777  fourierdlem68  46779  fourierdlem72  46783  fourierdlem73  46784  fourierdlem76  46787  fourierdlem80  46791  fourierdlem83  46794  fourierdlem85  46796  fourierdlem89  46800  fourierdlem90  46801  fourierdlem91  46802  fourierdlem95  46806  fourierdlem97  46808  fourierdlem101  46812  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  sqwvfoura  46833  sqwvfourb  46834  fourierswlem  46835  fouriersw  46836  elaa2lem  46838  etransclem8  46847  etransclem18  46857  etransclem20  46859  etransclem21  46860  etransclem23  46862  etransclem24  46863  etransclem31  46870  etransclem33  46872  etransclem35  46874  etransclem45  46884  etransclem46  46885  etransclem47  46886  etransclem48  46887  hoicvrrex  47161  hoidmvlelem2  47201  smfmullem1  47396  sigarim  47456  sigarac  47457  sigaraf  47458  sigarmf  47459  sigarls  47462  sigardiv  47466  sigarcol  47469  cevathlem1  47472  sin3t  47496  cos3t  47497  sin5tlem1  47498  sin5tlem2  47499  sin5tlem3  47500  sin5tlem4  47501  sin5tlem5  47502  sin5t  47503  cos5t  47504  fldivmod  47969  fmtnorec2lem  48182  fmtnorec3  48188  fmtnorec4  48189  fmtnoprmfac1  48205  fmtnoprmfac2  48207  fmtnofac2lem  48208  sfprmdvdsmersenne  48243  lighneallem3  48247  quad1  48273  requad01  48274  requad2  48276  opeoALTV  48337  perfectALTVlem2  48375  fppr2odd  48384  0nodd  48823  2nodd  48825  2zlidl  48893  2zrngnmlid  48908  altgsumbcALT  49017  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  nn0sumshdiglem2  49286  nn0mullong  49289  itcovalt2lem2lem2  49338  ackval2  49346  submuladdmuld  49365  affinecomb2  49367  affineid  49368  1subrec1sub  49369  eenglngeehlnmlem1  49401  eenglngeehlnmlem2  49402  rrx2linest  49406  line2x  49418  line2y  49419  itschlc0yqe  49424  itsclc0yqsollem1  49426  itsclc0yqsol  49428  itscnhlc0xyqsol  49429  itschlc0xyqsol1  49430  itschlc0xyqsol  49431  itsclc0xyqsolr  49433  2itscplem1  49442  2itscplem2  49443  2itscplem3  49444  2itscp  49445  itscnhlinecirc02plem1  49446  itscnhlinecirc02plem2  49447  inlinecirc02plem  49450  inlinecirc02p  49451  i2linesd  50441  aacllem  50474  amgmwlem  50475  amgmlemALT  50476