Theorem mulcld 10979

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   · cmul 10860

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

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

This theorem is referenced by:  mul02lem1  11134  addid1  11138  cnegex  11139  kcnktkm1cn  11389  subaddmulsub  11421  mulsubaddmulsub  11422  receu  11603  divrec  11632  divcan3  11642  muldivdir  11651  subdivcomb1  11653  subdivcomb2  11654  divdivdiv  11659  divsubdiv  11674  lineq  11795  cru  11948  mul2lt0rlt0  12814  lincmb01cmp  13209  iccf1o  13210  flpmodeq  13575  moddiffl  13583  modvalp1  13591  modcyc  13607  modadd1  13609  modmuladdnn0  13616  modmul1  13625  modaddmulmod  13639  mulexpz  13804  expmulz  13810  binom3  13920  bernneq  13925  mulsubdivbinom2  13957  muldivbinom2  13958  remullem  14820  cjreim2  14853  absimle  15002  abstri  15023  sqreulem  15052  sqreu  15053  bhmafibid1cn  15156  bhmafibid2cn  15157  bhmafibid1  15158  bhmafibid2  15159  mulcn2  15286  reccn2  15287  o1rlimmul  15309  rlimmul  15336  isummulc2  15455  fsummulc2  15477  fsumparts  15499  binomlem  15522  binom1dif  15526  incexclem  15529  incexc  15530  incexc2  15531  pwdif  15561  geomulcvg  15569  mertenslem1  15577  mertens  15579  fprodmul  15651  fprodn0f  15682  iprodmul  15694  binomfallfaclem1  15730  binomfallfaclem2  15731  binomrisefac  15733  bpolycl  15743  bpolysum  15744  bpolydiflem  15745  bpoly4  15750  efaddlem  15783  sinadd  15854  cosadd  15855  tanaddlem  15856  tanadd  15857  addsin  15860  sincossq  15866  sin2t  15867  dvds2ln  15979  oddm1even  16033  pwp1fsum  16081  flodddiv4  16103  sadadd2lem2  16138  bezoutlem2  16229  bezoutlem3  16230  bezoutlem4  16231  lcmgcdlem  16292  phiprmpw  16458  pythagtriplem12  16508  pythagtriplem14  16510  pythagtriplem16  16512  pcpremul  16525  pcaddlem  16570  fldivp1  16579  mul4sqlem  16635  4sqlem14  16640  vdwapun  16656  vdwlem2  16664  vdwlem6  16668  ablsimpgfindlem1  19691  zringlpirlem3  20667  znunit  20752  blcvx  23942  icopnfcnv  24086  cphipipcj  24345  cphipval2  24386  4cphipval2  24387  cphipval  24388  mbfmulc2re  24793  mbfmulc2  24808  itg1addlem4  24844  itg1addlem4OLD  24845  itg1addlem5  24846  itg1mulc  24850  mbfmul  24872  itgcl  24929  itgcnlem  24935  iblmulc2  24976  itgmulc2  24979  itgabs  24980  itgsplit  24981  dvmulbr  25084  dvcmul  25089  dvcmulf  25090  dvexp  25098  dvmptcmul  25109  dvmptdiv  25119  dvexp3  25123  dvsincos  25126  cmvth  25136  dvlipcn  25139  dvfsumabs  25168  dvfsumlem1  25171  ftc1lem4  25184  itgparts  25192  itgpowd  25195  plyf  25340  ply1termlem  25345  plyeq0lem  25352  plypf1  25354  plyaddlem1  25355  plymullem1  25356  coeeulem  25366  coeidlem  25379  coeid3  25382  plyco  25383  coemullem  25392  coemulhi  25396  coemulc  25397  dgrcolem2  25416  plycjlem  25418  plyrecj  25421  dvply1  25425  vieta1lem2  25452  vieta1  25453  elqaalem3  25462  aareccl  25467  aalioulem1  25473  taylfvallem1  25497  tayl0  25502  dvtaylp  25510  taylthlem2  25514  psergf  25552  radcnvlem1  25553  dvradcnv  25561  psercn2  25563  pserdvlem2  25568  pserdv2  25570  abelthlem4  25574  abelthlem5  25575  abelthlem6  25576  abelthlem7  25578  abelthlem9  25580  tanregt0  25676  efgh  25678  efabl  25687  efsubm  25688  cosargd  25744  abslogle  25754  tanarg  25755  advlogexp  25791  logtayllem  25795  logtayl  25796  cxpadd  25815  mulcxp  25821  cxpmul  25824  cxpmul2  25825  cxpmul2z  25827  abscxp  25828  abscxp2  25829  dvcxp2  25875  abscxpbnd  25887  root1eq1  25889  cxpeq  25891  angcan  25933  pythag  25948  ssscongptld  25953  affineequiv  25954  affineequiv2  25955  affineequiv3  25956  affineequiv4  25957  chordthmlem2  25964  chordthmlem3  25965  chordthmlem4  25966  chordthmlem5  25967  heron  25969  quad2  25970  quad  25971  dcubic1lem  25974  dcubic2  25975  dcubic1  25976  dcubic  25977  mcubic  25978  cubic2  25979  cubic  25980  binom4  25981  dquartlem1  25982  dquartlem2  25983  dquart  25984  quart1cl  25985  quart1lem  25986  quart1  25987  quartlem1  25988  quartlem2  25989  atantayl3  26070  leibpi  26073  birthdaylem2  26083  divsqrtsumo1  26114  cvxcl  26115  jensenlem2  26118  lgamgulmlem2  26160  lgamgulmlem3  26161  lgamgulmlem4  26162  lgamgulmlem5  26163  lgamgulmlem6  26164  lgamgulm2  26166  lgamcvg2  26185  gamcvg  26186  gamcvg2lem  26189  wilthlem2  26199  ftalem1  26203  ftalem2  26204  ftalem4  26206  ftalem5  26207  basellem2  26212  basellem3  26213  basellem8  26218  muinv  26323  fsumdvdsmul  26325  logfacrlim  26353  logexprlim  26354  perfectlem2  26359  bposlem9  26421  gausslemma2dlem4  26498  lgsquad2lem1  26513  2lgslem3b  26526  2lgslem3c  26527  2lgslem3d  26528  2sqlem3  26549  2sqmod  26565  rplogsumlem1  26613  dchrisumlem2  26619  dchrisumlem3  26620  dchrmusum2  26623  dchrvmasumlem1  26624  dchrvmasum2lem  26625  dchrvmasum2if  26626  dchrvmasumlem3  26628  dchrvmasumiflem1  26630  dchrvmasumiflem2  26631  rpvmasum2  26641  dchrisum0lem1  26645  dchrisum0lem2a  26646  dchrisum0lem2  26647  dchrmusumlem  26651  dchrvmasumlem  26652  rplogsum  26656  mudivsum  26659  mulogsumlem  26660  mulogsum  26661  mulog2sumlem1  26663  mulog2sumlem2  26664  mulog2sumlem3  26665  vmalogdivsum  26668  logsqvma  26671  log2sumbnd  26673  selberglem1  26674  selberglem2  26675  selberglem3  26676  selberg  26677  selberg2lem  26679  selberg2  26680  selberg3lem1  26686  selberg3  26688  selberg4lem1  26689  selberg4  26690  pntrsumo1  26694  selbergr  26697  selberg3r  26698  selberg4r  26699  selberg34r  26700  pntsval2  26705  pntrlog2bndlem1  26706  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  pntrlog2bndlem6  26712  pntrlog2bnd  26713  pntlemb  26726  pntlemf  26734  pntlemo  26736  ostth2lem2  26763  ostth2lem3  26764  ttgcontlem1  27233  brbtwn2  27254  colinearalg  27259  ax5seglem2  27278  ax5seglem9  27286  axeuclidlem  27311  axcontlem2  27314  axcontlem4  27316  axcontlem7  27319  axcontlem8  27320  finsumvtxdg2ssteplem4  27896  ex-ind-dvds  28804  ipval2  29048  dipcl  29053  riesz3i  30403  dpfrac1  31145  wrdt2ind  31204  ccfldsrarelvec  31720  ccfldextdgrr  31721  cnre2csqima  31840  rmulccn  31857  indsum  31968  indsumin  31969  dya2icoseg  32223  oddpwdc  32300  eulerpartlems  32306  eulerpartlemsv3  32307  eulerpartlemgs2  32326  signsplypnf  32508  itgexpif  32565  breprexplemc  32591  breprexp  32592  vtscl  32597  vtsprod  32598  circlemeth  32599  logdivsqrle  32609  hgt750lemf  32612  hgt750leme  32617  subfacval2  33128  subfaclim  33129  resconn  33187  iprodgam  33687  fwddifnp1  34446  knoppndvlem2  34672  knoppndvlem7  34677  knoppndvlem9  34679  knoppndvlem11  34681  knoppndvlem14  34684  knoppndvlem16  34686  knoppndvlem17  34687  bj-subcom  35458  bj-bary1lem  35460  bj-bary1lem1  35461  bj-bary1  35462  iblmulc2nc  35821  itgmulc2nc  35824  itgabsnc  35825  ftc1cnnclem  35827  ftc1anclem3  35831  dvasin  35840  areacirclem1  35844  areacirclem4  35847  areacirc  35849  cntotbnd  35933  3factsumint1  40009  3factsumint3  40011  3factsumint4  40012  lcmineqlem2  40018  lcmineqlem6  40022  lcmineqlem8  40024  lcmineqlem10  40026  lcmineqlem11  40027  lcmineqlem12  40028  lcmineqlem16  40032  lcmineqlem18  40034  lcmineqlem23  40039  3lexlogpow5ineq5  40048  aks4d1p1p1  40051  dvrelogpow2b  40056  aks4d1p1p6  40061  aks4d1p1p7  40062  aks4d1p1p5  40063  2np3bcnp1  40080  2ap1caineq  40081  sn-addid2  40367  sn-it0e0  40377  sn-negex12  40378  sn-mul01  40387  sn-mulid2  40397  sn-0tie0  40401  sn-mul02  40402  cnreeu  40418  fltnltalem  40479  fltnlta  40480  cu3addd  40482  3cubeslem2  40487  3cubeslem3l  40488  3cubeslem3r  40489  3cubeslem4  40491  pellexlem1  40631  pellexlem2  40632  pellexlem6  40636  pell1234qrne0  40655  pell1234qrreccl  40656  pell1234qrmulcl  40657  pell1234qrdich  40663  pell14qrdich  40671  pell1qrge1  40672  pell1qrgaplem  40675  rmspecsqrtnq  40708  qirropth  40710  rmxyneg  40722  rmxyadd  40723  rmxm1  40736  rmym1  40737  rmxluc  40738  rmyluc  40739  rmxdbl  40741  rmydbl  40742  jm2.18  40790  jm2.19lem1  40791  jm2.19lem2  40792  jm2.19lem4  40794  jm2.19  40795  jm2.22  40797  jm2.23  40798  jm2.25  40801  jm2.27c  40809  jm3.1lem2  40820  flcidc  40979  areaquad  41027  sqrtcval  41202  inductionexd  41718  imo72b2lem0  41729  int-leftdistd  41743  radcnvrat  41885  expgrowth  41906  binomcxplemwb  41919  binomcxplemnn0  41920  binomcxplemfrat  41922  binomcxplemdvbinom  41924  binomcxplemnotnn0  41927  sineq0ALT  42510  mul13d  42771  fperiodmullem  42796  fperiodmul  42797  divcan8d  42805  dmmcand  42806  ltdiv23neg  42888  mulc1cncfg  43084  mccllem  43092  clim1fr1  43096  mullimc  43111  mullimcf  43118  sumnnodd  43125  reclimc  43148  sinmulcos  43360  coskpi2  43361  cosknegpi  43364  dvsinexp  43406  dvasinbx  43415  dvdivf  43417  dvdivbd  43418  dvdivcncf  43422  dvbdfbdioolem2  43424  dvxpaek  43435  dvnxpaek  43437  dvnmul  43438  dvmptfprodlem  43439  dvnprodlem2  43442  itgsinexplem1  43449  itgsinexp  43450  itgcoscmulx  43464  itgsincmulx  43469  itgiccshift  43475  itgperiod  43476  stoweidlem1  43496  stoweidlem11  43506  stoweidlem13  43508  stoweidlem14  43509  stoweidlem17  43512  stoweidlem25  43520  stoweidlem26  43521  stoweidlem42  43537  wallispilem4  43563  wallispilem5  43564  wallispi  43565  wallispi2lem1  43566  wallispi2lem2  43567  wallispi2  43568  stirlinglem1  43569  stirlinglem3  43571  stirlinglem4  43572  stirlinglem5  43573  stirlinglem6  43574  stirlinglem7  43575  stirlinglem8  43576  stirlinglem10  43578  stirlinglem11  43579  stirlinglem12  43580  stirlinglem13  43581  stirlinglem14  43582  stirlinglem15  43583  dirker2re  43587  dirkerdenne0  43588  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkertrigeqlem3  43595  dirkertrigeq  43596  dirkeritg  43597  dirkercncflem2  43599  dirkercncflem4  43601  fourierdlem26  43628  fourierdlem30  43632  fourierdlem39  43641  fourierdlem42  43644  fourierdlem47  43648  fourierdlem48  43649  fourierdlem56  43657  fourierdlem57  43658  fourierdlem58  43659  fourierdlem62  43663  fourierdlem65  43666  fourierdlem66  43667  fourierdlem68  43669  fourierdlem72  43673  fourierdlem73  43674  fourierdlem76  43677  fourierdlem80  43681  fourierdlem83  43684  fourierdlem85  43686  fourierdlem89  43690  fourierdlem90  43691  fourierdlem91  43692  fourierdlem95  43696  fourierdlem97  43698  fourierdlem101  43702  fourierdlem103  43704  fourierdlem104  43705  fourierdlem111  43712  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  fouriersw  43726  elaa2lem  43728  etransclem8  43737  etransclem18  43747  etransclem20  43749  etransclem21  43750  etransclem23  43752  etransclem24  43753  etransclem31  43760  etransclem33  43762  etransclem35  43764  etransclem45  43774  etransclem46  43775  etransclem47  43776  etransclem48  43777  hoicvrrex  44048  hoidmvlelem2  44088  smfmullem1  44276  sigarim  44318  sigarac  44319  sigaraf  44320  sigarmf  44321  sigarls  44324  sigardiv  44328  sigarcol  44331  cevathlem1  44334  fmtnorec2lem  44946  fmtnorec3  44952  fmtnorec4  44953  fmtnoprmfac1  44969  fmtnoprmfac2  44971  fmtnofac2lem  44972  sfprmdvdsmersenne  45007  lighneallem3  45011  quad1  45024  requad01  45025  requad2  45027  opeoALTV  45088  perfectALTVlem2  45126  fppr2odd  45135  0nodd  45316  2nodd  45318  2zlidl  45444  2zrngnmlid  45459  altgsumbcALT  45641  fldivmod  45816  nn0sumshdiglemA  45917  nn0sumshdiglemB  45918  nn0sumshdiglem2  45920  nn0mullong  45923  itcovalt2lem2lem2  45972  ackval2  45980  submuladdmuld  45999  affinecomb2  46001  affineid  46002  1subrec1sub  46003  eenglngeehlnmlem1  46035  eenglngeehlnmlem2  46036  rrx2linest  46040  line2x  46052  line2y  46053  itschlc0yqe  46058  itsclc0yqsollem1  46060  itsclc0yqsol  46062  itscnhlc0xyqsol  46063  itschlc0xyqsol1  46064  itschlc0xyqsol  46065  itsclc0xyqsolr  46067  2itscplem1  46076  2itscplem2  46077  2itscplem3  46078  2itscp  46079  itscnhlinecirc02plem1  46080  itscnhlinecirc02plem2  46081  inlinecirc02plem  46084  inlinecirc02p  46085  i2linesd  46435  aacllem  46457  amgmwlem  46458  amgmlemALT  46459