Theorem mulcld 11159

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030   · cmul 11037

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mul02lem1  11316  addrid  11320  cnegex  11321  kcnktkm1cn  11575  subaddmulsub  11607  mulsubaddmulsub  11608  receu  11789  divrec  11819  divcan3  11829  muldivdir  11841  subdivcomb1  11844  subdivcomb2  11845  divdivdiv  11850  divsubdiv  11865  lineq  11986  cru  12145  mul2lt0rlt0  13040  lincmb01cmp  13442  iccf1o  13443  flpmodeq  13827  moddiffl  13835  modvalp1  13843  modcyc  13859  modadd1  13861  modmuladdnn0  13871  modmul1  13880  modaddmulmod  13894  mulexpz  14058  expmulz  14064  binom3  14180  bernneq  14185  mulsubdivbinom2  14218  muldivbinom2  14219  remullem  15084  cjreim2  15117  absimle  15265  abstri  15287  sqreulem  15316  sqreu  15317  bhmafibid1cn  15422  bhmafibid2cn  15423  bhmafibid1  15424  bhmafibid2  15425  mulcn2  15552  reccn2  15553  o1rlimmul  15575  rlimmul  15601  isummulc2  15718  fsummulc2  15740  fsumparts  15763  indsum  15785  binomlem  15788  binom1dif  15792  incexclem  15795  incexc  15796  incexc2  15797  pwdif  15827  geomulcvg  15835  mertenslem1  15843  mertens  15845  fprodmul  15919  fprodn0f  15950  iprodmul  15962  binomfallfaclem1  15998  binomfallfaclem2  15999  binomrisefac  16001  bpolycl  16011  bpolysum  16012  bpolydiflem  16013  bpoly4  16018  efaddlem  16052  sinadd  16125  cosadd  16126  tanaddlem  16127  tanadd  16128  addsin  16131  sincossq  16137  sin2t  16138  dvds2ln  16252  oddm1even  16306  pwp1fsum  16354  flodddiv4  16378  sadadd2lem2  16413  bezoutlem2  16503  bezoutlem3  16504  bezoutlem4  16505  lcmgcdlem  16569  phiprmpw  16740  pythagtriplem12  16791  pythagtriplem14  16793  pythagtriplem16  16795  pcpremul  16808  pcaddlem  16853  fldivp1  16862  mul4sqlem  16918  4sqlem14  16923  vdwapun  16939  vdwlem2  16947  vdwlem6  16951  ablsimpgfindlem1  20078  zringlpirlem3  21457  znunit  21556  blcvx  24776  icopnfcnv  24922  cphipipcj  25180  cphipval2  25221  4cphipval2  25222  cphipval  25223  mbfmulc2re  25628  mbfmulc2  25643  itg1addlem4  25679  itg1addlem5  25680  itg1mulc  25684  mbfmul  25706  itgcl  25764  itgcnlem  25770  iblmulc2  25811  itgmulc2  25814  itgabs  25815  itgsplit  25816  dvmulbr  25919  dvcmul  25924  dvcmulf  25925  dvexp  25933  dvmptcmul  25944  dvmptdiv  25954  dvexp3  25958  dvsincos  25961  cmvth  25971  dvlipcn  25974  dvfsumabs  26003  dvfsumlem1  26006  ftc1lem4  26019  itgparts  26027  itgpowd  26030  plyf  26176  ply1termlem  26181  plyeq0lem  26188  plypf1  26190  plyaddlem1  26191  plymullem1  26192  coeeulem  26202  coeidlem  26215  coeid3  26218  plyco  26219  coemullem  26228  coemulhi  26232  coemulc  26233  dgrcolem2  26252  plycjlem  26254  plyrecj  26259  dvply1  26263  vieta1lem2  26291  vieta1  26292  elqaalem3  26301  aareccl  26306  aalioulem1  26312  taylfvallem1  26336  tayl0  26341  dvtaylp  26350  taylthlem2  26354  taylthlem2OLD  26355  psergf  26393  radcnvlem1  26394  dvradcnv  26402  psercn2  26404  pserdvlem2  26409  pserdv2  26411  abelthlem4  26415  abelthlem5  26416  abelthlem6  26417  abelthlem7  26419  abelthlem9  26421  tanregt0  26519  efgh  26521  efabl  26530  efsubm  26531  cosargd  26588  abslogle  26598  tanarg  26599  advlogexp  26635  logtayllem  26639  logtayl  26640  cxpadd  26659  mulcxp  26665  cxpmul  26668  cxpmul2  26669  cxpmul2z  26671  abscxp  26672  abscxp2  26673  dvcxp2  26721  abscxpbnd  26733  root1eq1  26735  cxpeq  26737  angcan  26782  pythag  26797  ssscongptld  26802  affineequiv  26803  affineequiv2  26804  affineequiv3  26805  affineequiv4  26806  chordthmlem2  26813  chordthmlem3  26814  chordthmlem4  26815  chordthmlem5  26816  heron  26818  quad2  26819  quad  26820  dcubic1lem  26823  dcubic2  26824  dcubic1  26825  dcubic  26826  mcubic  26827  cubic2  26828  cubic  26829  binom4  26830  dquartlem1  26831  dquartlem2  26832  dquart  26833  quart1cl  26834  quart1lem  26835  quart1  26836  quartlem1  26837  quartlem2  26838  atantayl3  26919  leibpi  26922  birthdaylem2  26932  divsqrtsumo1  26964  cvxcl  26965  jensenlem2  26968  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem4  27012  lgamgulmlem5  27013  lgamgulmlem6  27014  lgamgulm2  27016  lgamcvg2  27035  gamcvg  27036  gamcvg2lem  27039  wilthlem2  27049  ftalem1  27053  ftalem2  27054  ftalem4  27056  ftalem5  27057  basellem2  27062  basellem3  27063  basellem8  27068  muinv  27173  fsumdvdsmul  27175  logfacrlim  27204  logexprlim  27205  perfectlem2  27210  bposlem9  27272  gausslemma2dlem4  27349  lgsquad2lem1  27364  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2sqlem3  27400  2sqmod  27416  rplogsumlem1  27464  dchrisumlem2  27470  dchrisumlem3  27471  dchrmusum2  27474  dchrvmasumlem1  27475  dchrvmasum2lem  27476  dchrvmasum2if  27477  dchrvmasumlem3  27479  dchrvmasumiflem1  27481  dchrvmasumiflem2  27482  rpvmasum2  27492  dchrisum0lem1  27496  dchrisum0lem2a  27497  dchrisum0lem2  27498  dchrmusumlem  27502  dchrvmasumlem  27503  rplogsum  27507  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  mulog2sumlem1  27514  mulog2sumlem2  27515  mulog2sumlem3  27516  vmalogdivsum  27519  logsqvma  27522  log2sumbnd  27524  selberglem1  27525  selberglem2  27526  selberglem3  27527  selberg  27528  selberg2lem  27530  selberg2  27531  selberg3lem1  27537  selberg3  27539  selberg4lem1  27540  selberg4  27541  pntrsumo1  27545  selbergr  27548  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntsval2  27556  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntlemb  27577  pntlemf  27585  pntlemo  27587  ostth2lem2  27614  ostth2lem3  27615  ttgcontlem1  28970  brbtwn2  28991  colinearalg  28996  ax5seglem2  29015  ax5seglem9  29023  axeuclidlem  29048  axcontlem2  29051  axcontlem4  29053  axcontlem7  29056  axcontlem8  29057  finsumvtxdg2ssteplem4  29635  ex-ind-dvds  30549  nrt2irr  30561  ipval2  30796  dipcl  30801  riesz3i  32151  re0cj  32834  pythagreim  32836  quad3d  32840  indsumin  32939  dpfrac1  32969  wrdt2ind  33031  zringfrac  33632  ccfldsrarelvec  33834  ccfldextdgrr  33835  constrrtll  33894  constrrtlc1  33895  constrrtcclem  33897  constrrtcc  33898  constrconj  33908  constrfin  33909  constrelextdg2  33910  nn0constr  33924  constraddcl  33925  constrnegcl  33926  constrdircl  33928  iconstr  33929  constrremulcl  33930  constrrecl  33932  constrimcl  33933  constrmulcl  33934  constrreinvcl  33935  constrinvcl  33936  constrresqrtcl  33940  constrabscl  33941  constrsqrtcl  33942  cos9thpiminplylem1  33945  cos9thpiminplylem2  33946  cos9thpiminplylem3  33947  cos9thpiminply  33951  cos9thpinconstrlem1  33952  cos9thpinconstrlem2  33953  cos9thpinconstr  33954  cnre2csqima  34074  rmulccn  34091  dya2icoseg  34440  oddpwdc  34517  eulerpartlems  34523  eulerpartlemsv3  34524  eulerpartlemgs2  34543  signsplypnf  34713  itgexpif  34769  breprexplemc  34795  breprexp  34796  vtscl  34801  vtsprod  34802  circlemeth  34803  logdivsqrle  34813  hgt750lemf  34816  hgt750leme  34821  subfacval2  35388  subfaclim  35389  resconn  35447  iprodgam  35943  fwddifnp1  36366  knoppcnlem10  36781  knoppndvlem2  36792  knoppndvlem7  36797  knoppndvlem9  36799  knoppndvlem11  36801  knoppndvlem14  36804  knoppndvlem16  36806  knoppndvlem17  36807  bj-subcom  37641  bj-bary1lem  37643  bj-bary1lem1  37644  bj-bary1  37645  iblmulc2nc  38023  itgmulc2nc  38026  itgabsnc  38027  ftc1cnnclem  38029  ftc1anclem3  38033  dvasin  38042  areacirclem1  38046  areacirclem4  38049  areacirc  38051  cntotbnd  38134  3factsumint1  42477  3factsumint3  42479  3factsumint4  42480  lcmineqlem2  42486  lcmineqlem6  42490  lcmineqlem8  42492  lcmineqlem10  42494  lcmineqlem11  42495  lcmineqlem12  42496  lcmineqlem16  42500  lcmineqlem18  42502  lcmineqlem23  42507  3lexlogpow5ineq5  42516  aks4d1p1p1  42519  dvrelogpow2b  42524  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  primrootscoprmpow  42555  posbezout  42556  primrootscoprbij  42558  primrootspoweq0  42562  2np3bcnp1  42600  2ap1caineq  42601  oddnumth  42760  nicomachus  42761  sumcubes  42762  ef11d  42788  cxp112d  42790  cxp111d  42791  readvrec2  42810  sn-addlid  42853  sn-it0e0  42865  sn-negex12  42866  sn-mul01  42875  sn-mullid  42885  sn-0tie0  42913  sn-mul02  42914  cnreeu  42952  fltnltalem  43112  fltnlta  43113  cu3addd  43130  3cubeslem2  43134  3cubeslem3l  43135  3cubeslem3r  43136  3cubeslem4  43138  pellexlem1  43278  pellexlem2  43279  pellexlem6  43283  pell1234qrne0  43302  pell1234qrreccl  43303  pell1234qrmulcl  43304  pell1234qrdich  43310  pell14qrdich  43318  pell1qrge1  43319  pell1qrgaplem  43322  rmspecsqrtnq  43355  qirropth  43357  rmxyneg  43369  rmxyadd  43370  rmxm1  43383  rmym1  43384  rmxluc  43385  rmyluc  43386  rmxdbl  43388  rmydbl  43389  jm2.18  43437  jm2.19lem1  43438  jm2.19lem2  43439  jm2.19lem4  43441  jm2.19  43442  jm2.22  43444  jm2.23  43445  jm2.25  43448  jm2.27c  43456  jm3.1lem2  43467  flcidc  43619  areaquad  43665  sqrtcval  44089  inductionexd  44603  imo72b2lem0  44613  int-leftdistd  44627  radcnvrat  44762  expgrowth  44783  binomcxplemwb  44796  binomcxplemnn0  44797  binomcxplemfrat  44799  binomcxplemdvbinom  44801  binomcxplemnotnn0  44804  sineq0ALT  45384  mul13d  45734  fperiodmullem  45757  fperiodmul  45758  divcan8d  45766  dmmcand  45767  ltdiv23neg  45844  mulc1cncfg  46040  mccllem  46048  clim1fr1  46052  mullimc  46067  mullimcf  46074  sumnnodd  46081  reclimc  46102  sinmulcos  46314  coskpi2  46315  cosknegpi  46318  dvsinexp  46360  dvasinbx  46369  dvdivf  46371  dvdivbd  46372  dvdivcncf  46376  dvbdfbdioolem2  46378  dvxpaek  46389  dvnxpaek  46391  dvnmul  46392  dvmptfprodlem  46393  dvnprodlem2  46396  itgsinexplem1  46403  itgsinexp  46404  itgcoscmulx  46418  itgsincmulx  46423  itgiccshift  46429  itgperiod  46430  stoweidlem1  46450  stoweidlem11  46460  stoweidlem13  46462  stoweidlem14  46463  stoweidlem17  46466  stoweidlem25  46474  stoweidlem26  46475  stoweidlem42  46491  wallispilem4  46517  wallispilem5  46518  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  wallispi2  46522  stirlinglem1  46523  stirlinglem3  46525  stirlinglem4  46526  stirlinglem5  46527  stirlinglem6  46528  stirlinglem7  46529  stirlinglem8  46530  stirlinglem10  46532  stirlinglem11  46533  stirlinglem12  46534  stirlinglem13  46535  stirlinglem14  46536  stirlinglem15  46537  dirker2re  46541  dirkerdenne0  46542  dirkerper  46545  dirkertrigeqlem1  46547  dirkertrigeqlem2  46548  dirkertrigeqlem3  46549  dirkertrigeq  46550  dirkeritg  46551  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem26  46582  fourierdlem30  46586  fourierdlem39  46595  fourierdlem42  46598  fourierdlem47  46602  fourierdlem48  46603  fourierdlem56  46611  fourierdlem57  46612  fourierdlem58  46613  fourierdlem62  46617  fourierdlem65  46620  fourierdlem66  46621  fourierdlem68  46623  fourierdlem72  46627  fourierdlem73  46628  fourierdlem76  46631  fourierdlem80  46635  fourierdlem83  46638  fourierdlem85  46640  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem95  46650  fourierdlem97  46652  fourierdlem101  46656  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  sqwvfoura  46677  sqwvfourb  46678  fourierswlem  46679  fouriersw  46680  elaa2lem  46682  etransclem8  46691  etransclem18  46701  etransclem20  46703  etransclem21  46704  etransclem23  46706  etransclem24  46707  etransclem31  46714  etransclem33  46716  etransclem35  46718  etransclem45  46728  etransclem46  46729  etransclem47  46730  etransclem48  46731  hoicvrrex  47005  hoidmvlelem2  47045  smfmullem1  47240  sigarim  47300  sigarac  47301  sigaraf  47302  sigarmf  47303  sigarls  47306  sigardiv  47310  sigarcol  47313  cevathlem1  47316  sin3t  47338  cos3t  47339  sin5tlem1  47340  sin5tlem2  47341  sin5tlem3  47342  sin5tlem4  47343  sin5tlem5  47344  sin5t  47345  fldivmod  47807  fmtnorec2lem  48020  fmtnorec3  48026  fmtnorec4  48027  fmtnoprmfac1  48043  fmtnoprmfac2  48045  fmtnofac2lem  48046  sfprmdvdsmersenne  48081  lighneallem3  48085  quad1  48111  requad01  48112  requad2  48114  opeoALTV  48175  perfectALTVlem2  48213  fppr2odd  48222  0nodd  48661  2nodd  48663  2zlidl  48731  2zrngnmlid  48746  altgsumbcALT  48844  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem2  49113  nn0mullong  49116  itcovalt2lem2lem2  49165  ackval2  49173  submuladdmuld  49192  affinecomb2  49194  affineid  49195  1subrec1sub  49196  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2linest  49233  line2x  49245  line2y  49246  itschlc0yqe  49251  itsclc0yqsollem1  49253  itsclc0yqsol  49255  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  itschlc0xyqsol  49258  itsclc0xyqsolr  49260  2itscplem1  49269  2itscplem2  49270  2itscplem3  49271  2itscp  49272  itscnhlinecirc02plem1  49273  itscnhlinecirc02plem2  49274  inlinecirc02plem  49277  inlinecirc02p  49278  i2linesd  50269  aacllem  50291  amgmwlem  50292  amgmlemALT  50293