Theorem mulcld 11170

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   · cmul 11049

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

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

This theorem is referenced by:  mul02lem1  11326  addrid  11330  cnegex  11331  kcnktkm1cn  11585  subaddmulsub  11617  mulsubaddmulsub  11618  receu  11799  divrec  11829  divcan3  11839  muldivdir  11851  subdivcomb1  11853  subdivcomb2  11854  divdivdiv  11859  divsubdiv  11874  lineq  11995  cru  12154  mul2lt0rlt0  13031  lincmb01cmp  13432  iccf1o  13433  flpmodeq  13812  moddiffl  13820  modvalp1  13828  modcyc  13844  modadd1  13846  modmuladdnn0  13856  modmul1  13865  modaddmulmod  13879  mulexpz  14043  expmulz  14049  binom3  14165  bernneq  14170  mulsubdivbinom2  14203  muldivbinom2  14204  remullem  15070  cjreim2  15103  absimle  15251  abstri  15273  sqreulem  15302  sqreu  15303  bhmafibid1cn  15408  bhmafibid2cn  15409  bhmafibid1  15410  bhmafibid2  15411  mulcn2  15538  reccn2  15539  o1rlimmul  15561  rlimmul  15587  isummulc2  15704  fsummulc2  15726  fsumparts  15748  binomlem  15771  binom1dif  15775  incexclem  15778  incexc  15779  incexc2  15780  pwdif  15810  geomulcvg  15818  mertenslem1  15826  mertens  15828  fprodmul  15902  fprodn0f  15933  iprodmul  15945  binomfallfaclem1  15981  binomfallfaclem2  15982  binomrisefac  15984  bpolycl  15994  bpolysum  15995  bpolydiflem  15996  bpoly4  16001  efaddlem  16035  sinadd  16108  cosadd  16109  tanaddlem  16110  tanadd  16111  addsin  16114  sincossq  16120  sin2t  16121  dvds2ln  16235  oddm1even  16289  pwp1fsum  16337  flodddiv4  16361  sadadd2lem2  16396  bezoutlem2  16486  bezoutlem3  16487  bezoutlem4  16488  lcmgcdlem  16552  phiprmpw  16722  pythagtriplem12  16773  pythagtriplem14  16775  pythagtriplem16  16777  pcpremul  16790  pcaddlem  16835  fldivp1  16844  mul4sqlem  16900  4sqlem14  16905  vdwapun  16921  vdwlem2  16929  vdwlem6  16933  ablsimpgfindlem1  20023  zringlpirlem3  21406  znunit  21505  blcvx  24719  icopnfcnv  24873  cphipipcj  25133  cphipval2  25174  4cphipval2  25175  cphipval  25176  mbfmulc2re  25582  mbfmulc2  25597  itg1addlem4  25633  itg1addlem5  25634  itg1mulc  25638  mbfmul  25660  itgcl  25718  itgcnlem  25724  iblmulc2  25765  itgmulc2  25768  itgabs  25769  itgsplit  25770  dvmulbr  25874  dvmulbrOLD  25875  dvcmul  25880  dvcmulf  25881  dvexp  25890  dvmptcmul  25901  dvmptdiv  25911  dvexp3  25915  dvsincos  25918  cmvth  25928  cmvthOLD  25929  dvlipcn  25932  dvfsumabs  25962  dvfsumlem1  25965  ftc1lem4  25979  itgparts  25987  itgpowd  25990  plyf  26136  ply1termlem  26141  plyeq0lem  26148  plypf1  26150  plyaddlem1  26151  plymullem1  26152  coeeulem  26162  coeidlem  26175  coeid3  26178  plyco  26179  coemullem  26188  coemulhi  26192  coemulc  26193  dgrcolem2  26213  plycjlem  26215  plyrecj  26220  dvply1  26224  vieta1lem2  26252  vieta1  26253  elqaalem3  26262  aareccl  26267  aalioulem1  26273  taylfvallem1  26297  tayl0  26302  dvtaylp  26311  taylthlem2  26315  taylthlem2OLD  26316  psergf  26354  radcnvlem1  26355  dvradcnv  26363  psercn2  26365  psercn2OLD  26366  pserdvlem2  26371  pserdv2  26373  abelthlem4  26377  abelthlem5  26378  abelthlem6  26379  abelthlem7  26381  abelthlem9  26383  tanregt0  26481  efgh  26483  efabl  26492  efsubm  26493  cosargd  26550  abslogle  26560  tanarg  26561  advlogexp  26597  logtayllem  26601  logtayl  26602  cxpadd  26621  mulcxp  26627  cxpmul  26630  cxpmul2  26631  cxpmul2z  26633  abscxp  26634  abscxp2  26635  dvcxp2  26683  abscxpbnd  26696  root1eq1  26698  cxpeq  26700  angcan  26745  pythag  26760  ssscongptld  26765  affineequiv  26766  affineequiv2  26767  affineequiv3  26768  affineequiv4  26769  chordthmlem2  26776  chordthmlem3  26777  chordthmlem4  26778  chordthmlem5  26779  heron  26781  quad2  26782  quad  26783  dcubic1lem  26786  dcubic2  26787  dcubic1  26788  dcubic  26789  mcubic  26790  cubic2  26791  cubic  26792  binom4  26793  dquartlem1  26794  dquartlem2  26795  dquart  26796  quart1cl  26797  quart1lem  26798  quart1  26799  quartlem1  26800  quartlem2  26801  atantayl3  26882  leibpi  26885  birthdaylem2  26895  divsqrtsumo1  26927  cvxcl  26928  jensenlem2  26931  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem4  26975  lgamgulmlem5  26976  lgamgulmlem6  26977  lgamgulm2  26979  lgamcvg2  26998  gamcvg  26999  gamcvg2lem  27002  wilthlem2  27012  ftalem1  27016  ftalem2  27017  ftalem4  27019  ftalem5  27020  basellem2  27025  basellem3  27026  basellem8  27031  muinv  27136  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  logfacrlim  27168  logexprlim  27169  perfectlem2  27174  bposlem9  27236  gausslemma2dlem4  27313  lgsquad2lem1  27328  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  2sqlem3  27364  2sqmod  27380  rplogsumlem1  27428  dchrisumlem2  27434  dchrisumlem3  27435  dchrmusum2  27438  dchrvmasumlem1  27439  dchrvmasum2lem  27440  dchrvmasum2if  27441  dchrvmasumlem3  27443  dchrvmasumiflem1  27445  dchrvmasumiflem2  27446  rpvmasum2  27456  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem2  27462  dchrmusumlem  27466  dchrvmasumlem  27467  rplogsum  27471  mudivsum  27474  mulogsumlem  27475  mulogsum  27476  mulog2sumlem1  27478  mulog2sumlem2  27479  mulog2sumlem3  27480  vmalogdivsum  27483  logsqvma  27486  log2sumbnd  27488  selberglem1  27489  selberglem2  27490  selberglem3  27491  selberg  27492  selberg2lem  27494  selberg2  27495  selberg3lem1  27501  selberg3  27503  selberg4lem1  27504  selberg4  27505  pntrsumo1  27509  selbergr  27512  selberg3r  27513  selberg4r  27514  selberg34r  27515  pntsval2  27520  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntlemb  27541  pntlemf  27549  pntlemo  27551  ostth2lem2  27578  ostth2lem3  27579  ttgcontlem1  28865  brbtwn2  28885  colinearalg  28890  ax5seglem2  28909  ax5seglem9  28917  axeuclidlem  28942  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem8  28951  finsumvtxdg2ssteplem4  29529  ex-ind-dvds  30440  nrt2irr  30452  ipval2  30686  dipcl  30691  riesz3i  32041  re0cj  32717  pythagreim  32719  quad3d  32723  indsum  32834  indsumin  32835  dpfrac1  32862  wrdt2ind  32925  zringfrac  33518  ccfldsrarelvec  33659  ccfldextdgrr  33660  constrrtll  33714  constrrtlc1  33715  constrrtcclem  33717  constrrtcc  33718  constrconj  33728  constrfin  33729  constrelextdg2  33730  nn0constr  33744  constraddcl  33745  constrnegcl  33746  constrdircl  33748  iconstr  33749  constrremulcl  33750  constrrecl  33752  constrimcl  33753  constrmulcl  33754  constrreinvcl  33755  constrinvcl  33756  constrresqrtcl  33760  constrabscl  33761  constrsqrtcl  33762  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  cos9thpiminplylem3  33767  cos9thpiminply  33771  cos9thpinconstrlem1  33772  cos9thpinconstrlem2  33773  cos9thpinconstr  33774  cnre2csqima  33894  rmulccn  33911  dya2icoseg  34261  oddpwdc  34338  eulerpartlems  34344  eulerpartlemsv3  34345  eulerpartlemgs2  34364  signsplypnf  34534  itgexpif  34590  breprexplemc  34616  breprexp  34617  vtscl  34622  vtsprod  34623  circlemeth  34624  logdivsqrle  34634  hgt750lemf  34637  hgt750leme  34642  subfacval2  35167  subfaclim  35168  resconn  35226  iprodgam  35722  fwddifnp1  36146  knoppcnlem10  36483  knoppndvlem2  36494  knoppndvlem7  36499  knoppndvlem9  36501  knoppndvlem11  36503  knoppndvlem14  36506  knoppndvlem16  36508  knoppndvlem17  36509  bj-subcom  37289  bj-bary1lem  37291  bj-bary1lem1  37292  bj-bary1  37293  iblmulc2nc  37672  itgmulc2nc  37675  itgabsnc  37676  ftc1cnnclem  37678  ftc1anclem3  37682  dvasin  37691  areacirclem1  37695  areacirclem4  37698  areacirc  37700  cntotbnd  37783  3factsumint1  42002  3factsumint3  42004  3factsumint4  42005  lcmineqlem2  42011  lcmineqlem6  42015  lcmineqlem8  42017  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem12  42021  lcmineqlem16  42025  lcmineqlem18  42027  lcmineqlem23  42032  3lexlogpow5ineq5  42041  aks4d1p1p1  42044  dvrelogpow2b  42049  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij  42083  primrootspoweq0  42087  2np3bcnp1  42125  2ap1caineq  42126  oddnumth  42292  nicomachus  42293  sumcubes  42294  ef11d  42320  cxp112d  42322  cxp111d  42323  readvrec2  42342  sn-addlid  42385  sn-it0e0  42397  sn-negex12  42398  sn-mul01  42407  sn-mullid  42417  sn-0tie0  42432  sn-mul02  42433  cnreeu  42471  fltnltalem  42643  fltnlta  42644  cu3addd  42662  3cubeslem2  42666  3cubeslem3l  42667  3cubeslem3r  42668  3cubeslem4  42670  pellexlem1  42810  pellexlem2  42811  pellexlem6  42815  pell1234qrne0  42834  pell1234qrreccl  42835  pell1234qrmulcl  42836  pell1234qrdich  42842  pell14qrdich  42850  pell1qrge1  42851  pell1qrgaplem  42854  rmspecsqrtnq  42887  qirropth  42889  rmxyneg  42902  rmxyadd  42903  rmxm1  42916  rmym1  42917  rmxluc  42918  rmyluc  42919  rmxdbl  42921  rmydbl  42922  jm2.18  42970  jm2.19lem1  42971  jm2.19lem2  42972  jm2.19lem4  42974  jm2.19  42975  jm2.22  42977  jm2.23  42978  jm2.25  42981  jm2.27c  42989  jm3.1lem2  43000  flcidc  43152  areaquad  43198  sqrtcval  43623  inductionexd  44137  imo72b2lem0  44147  int-leftdistd  44161  radcnvrat  44296  expgrowth  44317  binomcxplemwb  44330  binomcxplemnn0  44331  binomcxplemfrat  44333  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  sineq0ALT  44919  mul13d  45271  fperiodmullem  45294  fperiodmul  45295  divcan8d  45303  dmmcand  45304  ltdiv23neg  45383  mulc1cncfg  45580  mccllem  45588  clim1fr1  45592  mullimc  45607  mullimcf  45614  sumnnodd  45621  reclimc  45644  sinmulcos  45856  coskpi2  45857  cosknegpi  45860  dvsinexp  45902  dvasinbx  45911  dvdivf  45913  dvdivbd  45914  dvdivcncf  45918  dvbdfbdioolem2  45920  dvxpaek  45931  dvnxpaek  45933  dvnmul  45934  dvmptfprodlem  45935  dvnprodlem2  45938  itgsinexplem1  45945  itgsinexp  45946  itgcoscmulx  45960  itgsincmulx  45965  itgiccshift  45971  itgperiod  45972  stoweidlem1  45992  stoweidlem11  46002  stoweidlem13  46004  stoweidlem14  46005  stoweidlem17  46008  stoweidlem25  46016  stoweidlem26  46017  stoweidlem42  46033  wallispilem4  46059  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  wallispi2lem2  46063  wallispi2  46064  stirlinglem1  46065  stirlinglem3  46067  stirlinglem4  46068  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem8  46072  stirlinglem10  46074  stirlinglem11  46075  stirlinglem12  46076  stirlinglem13  46077  stirlinglem14  46078  stirlinglem15  46079  dirker2re  46083  dirkerdenne0  46084  dirkerper  46087  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkeritg  46093  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem26  46124  fourierdlem30  46128  fourierdlem39  46137  fourierdlem42  46140  fourierdlem47  46144  fourierdlem48  46145  fourierdlem56  46153  fourierdlem57  46154  fourierdlem58  46155  fourierdlem62  46159  fourierdlem65  46162  fourierdlem66  46163  fourierdlem68  46165  fourierdlem72  46169  fourierdlem73  46170  fourierdlem76  46173  fourierdlem80  46177  fourierdlem83  46180  fourierdlem85  46182  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem95  46192  fourierdlem97  46194  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  elaa2lem  46224  etransclem8  46233  etransclem18  46243  etransclem20  46245  etransclem21  46246  etransclem23  46248  etransclem24  46249  etransclem31  46256  etransclem33  46258  etransclem35  46260  etransclem45  46270  etransclem46  46271  etransclem47  46272  etransclem48  46273  hoicvrrex  46547  hoidmvlelem2  46587  smfmullem1  46782  sigarim  46842  sigarac  46843  sigaraf  46844  sigarmf  46845  sigarls  46848  sigardiv  46852  sigarcol  46855  cevathlem1  46858  fldivmod  47332  fmtnorec2lem  47536  fmtnorec3  47542  fmtnorec4  47543  fmtnoprmfac1  47559  fmtnoprmfac2  47561  fmtnofac2lem  47562  sfprmdvdsmersenne  47597  lighneallem3  47601  quad1  47614  requad01  47615  requad2  47617  opeoALTV  47678  perfectALTVlem2  47716  fppr2odd  47725  0nodd  48151  2nodd  48153  2zlidl  48221  2zrngnmlid  48236  altgsumbcALT  48334  nn0sumshdiglemA  48601  nn0sumshdiglemB  48602  nn0sumshdiglem2  48604  nn0mullong  48607  itcovalt2lem2lem2  48656  ackval2  48664  submuladdmuld  48683  affinecomb2  48685  affineid  48686  1subrec1sub  48687  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  rrx2linest  48724  line2x  48736  line2y  48737  itschlc0yqe  48742  itsclc0yqsollem1  48744  itsclc0yqsol  48746  itscnhlc0xyqsol  48747  itschlc0xyqsol1  48748  itschlc0xyqsol  48749  itsclc0xyqsolr  48751  2itscplem1  48760  2itscplem2  48761  2itscplem3  48762  2itscp  48763  itscnhlinecirc02plem1  48764  itscnhlinecirc02plem2  48765  inlinecirc02plem  48768  inlinecirc02p  48769  i2linesd  49761  aacllem  49783  amgmwlem  49784  amgmlemALT  49785