Theorem mulcld 11254

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414  ℂcc 11123   · cmul 11130

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

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

This theorem is used by:  mul02lem1  11411  addrid  11415  cnegex  11416  kcnktkm1cn  11670  subaddmulsub  11702  mulsubaddmulsub  11703  receu  11884  divrec  11913  divcan3  11923  muldivdir  11932  subdivcomb1  11935  subdivcomb2  11936  divdivdiv  11941  divsubdiv  11956  lineq  12077  cru  12235  mul2lt0rlt0  13147  lincmb01cmp  13549  iccf1o  13550  flpmodeq  13936  moddiffl  13944  modvalp1  13952  modcyc  13968  modadd1  13970  modmuladdnn0  13980  modmul1  13989  modaddmulmod  14003  mulexpz  14167  expmulz  14173  binom3  14289  bernneq  14294  mulsubdivbinom2  14327  muldivbinom2  14328  remullem  15216  cjreim2  15249  absimle  15397  abstri  15419  sqreulem  15448  sqreu  15449  bhmafibid1cn  15554  bhmafibid2cn  15555  bhmafibid1  15556  bhmafibid2  15557  mulcn2  15684  reccn2  15685  o1rlimmul  15707  rlimmul  15733  isummulc2  15849  fsummulc2  15871  fsumparts  15894  indsum  15916  binomlem  15919  binom1dif  15923  incexclem  15926  incexc  15927  incexc2  15928  pwdif  15958  geomulcvg  15966  mertenslem1  15974  mertens  15976  fprodmul  16048  fprodn0f  16079  iprodmul  16091  binomfallfaclem1  16126  binomfallfaclem2  16127  binomrisefac  16129  bpolycl  16139  bpolysum  16140  bpolydiflem  16141  bpoly4  16146  efaddlem  16180  sinadd  16253  cosadd  16254  tanaddlem  16255  tanadd  16256  addsin  16259  sincossq  16265  sin2t  16266  dvds2ln  16380  oddm1even  16434  pwp1fsum  16482  flodddiv4  16506  sadadd2lem2  16541  bezoutlem2  16631  bezoutlem3  16632  bezoutlem4  16633  lcmgcdlem  16697  phiprmpw  16868  pythagtriplem12  16919  pythagtriplem14  16921  pythagtriplem16  16923  pcpremul  16936  pcaddlem  16981  fldivp1  16990  mul4sqlem  17046  4sqlem14  17051  vdwapun  17067  vdwlem2  17075  vdwlem6  17079  ablsimpgfindlem1  20237  zringlpirlem3  21678  znunit  21777  blcvx  25025  icopnfcnv  25171  cphipipcj  25429  cphipval2  25470  4cphipval2  25471  cphipval  25472  mbfmulc2re  25877  mbfmulc2  25892  itg1addlem4  25928  itg1addlem5  25929  itg1mulc  25933  mbfmul  25955  itgcl  26012  itgcnlem  26018  iblmulc2  26059  itgmulc2  26062  itgabs  26063  itgsplit  26064  dvmulbr  26167  dvcmul  26172  dvcmulf  26173  dvexp  26181  dvmptcmul  26192  dvmptdiv  26202  dvexp3  26206  dvsincos  26209  cmvth  26219  dvlipcn  26222  dvfsumabs  26251  dvfsumlem1  26254  ftc1lem4  26267  itgparts  26275  itgpowd  26278  plyf  26424  ply1termlem  26429  plyeq0lem  26437  plypf1  26439  plyaddlem1  26440  plymullem1  26441  coeeulem  26451  coeidlem  26464  coeid3  26467  plyco  26468  coemullem  26477  coemulhi  26481  coemulc  26482  dgrcolem2  26501  plycjlem  26503  plyrecj  26508  dvply1  26515  vieta1lem2  26544  vieta1  26545  elqaalem3  26554  aareccl  26563  aalioulem1  26569  taylfvallem1  26594  tayl0  26599  dvtaylp  26607  taylthlem2  26611  psergf  26649  radcnvlem1  26650  dvradcnv  26658  psercn2  26660  pserdvlem2  26665  pserdv2  26667  abelthlem4  26671  abelthlem5  26672  abelthlem6  26673  abelthlem7  26675  abelthlem9  26677  tanregt0  26777  efgh  26779  efabl  26788  efsubm  26789  cosargd  26846  abslogle  26856  tanarg  26857  advlogexp  26893  logtayllem  26897  logtayl  26898  cxpadd  26917  mulcxp  26923  cxpmul  26926  cxpmul2  26927  cxpmul2z  26929  abscxp  26930  abscxp2  26931  dvcxp2  26979  abscxpbnd  26991  root1eq1  26993  cxpeq  26995  angcan  27040  pythag  27055  ssscongptld  27060  affineequiv  27061  affineequiv2  27062  affineequiv3  27063  affineequiv4  27064  chordthmlem2  27071  chordthmlem3  27072  chordthmlem4  27073  chordthmlem5  27074  heron  27076  quad2  27077  quad  27078  dcubic1lem  27081  dcubic2  27082  dcubic1  27083  dcubic  27084  mcubic  27085  cubic2  27086  cubic  27087  binom4  27088  dquartlem1  27089  dquartlem2  27090  dquart  27091  quart1cl  27092  quart1lem  27093  quart1  27094  quartlem1  27095  quartlem2  27096  atantayl3  27177  leibpi  27180  birthdaylem2  27190  divsqrtsumo1  27221  cvxcl  27222  jensenlem2  27225  lgamgulmlem2  27267  lgamgulmlem3  27268  lgamgulmlem4  27269  lgamgulmlem5  27270  lgamgulmlem6  27271  lgamgulm2  27273  lgamcvg2  27292  gamcvg  27293  gamcvg2lem  27296  wilthlem2  27306  ftalem1  27310  ftalem2  27311  ftalem4  27313  ftalem5  27314  basellem2  27319  basellem3  27320  basellem8  27325  muinv  27430  fsumdvdsmul  27432  logfacrlim  27461  logexprlim  27462  perfectlem2  27467  bposlem9  27529  gausslemma2dlem4  27606  lgsquad2lem1  27621  2lgslem3b  27634  2lgslem3c  27635  2lgslem3d  27636  2sqlem3  27657  2sqmod  27673  rplogsumlem1  27721  dchrisumlem2  27727  dchrisumlem3  27728  dchrmusum2  27731  dchrvmasumlem1  27732  dchrvmasum2lem  27733  dchrvmasum2if  27734  dchrvmasumlem3  27736  dchrvmasumiflem1  27738  dchrvmasumiflem2  27739  rpvmasum2  27749  dchrisum0lem1  27753  dchrisum0lem2a  27754  dchrisum0lem2  27755  dchrmusumlem  27759  dchrvmasumlem  27760  rplogsum  27764  mudivsum  27767  mulogsumlem  27768  mulogsum  27769  mulog2sumlem1  27771  mulog2sumlem2  27772  mulog2sumlem3  27773  vmalogdivsum  27776  logsqvma  27779  log2sumbnd  27781  selberglem1  27782  selberglem2  27783  selberglem3  27784  selberg  27785  selberg2lem  27787  selberg2  27788  selberg3lem1  27794  selberg3  27796  selberg4lem1  27797  selberg4  27798  pntrsumo1  27802  selbergr  27805  selberg3r  27806  selberg4r  27807  selberg34r  27808  pntsval2  27813  pntrlog2bndlem1  27814  pntrlog2bndlem2  27815  pntrlog2bndlem3  27816  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntrlog2bndlem6  27820  pntrlog2bnd  27821  pntlemb  27834  pntlemf  27842  pntlemo  27844  ostth2lem2  27871  ostth2lem3  27872  ttgcontlem1  29342  brbtwn2  29363  colinearalg  29368  ax5seglem2  29387  ax5seglem9  29395  axeuclidlem  29420  axcontlem2  29423  axcontlem4  29425  axcontlem7  29428  axcontlem8  29429  finsumvtxdg2ssteplem4  30009  ex-ind-dvds  30942  nrt2irr  30954  ipval2  31189  dipcl  31194  riesz3i  32544  re0cj  33215  pythagreim  33217  quad3d  33221  indsumin  33308  dpfrac1  33338  wrdt2ind  33396  zringfrac  33965  ccfldsrarelvec  34182  ccfldextdgrr  34183  constrrtll  34242  constrrtlc1  34243  constrrtcclem  34245  constrrtcc  34246  constrconj  34256  constrfin  34257  constrelextdg2  34258  nn0constr  34272  constraddcl  34273  constrnegcl  34274  constrdircl  34276  iconstr  34277  constrremulcl  34278  constrrecl  34280  constrimcl  34281  constrmulcl  34282  constrreinvcl  34283  constrinvcl  34284  constrresqrtcl  34288  constrabscl  34289  constrsqrtcl  34290  cos9thpiminplylem1  34293  cos9thpiminplylem2  34294  cos9thpiminplylem3  34295  cos9thpiminply  34299  cos9thpinconstrlem1  34300  cos9thpinconstrlem2  34301  cos9thpinconstr  34302  cnre2csqima  34422  rmulccn  34439  dya2icoseg  34789  oddpwdc  34866  eulerpartlems  34872  eulerpartlemsv3  34873  eulerpartlemgs2  34892  signsplypnf  35059  itgexpif  35115  breprexplemc  35141  breprexp  35142  vtscl  35147  vtsprod  35148  circlemeth  35149  logdivsqrle  35159  hgt750lemf  35162  hgt750leme  35167  subfacval2  35767  subfaclim  35768  resconn  35826  iprodgam  36322  fwddifnp1  36746  knoppcnlem10  37200  knoppndvlem2  37211  knoppndvlem7  37216  knoppndvlem9  37218  knoppndvlem11  37220  knoppndvlem14  37223  knoppndvlem16  37225  knoppndvlem17  37226  bj-subcom  38061  bj-bary1lem  38063  bj-bary1lem1  38064  bj-bary1  38065  qdiff  38080  iblmulc2nc  38435  itgmulc2nc  38438  itgabsnc  38439  ftc1cnnclem  38441  ftc1anclem3  38445  dvasin  38454  areacirclem1  38458  areacirclem4  38461  areacirc  38463  cntotbnd  38547  3factsumint1  42888  3factsumint3  42890  3factsumint4  42891  lcmineqlem2  42897  lcmineqlem6  42901  lcmineqlem8  42903  lcmineqlem10  42905  lcmineqlem11  42906  lcmineqlem12  42907  lcmineqlem16  42911  lcmineqlem18  42913  lcmineqlem23  42918  3lexlogpow5ineq5  42927  aks4d1p1p1  42930  dvrelogpow2b  42935  aks4d1p1p6  42940  aks4d1p1p7  42941  aks4d1p1p5  42942  primrootscoprmpow  42966  posbezout  42967  primrootscoprbij  42969  primrootspoweq0  42973  2np3bcnp1  43011  2ap1caineq  43012  quadfac  43072  oddnumth  43187  nicomachus  43188  sumcubes  43189  ef11d  43215  cxp112d  43217  cxp111d  43218  readvrec2  43237  sn-addlid  43280  sn-it0e0  43292  sn-negex12  43293  sn-mul01  43302  sn-mullid  43312  sn-0tie0  43340  sn-mul02  43341  cnreeu  43379  fltnltalem  43509  fltnlta  43510  cu3addd  43527  3cubeslem2  43531  3cubeslem3l  43532  3cubeslem3r  43533  3cubeslem4  43535  pellexlem1  43671  pellexlem2  43672  pellexlem6  43676  pell1234qrne0  43695  pell1234qrreccl  43696  pell1234qrmulcl  43697  pell1234qrdich  43703  pell14qrdich  43711  pell1qrge1  43712  pell1qrgaplem  43715  rmspecsqrtnq  43748  qirropth  43750  rmxyneg  43762  rmxyadd  43763  rmxm1  43776  rmym1  43777  rmxluc  43778  rmyluc  43779  rmxdbl  43781  rmydbl  43782  jm2.18  43830  jm2.19lem1  43831  jm2.19lem2  43832  jm2.19lem4  43834  jm2.19  43835  jm2.22  43837  jm2.23  43838  jm2.25  43841  jm2.27c  43849  jm3.1lem2  43860  flcidc  44012  areaquad  44058  sqrtcval  44482  inductionexd  44996  imo72b2lem0  45006  int-leftdistd  45020  radcnvrat  45139  expgrowth  45160  binomcxplemwb  45173  binomcxplemnn0  45174  binomcxplemfrat  45176  binomcxplemdvbinom  45178  binomcxplemnotnn0  45181  sineq0ALT  45760  mul13d  46114  fperiodmullem  46137  fperiodmul  46138  divcan8d  46146  dmmcand  46147  ltdiv23neg  46224  mulc1cncfg  46420  mccllem  46428  clim1fr1  46432  mullimc  46447  mullimcf  46454  sumnnodd  46461  reclimc  46482  sinmulcos  46694  coskpi2  46695  cosknegpi  46698  dvsinexp  46740  dvasinbx  46749  dvdivf  46751  dvdivbd  46752  dvdivcncf  46756  dvbdfbdioolem2  46758  dvxpaek  46769  dvnxpaek  46771  dvnmul  46772  dvmptfprodlem  46773  dvnprodlem2  46776  itgsinexplem1  46783  itgsinexp  46784  itgcoscmulx  46798  itgsincmulx  46803  itgiccshift  46809  itgperiod  46810  stoweidlem1  46830  stoweidlem11  46840  stoweidlem13  46842  stoweidlem14  46843  stoweidlem17  46846  stoweidlem25  46854  stoweidlem26  46855  stoweidlem42  46871  wallispilem4  46897  wallispilem5  46898  wallispi  46899  wallispi2lem1  46900  wallispi2lem2  46901  wallispi2  46902  stirlinglem1  46903  stirlinglem3  46905  stirlinglem4  46906  stirlinglem5  46907  stirlinglem6  46908  stirlinglem7  46909  stirlinglem8  46910  stirlinglem10  46912  stirlinglem11  46913  stirlinglem12  46914  stirlinglem13  46915  stirlinglem14  46916  stirlinglem15  46917  dirker2re  46921  dirkerdenne0  46922  dirkerper  46925  dirkertrigeqlem1  46927  dirkertrigeqlem2  46928  dirkertrigeqlem3  46929  dirkertrigeq  46930  dirkeritg  46931  dirkercncflem2  46933  dirkercncflem4  46935  fourierdlem26  46962  fourierdlem30  46966  fourierdlem39  46975  fourierdlem42  46978  fourierdlem47  46982  fourierdlem48  46983  fourierdlem56  46991  fourierdlem57  46992  fourierdlem58  46993  fourierdlem62  46997  fourierdlem65  47000  fourierdlem66  47001  fourierdlem68  47003  fourierdlem72  47007  fourierdlem73  47008  fourierdlem76  47011  fourierdlem80  47015  fourierdlem83  47018  fourierdlem85  47020  fourierdlem89  47024  fourierdlem90  47025  fourierdlem91  47026  fourierdlem95  47030  fourierdlem97  47032  fourierdlem101  47036  fourierdlem103  47038  fourierdlem104  47039  fourierdlem111  47046  sqwvfoura  47057  sqwvfourb  47058  fourierswlem  47059  fouriersw  47060  elaa2lem  47062  etransclem8  47071  etransclem18  47081  etransclem20  47083  etransclem21  47084  etransclem23  47086  etransclem24  47087  etransclem31  47094  etransclem33  47096  etransclem35  47098  etransclem45  47108  etransclem46  47109  etransclem47  47110  etransclem48  47111  hoicvrrex  47385  hoidmvlelem2  47425  smfmullem1  47620  sigarim  47680  sigarac  47681  sigaraf  47682  sigarmf  47683  sigarls  47686  sigardiv  47690  sigarcol  47693  cevathlem1  47696  sin3t  47736  cos3t  47737  sin5tlem1  47738  sin5tlem2  47739  sin5tlem3  47740  sin5tlem4  47741  sin5tlem5  47742  sin5t  47743  cos5t  47744  fldivmod  48233  fmtnorec2lem  48446  fmtnorec3  48452  fmtnorec4  48453  fmtnoprmfac1  48469  fmtnoprmfac2  48471  fmtnofac2lem  48472  sfprmdvdsmersenne  48507  lighneallem3  48511  quad1  48537  requad01  48538  requad2  48540  opeoALTV  48601  perfectALTVlem2  48639  fppr2odd  48648  0nodd  49086  2nodd  49088  2zlidl  49156  2zrngnmlid  49171  altgsumbcALT  49284  nn0sumshdiglemA  49550  nn0sumshdiglemB  49551  nn0sumshdiglem2  49553  nn0mullong  49556  itcovalt2lem2lem2  49605  ackval2  49613  submuladdmuld  49632  affinecomb2  49634  affineid  49635  1subrec1sub  49636  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669  rrx2linest  49673  line2x  49685  line2y  49686  itschlc0yqe  49691  itsclc0yqsollem1  49693  itsclc0yqsol  49695  itscnhlc0xyqsol  49696  itschlc0xyqsol1  49697  itschlc0xyqsol  49698  itsclc0xyqsolr  49700  2itscplem1  49709  2itscplem2  49710  2itscplem3  49711  2itscp  49712  itscnhlinecirc02plem1  49713  itscnhlinecirc02plem2  49714  inlinecirc02plem  49717  inlinecirc02p  49718  dvsec  50690  i2linesd  50709  aacllem  50773  crossp3d  50801  amgmwlem  50821  amgmlemALT  50822