Theorem mulcld 11156

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   · cmul 11034

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  mul02lem1  11313  addrid  11317  cnegex  11318  kcnktkm1cn  11572  subaddmulsub  11604  mulsubaddmulsub  11605  receu  11786  divrec  11816  divcan3  11826  muldivdir  11838  subdivcomb1  11841  subdivcomb2  11842  divdivdiv  11847  divsubdiv  11862  lineq  11983  cru  12142  mul2lt0rlt0  13037  lincmb01cmp  13439  iccf1o  13440  flpmodeq  13824  moddiffl  13832  modvalp1  13840  modcyc  13856  modadd1  13858  modmuladdnn0  13868  modmul1  13877  modaddmulmod  13891  mulexpz  14055  expmulz  14061  binom3  14177  bernneq  14182  mulsubdivbinom2  14215  muldivbinom2  14216  remullem  15081  cjreim2  15114  absimle  15262  abstri  15284  sqreulem  15313  sqreu  15314  bhmafibid1cn  15419  bhmafibid2cn  15420  bhmafibid1  15421  bhmafibid2  15422  mulcn2  15549  reccn2  15550  o1rlimmul  15572  rlimmul  15598  isummulc2  15715  fsummulc2  15737  fsumparts  15760  indsum  15782  binomlem  15785  binom1dif  15789  incexclem  15792  incexc  15793  incexc2  15794  pwdif  15824  geomulcvg  15832  mertenslem1  15840  mertens  15842  fprodmul  15916  fprodn0f  15947  iprodmul  15959  binomfallfaclem1  15995  binomfallfaclem2  15996  binomrisefac  15998  bpolycl  16008  bpolysum  16009  bpolydiflem  16010  bpoly4  16015  efaddlem  16049  sinadd  16122  cosadd  16123  tanaddlem  16124  tanadd  16125  addsin  16128  sincossq  16134  sin2t  16135  dvds2ln  16249  oddm1even  16303  pwp1fsum  16351  flodddiv4  16375  sadadd2lem2  16410  bezoutlem2  16500  bezoutlem3  16501  bezoutlem4  16502  lcmgcdlem  16566  phiprmpw  16737  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem16  16792  pcpremul  16805  pcaddlem  16850  fldivp1  16859  mul4sqlem  16915  4sqlem14  16920  vdwapun  16936  vdwlem2  16944  vdwlem6  16948  ablsimpgfindlem1  20075  zringlpirlem3  21439  znunit  21538  blcvx  24781  icopnfcnv  24927  cphipipcj  25185  cphipval2  25226  4cphipval2  25227  cphipval  25228  mbfmulc2re  25633  mbfmulc2  25648  itg1addlem4  25684  itg1addlem5  25685  itg1mulc  25689  mbfmul  25711  itgcl  25769  itgcnlem  25775  iblmulc2  25816  itgmulc2  25819  itgabs  25820  itgsplit  25821  dvmulbr  25924  dvcmul  25929  dvcmulf  25930  dvexp  25938  dvmptcmul  25949  dvmptdiv  25959  dvexp3  25963  dvsincos  25966  cmvth  25976  dvlipcn  25979  dvfsumabs  26008  dvfsumlem1  26011  ftc1lem4  26024  itgparts  26032  itgpowd  26035  plyf  26181  ply1termlem  26186  plyeq0lem  26193  plypf1  26195  plyaddlem1  26196  plymullem1  26197  coeeulem  26207  coeidlem  26220  coeid3  26223  plyco  26224  coemullem  26233  coemulhi  26237  coemulc  26238  dgrcolem2  26257  plycjlem  26259  plyrecj  26264  dvply1  26268  vieta1lem2  26295  vieta1  26296  elqaalem3  26305  aareccl  26310  aalioulem1  26316  taylfvallem1  26340  tayl0  26345  dvtaylp  26353  taylthlem2  26357  psergf  26395  radcnvlem1  26396  dvradcnv  26404  psercn2  26406  pserdvlem2  26411  pserdv2  26413  abelthlem4  26417  abelthlem5  26418  abelthlem6  26419  abelthlem7  26421  abelthlem9  26423  tanregt0  26521  efgh  26523  efabl  26532  efsubm  26533  cosargd  26590  abslogle  26600  tanarg  26601  advlogexp  26637  logtayllem  26641  logtayl  26642  cxpadd  26661  mulcxp  26667  cxpmul  26670  cxpmul2  26671  cxpmul2z  26673  abscxp  26674  abscxp2  26675  dvcxp2  26723  abscxpbnd  26735  root1eq1  26737  cxpeq  26739  angcan  26784  pythag  26799  ssscongptld  26804  affineequiv  26805  affineequiv2  26806  affineequiv3  26807  affineequiv4  26808  chordthmlem2  26815  chordthmlem3  26816  chordthmlem4  26817  chordthmlem5  26818  heron  26820  quad2  26821  quad  26822  dcubic1lem  26825  dcubic2  26826  dcubic1  26827  dcubic  26828  mcubic  26829  cubic2  26830  cubic  26831  binom4  26832  dquartlem1  26833  dquartlem2  26834  dquart  26835  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem1  26839  quartlem2  26840  atantayl3  26921  leibpi  26924  birthdaylem2  26934  divsqrtsumo1  26965  cvxcl  26966  jensenlem2  26969  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  wilthlem2  27050  ftalem1  27054  ftalem2  27055  ftalem4  27057  ftalem5  27058  basellem2  27063  basellem3  27064  basellem8  27069  muinv  27174  fsumdvdsmul  27176  logfacrlim  27205  logexprlim  27206  perfectlem2  27211  bposlem9  27273  gausslemma2dlem4  27350  lgsquad2lem1  27365  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2sqlem3  27401  2sqmod  27417  rplogsumlem1  27465  dchrisumlem2  27471  dchrisumlem3  27472  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasum2lem  27477  dchrvmasum2if  27478  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrvmasumiflem2  27483  rpvmasum2  27493  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrmusumlem  27503  dchrvmasumlem  27504  rplogsum  27508  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  mulog2sumlem1  27515  mulog2sumlem2  27516  mulog2sumlem3  27517  vmalogdivsum  27520  logsqvma  27523  log2sumbnd  27525  selberglem1  27526  selberglem2  27527  selberglem3  27528  selberg  27529  selberg2lem  27531  selberg2  27532  selberg3lem1  27538  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrsumo1  27546  selbergr  27549  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntsval2  27557  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntlemb  27578  pntlemf  27586  pntlemo  27588  ostth2lem2  27615  ostth2lem3  27616  ttgcontlem1  28971  brbtwn2  28992  colinearalg  28997  ax5seglem2  29016  ax5seglem9  29024  axeuclidlem  29049  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  axcontlem8  29058  finsumvtxdg2ssteplem4  29635  ex-ind-dvds  30549  nrt2irr  30561  ipval2  30796  dipcl  30801  riesz3i  32151  re0cj  32835  pythagreim  32837  quad3d  32841  indsumin  32940  dpfrac1  32970  wrdt2ind  33032  zringfrac  33637  ccfldsrarelvec  33855  ccfldextdgrr  33856  constrrtll  33915  constrrtlc1  33916  constrrtcclem  33918  constrrtcc  33919  constrconj  33929  constrfin  33930  constrelextdg2  33931  nn0constr  33945  constraddcl  33946  constrnegcl  33947  constrdircl  33949  iconstr  33950  constrremulcl  33951  constrrecl  33953  constrimcl  33954  constrmulcl  33955  constrreinvcl  33956  constrinvcl  33957  constrresqrtcl  33961  constrabscl  33962  constrsqrtcl  33963  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  cos9thpinconstr  33975  cnre2csqima  34095  rmulccn  34112  dya2icoseg  34461  oddpwdc  34538  eulerpartlems  34544  eulerpartlemsv3  34545  eulerpartlemgs2  34564  signsplypnf  34734  itgexpif  34790  breprexplemc  34816  breprexp  34817  vtscl  34822  vtsprod  34823  circlemeth  34824  logdivsqrle  34834  hgt750lemf  34837  hgt750leme  34842  subfacval2  35415  subfaclim  35416  resconn  35474  iprodgam  35970  fwddifnp1  36393  knoppcnlem10  36808  knoppndvlem2  36819  knoppndvlem7  36824  knoppndvlem9  36826  knoppndvlem11  36828  knoppndvlem14  36831  knoppndvlem16  36833  knoppndvlem17  36834  bj-subcom  37668  bj-bary1lem  37670  bj-bary1lem1  37671  bj-bary1  37672  qdiff  37687  iblmulc2nc  38052  itgmulc2nc  38055  itgabsnc  38056  ftc1cnnclem  38058  ftc1anclem3  38062  dvasin  38071  areacirclem1  38075  areacirclem4  38078  areacirc  38080  cntotbnd  38163  3factsumint1  42506  3factsumint3  42508  3factsumint4  42509  lcmineqlem2  42515  lcmineqlem6  42519  lcmineqlem8  42521  lcmineqlem10  42523  lcmineqlem11  42524  lcmineqlem12  42525  lcmineqlem16  42529  lcmineqlem18  42531  lcmineqlem23  42536  3lexlogpow5ineq5  42545  aks4d1p1p1  42548  dvrelogpow2b  42553  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  primrootscoprmpow  42584  posbezout  42585  primrootscoprbij  42587  primrootspoweq0  42591  2np3bcnp1  42629  2ap1caineq  42630  oddnumth  42788  nicomachus  42789  sumcubes  42790  ef11d  42816  cxp112d  42818  cxp111d  42819  readvrec2  42838  sn-addlid  42881  sn-it0e0  42893  sn-negex12  42894  sn-mul01  42903  sn-mullid  42913  sn-0tie0  42941  sn-mul02  42942  cnreeu  42980  fltnltalem  43112  fltnlta  43113  cu3addd  43130  3cubeslem2  43134  3cubeslem3l  43135  3cubeslem3r  43136  3cubeslem4  43138  pellexlem1  43274  pellexlem2  43275  pellexlem6  43279  pell1234qrne0  43298  pell1234qrreccl  43299  pell1234qrmulcl  43300  pell1234qrdich  43306  pell14qrdich  43314  pell1qrge1  43315  pell1qrgaplem  43318  rmspecsqrtnq  43351  qirropth  43353  rmxyneg  43365  rmxyadd  43366  rmxm1  43379  rmym1  43380  rmxluc  43381  rmyluc  43382  rmxdbl  43384  rmydbl  43385  jm2.18  43433  jm2.19lem1  43434  jm2.19lem2  43435  jm2.19lem4  43437  jm2.19  43438  jm2.22  43440  jm2.23  43441  jm2.25  43444  jm2.27c  43452  jm3.1lem2  43463  flcidc  43615  areaquad  43661  sqrtcval  44085  inductionexd  44599  imo72b2lem0  44609  int-leftdistd  44623  radcnvrat  44758  expgrowth  44779  binomcxplemwb  44792  binomcxplemnn0  44793  binomcxplemfrat  44795  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  sineq0ALT  45380  mul13d  45728  fperiodmullem  45751  fperiodmul  45752  divcan8d  45760  dmmcand  45761  ltdiv23neg  45838  mulc1cncfg  46034  mccllem  46042  clim1fr1  46046  mullimc  46061  mullimcf  46068  sumnnodd  46075  reclimc  46096  sinmulcos  46308  coskpi2  46309  cosknegpi  46312  dvsinexp  46354  dvasinbx  46363  dvdivf  46365  dvdivbd  46366  dvdivcncf  46370  dvbdfbdioolem2  46372  dvxpaek  46383  dvnxpaek  46385  dvnmul  46386  dvmptfprodlem  46387  dvnprodlem2  46390  itgsinexplem1  46397  itgsinexp  46398  itgcoscmulx  46412  itgsincmulx  46417  itgiccshift  46423  itgperiod  46424  stoweidlem1  46444  stoweidlem11  46454  stoweidlem13  46456  stoweidlem14  46457  stoweidlem17  46460  stoweidlem25  46468  stoweidlem26  46469  stoweidlem42  46485  wallispilem4  46511  wallispilem5  46512  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem8  46524  stirlinglem10  46526  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  dirker2re  46535  dirkerdenne0  46536  dirkerper  46539  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkeritg  46545  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem26  46576  fourierdlem30  46580  fourierdlem39  46589  fourierdlem42  46592  fourierdlem47  46596  fourierdlem48  46597  fourierdlem56  46605  fourierdlem57  46606  fourierdlem58  46607  fourierdlem62  46611  fourierdlem65  46614  fourierdlem66  46615  fourierdlem68  46617  fourierdlem72  46621  fourierdlem73  46622  fourierdlem76  46625  fourierdlem80  46629  fourierdlem83  46632  fourierdlem85  46634  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem95  46644  fourierdlem97  46646  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  elaa2lem  46676  etransclem8  46685  etransclem18  46695  etransclem20  46697  etransclem21  46698  etransclem23  46700  etransclem24  46701  etransclem31  46708  etransclem33  46710  etransclem35  46712  etransclem45  46722  etransclem46  46723  etransclem47  46724  etransclem48  46725  hoicvrrex  46999  hoidmvlelem2  47039  smfmullem1  47234  sigarim  47294  sigarac  47295  sigaraf  47296  sigarmf  47297  sigarls  47300  sigardiv  47304  sigarcol  47307  cevathlem1  47310  sin3t  47334  cos3t  47335  sin5tlem1  47336  sin5tlem2  47337  sin5tlem3  47338  sin5tlem4  47339  sin5tlem5  47340  sin5t  47341  cos5t  47342  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