Theorem mulcld 11329

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 11284	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 11262

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul02lem1  11486  addrid  11490  cnegex  11491  kcnktkm1cn  11747  subaddmulsub  11779  mulsubaddmulsub  11780  receu  11961  divrec  11990  divcan3  12000  muldivdir  12009  subdivcomb1  12012  subdivcomb2  12013  divdivdiv  12018  divsubdiv  12033  lineq  12154  cru  12312  mul2lt0rlt0  13224  lincmb01cmp  13626  iccf1o  13627  flpmodeq  14014  moddiffl  14022  modvalp1  14030  modcyc  14046  modadd1  14048  modmuladdnn0  14058  modmul1  14067  modaddmulmod  14081  mulexpz  14245  expmulz  14251  binom3  14368  bernneq  14373  mulsubdivbinom2  14406  muldivbinom2  14407  remullem  15295  cjreim2  15328  absimle  15476  abstri  15498  sqreulem  15527  sqreu  15528  bhmafibid1cn  15633  bhmafibid2cn  15634  bhmafibid1  15635  bhmafibid2  15636  mulcn2  15763  reccn2  15764  o1rlimmul  15786  rlimmul  15812  isummulc2  15928  fsummulc2  15950  fsumparts  15973  indsum  15995  binomlem  15998  binom1dif  16002  incexclem  16005  incexc  16006  incexc2  16007  pwdif  16037  geomulcvg  16045  mertenslem1  16053  mertens  16055  fprodmul  16127  fprodn0f  16158  iprodmul  16170  binomfallfaclem1  16205  binomfallfaclem2  16206  binomrisefac  16208  bpolycl  16218  bpolysum  16219  bpolydiflem  16220  bpoly4  16225  efaddlem  16259  sinadd  16332  cosadd  16333  tanaddlem  16334  tanadd  16335  addsin  16338  sincossq  16344  sin2t  16345  dvds2ln  16459  oddm1even  16513  pwp1fsum  16561  flodddiv4  16585  sadadd2lem2  16620  bezoutlem2  16713  bezoutlem3  16714  bezoutlem4  16715  lcmgcdlem  16781  phiprmpw  16953  pythagtriplem12  17004  pythagtriplem14  17006  pythagtriplem16  17008  pcpremul  17021  pcaddlem  17066  fldivp1  17075  mul4sqlem  17131  4sqlem14  17136  vdwapun  17152  vdwlem2  17160  vdwlem6  17164  ablsimpgfindlem1  20323  zringlpirlem3  21770  znunit  21869  blcvx  25117  icopnfcnv  25263  cphipipcj  25521  cphipval2  25562  4cphipval2  25563  cphipval  25564  mbfmulc2re  25969  mbfmulc2  25984  itg1addlem4  26020  itg1addlem5  26021  itg1mulc  26025  mbfmul  26047  itgcl  26104  itgcnlem  26110  iblmulc2  26151  itgmulc2  26154  itgabs  26155  itgsplit  26156  dvmulbr  26259  dvcmul  26264  dvcmulf  26265  dvexp  26273  dvmptcmul  26284  dvmptdiv  26294  dvexp3  26298  dvsincos  26301  cmvth  26311  dvlipcn  26314  dvfsumabs  26343  dvfsumlem1  26346  ftc1lem4  26359  itgparts  26367  itgpowd  26370  plyf  26516  ply1termlem  26521  plyeq0lem  26529  plypf1  26531  plyaddlem1  26532  plymullem1  26533  coeeulem  26543  coeidlem  26556  coeid3  26559  plyco  26560  coemullem  26569  coemulhi  26573  coemulc  26574  dgrcolem2  26593  plycjlem  26595  plyrecj  26598  dvply1  26605  vieta1lem2  26634  vieta1  26635  elqaalem3  26644  aareccl  26653  aalioulem1  26659  taylfvallem1  26684  tayl0  26689  dvtaylp  26697  taylthlem2  26701  psergf  26739  radcnvlem1  26740  dvradcnv  26748  psercn2  26750  pserdvlem2  26755  pserdv2  26757  abelthlem4  26761  abelthlem5  26762  abelthlem6  26763  abelthlem7  26765  abelthlem9  26767  tanregt0  26867  efgh  26869  efabl  26878  efsubm  26879  cosargd  26936  abslogle  26946  tanarg  26947  advlogexp  26983  logtayllem  26987  logtayl  26988  cxpadd  27007  mulcxp  27013  cxpmul  27016  cxpmul2  27017  cxpmul2z  27019  abscxp  27020  abscxp2  27021  dvcxp2  27069  abscxpbnd  27081  root1eq1  27083  cxpeq  27085  angcan  27130  pythag  27145  ssscongptld  27150  affineequiv  27151  affineequiv2  27152  affineequiv3  27153  affineequiv4  27154  chordthmlem2  27161  chordthmlem3  27162  chordthmlem4  27163  chordthmlem5  27164  heron  27166  quad2  27167  quad  27168  dcubic1lem  27171  dcubic2  27172  dcubic1  27173  dcubic  27174  mcubic  27175  cubic2  27176  cubic  27177  binom4  27178  dquartlem1  27179  dquartlem2  27180  dquart  27181  quart1cl  27182  quart1lem  27183  quart1  27184  quartlem1  27185  quartlem2  27186  atantayl3  27267  leibpi  27270  birthdaylem2  27280  divsqrtsumo1  27311  cvxcl  27312  jensenlem2  27315  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem4  27359  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamgulm2  27363  lgamcvg2  27382  gamcvg  27383  gamcvg2lem  27386  wilthlem2  27396  ftalem1  27400  ftalem2  27401  ftalem4  27403  ftalem5  27404  basellem2  27409  basellem3  27410  basellem8  27415  muinv  27520  fsumdvdsmul  27522  logfacrlim  27551  logexprlim  27552  perfectlem2  27557  bposlem9  27619  gausslemma2dlem4  27696  lgsquad2lem1  27711  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  2sqlem3  27747  2sqmod  27763  rplogsumlem1  27811  dchrisumlem2  27817  dchrisumlem3  27818  dchrmusum2  27821  dchrvmasumlem1  27822  dchrvmasum2lem  27823  dchrvmasum2if  27824  dchrvmasumlem3  27826  dchrvmasumiflem1  27828  dchrvmasumiflem2  27829  rpvmasum2  27839  dchrisum0lem1  27843  dchrisum0lem2a  27844  dchrisum0lem2  27845  dchrmusumlem  27849  dchrvmasumlem  27850  rplogsum  27854  mudivsum  27857  mulogsumlem  27858  mulogsum  27859  mulog2sumlem1  27861  mulog2sumlem2  27862  mulog2sumlem3  27863  vmalogdivsum  27866  logsqvma  27869  log2sumbnd  27871  selberglem1  27872  selberglem2  27873  selberglem3  27874  selberg  27875  selberg2lem  27877  selberg2  27878  selberg3lem1  27884  selberg3  27886  selberg4lem1  27887  selberg4  27888  pntrsumo1  27892  selbergr  27895  selberg3r  27896  selberg4r  27897  selberg34r  27898  pntsval2  27903  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntrlog2bnd  27911  pntlemb  27924  pntlemf  27932  pntlemo  27934  ostth2lem2  27961  ostth2lem3  27962  ttgcontlem1  29462  brbtwn2  29483  colinearalg  29488  ax5seglem2  29507  ax5seglem9  29515  axeuclidlem  29540  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  axcontlem8  29549  finsumvtxdg2ssteplem4  30129  ex-ind-dvds  31062  nrt2irr  31074  ipval2  31309  dipcl  31314  riesz3i  32664  re0cj  33335  pythagreim  33337  quad3d  33341  indsumin  33428  dpfrac1  33458  wrdt2ind  33516  zringfrac  34086  ccfldsrarelvec  34303  ccfldextdgrr  34304  constrrtll  34363  constrrtlc1  34364  constrrtcclem  34366  constrrtcc  34367  constrconj  34377  constrfin  34378  constrelextdg2  34379  nn0constr  34393  constraddcl  34394  constrnegcl  34395  constrdircl  34397  iconstr  34398  constrremulcl  34399  constrrecl  34401  constrimcl  34402  constrmulcl  34403  constrreinvcl  34404  constrinvcl  34405  constrresqrtcl  34409  constrabscl  34410  constrsqrtcl  34411  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  cos9thpiminplylem3  34416  cos9thpiminply  34420  cos9thpinconstrlem1  34421  cos9thpinconstrlem2  34422  cos9thpinconstr  34423  cnre2csqima  34543  rmulccn  34560  dya2icoseg  34909  oddpwdc  34986  eulerpartlems  34992  eulerpartlemsv3  34993  eulerpartlemgs2  35012  signsplypnf  35179  itgexpif  35235  breprexplemc  35261  breprexp  35262  vtscl  35267  vtsprod  35268  circlemeth  35269  logdivsqrle  35279  hgt750lemf  35282  hgt750leme  35287  subfacval2  35952  subfaclim  35953  resconn  36011  iprodgam  36507  fwddifnp1  36930  knoppcnlem10  37368  knoppndvlem2  37379  knoppndvlem7  37384  knoppndvlem9  37386  knoppndvlem11  37388  knoppndvlem14  37391  knoppndvlem16  37393  knoppndvlem17  37394  bj-subcom  38229  bj-bary1lem  38231  bj-bary1lem1  38232  bj-bary1  38233  qdiff  38248  iblmulc2nc  38603  itgmulc2nc  38606  itgabsnc  38607  ftc1cnnclem  38609  ftc1anclem3  38613  dvasin  38622  areacirclem1  38626  areacirclem4  38629  areacirc  38631  cntotbnd  38730  3factsumint1  43071  3factsumint3  43073  3factsumint4  43074  lcmineqlem2  43080  lcmineqlem6  43084  lcmineqlem8  43086  lcmineqlem10  43088  lcmineqlem11  43089  lcmineqlem12  43090  lcmineqlem16  43094  lcmineqlem18  43096  lcmineqlem23  43101  3lexlogpow5ineq5  43110  aks4d1p1p1  43113  dvrelogpow2b  43118  aks4d1p1p6  43123  aks4d1p1p7  43124  aks4d1p1p5  43125  primrootscoprmpow  43149  posbezout  43150  primrootscoprbij  43152  primrootspoweq0  43156  2np3bcnp1  43194  2ap1caineq  43195  quadfac  43255  oddnumth  43368  nicomachus  43369  sumcubes  43370  ef11d  43390  cxp112d  43392  cxp111d  43393  readvrec2  43412  sn-addlid  43455  sn-it0e0  43467  sn-negex12  43468  sn-mul01  43477  sn-mullid  43487  sn-0tie0  43515  sn-mul02  43516  cnreeu  43554  fltnltalem  43673  fltnlta  43674  cu3addd  43691  3cubeslem2  43695  3cubeslem3l  43696  3cubeslem3r  43697  3cubeslem4  43699  pellexlem1  43835  pellexlem2  43836  pellexlem6  43840  pell1234qrne0  43859  pell1234qrreccl  43860  pell1234qrmulcl  43861  pell1234qrdich  43867  pell14qrdich  43875  pell1qrge1  43876  pell1qrgaplem  43879  rmspecsqrtnq  43912  qirropth  43914  rmxyneg  43926  rmxyadd  43927  rmxm1  43940  rmym1  43941  rmxluc  43942  rmyluc  43943  rmxdbl  43945  rmydbl  43946  jm2.18  43994  jm2.19lem1  43995  jm2.19lem2  43996  jm2.19lem4  43998  jm2.19  43999  jm2.22  44001  jm2.23  44002  jm2.25  44005  jm2.27c  44013  jm3.1lem2  44024  flcidc  44171  areaquad  44217  sqrtcval  44640  inductionexd  45154  imo72b2lem0  45164  int-leftdistd  45178  radcnvrat  45297  expgrowth  45318  binomcxplemwb  45331  binomcxplemnn0  45332  binomcxplemfrat  45334  binomcxplemdvbinom  45336  binomcxplemnotnn0  45339  sineq0ALT  45918  mul13d  46295  fperiodmullem  46318  fperiodmul  46319  divcan8d  46327  dmmcand  46328  ltdiv23neg  46404  mulc1cncfg  46600  mccllem  46608  clim1fr1  46612  mullimc  46627  mullimcf  46634  sumnnodd  46641  reclimc  46662  sinmulcos  46874  coskpi2  46875  cosknegpi  46878  dvsinexp  46920  dvasinbx  46929  dvdivf  46931  dvdivbd  46932  dvdivcncf  46936  dvbdfbdioolem2  46938  dvxpaek  46949  dvnxpaek  46951  dvnmul  46952  dvmptfprodlem  46953  dvnprodlem2  46956  itgsinexplem1  46963  itgsinexp  46964  itgcoscmulx  46978  itgsincmulx  46983  itgiccshift  46989  itgperiod  46990  stoweidlem1  47010  stoweidlem11  47020  stoweidlem13  47022  stoweidlem14  47023  stoweidlem17  47026  stoweidlem25  47034  stoweidlem26  47035  stoweidlem42  47051  wallispilem4  47077  wallispilem5  47078  wallispi  47079  wallispi2lem1  47080  wallispi2lem2  47081  wallispi2  47082  stirlinglem1  47083  stirlinglem3  47085  stirlinglem4  47086  stirlinglem5  47087  stirlinglem6  47088  stirlinglem7  47089  stirlinglem8  47090  stirlinglem10  47092  stirlinglem11  47093  stirlinglem12  47094  stirlinglem13  47095  stirlinglem14  47096  stirlinglem15  47097  dirker2re  47101  dirkerdenne0  47102  dirkerper  47105  dirkertrigeqlem1  47107  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  dirkertrigeq  47110  dirkeritg  47111  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem26  47142  fourierdlem30  47146  fourierdlem39  47155  fourierdlem42  47158  fourierdlem47  47162  fourierdlem48  47163  fourierdlem56  47171  fourierdlem57  47172  fourierdlem58  47173  fourierdlem62  47177  fourierdlem65  47180  fourierdlem66  47181  fourierdlem68  47183  fourierdlem72  47187  fourierdlem73  47188  fourierdlem76  47191  fourierdlem80  47195  fourierdlem83  47198  fourierdlem85  47200  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem95  47210  fourierdlem97  47212  fourierdlem101  47216  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  sqwvfoura  47237  sqwvfourb  47238  fourierswlem  47239  fouriersw  47240  elaa2lem  47242  etransclem8  47251  etransclem18  47261  etransclem20  47263  etransclem21  47264  etransclem23  47266  etransclem24  47267  etransclem31  47274  etransclem33  47276  etransclem35  47278  etransclem45  47288  etransclem46  47289  etransclem47  47290  etransclem48  47291  hoicvrrex  47565  hoidmvlelem2  47605  smfmullem1  47800  sigarim  47860  sigarac  47861  sigaraf  47862  sigarmf  47863  sigarls  47866  sigardiv  47870  sigarcol  47873  cevathlem1  47876  sin3t  47916  cos3t  47917  sin5tlem1  47918  sin5tlem2  47919  sin5tlem3  47920  sin5tlem4  47921  sin5tlem5  47922  sin5t  47923  cos5t  47924  fldivmod  48413  fmtnorec2lem  48626  fmtnorec3  48632  fmtnorec4  48633  fmtnoprmfac1  48649  fmtnoprmfac2  48651  fmtnofac2lem  48652  sfprmdvdsmersenne  48687  lighneallem3  48691  quad1  48717  requad01  48718  requad2  48720  opeoALTV  48781  perfectALTVlem2  48819  fppr2odd  48828  0nodd  49266  2nodd  49268  2zlidl  49336  2zrngnmlid  49351  altgsumbcALT  49464  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdiglem2  49733  nn0mullong  49736  itcovalt2lem2lem2  49785  ackval2  49793  submuladdmuld  49812  affinecomb2  49814  affineid  49815  1subrec1sub  49816  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  rrx2linest  49853  line2x  49865  line2y  49866  itschlc0yqe  49871  itsclc0yqsollem1  49873  itsclc0yqsol  49875  itscnhlc0xyqsol  49876  itschlc0xyqsol1  49877  itschlc0xyqsol  49878  itsclc0xyqsolr  49880  2itscplem1  49889  2itscplem2  49890  2itscplem3  49891  2itscp  49892  itscnhlinecirc02plem1  49893  itscnhlinecirc02plem2  49894  inlinecirc02plem  49897  inlinecirc02p  49898  dvsec  50855  i2linesd  50874  aacllem  50938  crossp3d  50966  amgmwlem  50986  amgmlemALT  50987