Theorem mulcld 11004

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

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

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

This theorem is referenced by:  mul02lem1  11160  addid1  11164  cnegex  11165  kcnktkm1cn  11415  subaddmulsub  11447  mulsubaddmulsub  11448  receu  11629  divrec  11658  divcan3  11668  muldivdir  11677  subdivcomb1  11679  subdivcomb2  11680  divdivdiv  11685  divsubdiv  11700  lineq  11821  cru  11974  mul2lt0rlt0  12841  lincmb01cmp  13236  iccf1o  13237  flpmodeq  13603  moddiffl  13611  modvalp1  13619  modcyc  13635  modadd1  13637  modmuladdnn0  13644  modmul1  13653  modaddmulmod  13667  mulexpz  13832  expmulz  13838  binom3  13948  bernneq  13953  mulsubdivbinom2  13985  muldivbinom2  13986  remullem  14848  cjreim2  14881  absimle  15030  abstri  15051  sqreulem  15080  sqreu  15081  bhmafibid1cn  15184  bhmafibid2cn  15185  bhmafibid1  15186  bhmafibid2  15187  mulcn2  15314  reccn2  15315  o1rlimmul  15337  rlimmul  15364  isummulc2  15483  fsummulc2  15505  fsumparts  15527  binomlem  15550  binom1dif  15554  incexclem  15557  incexc  15558  incexc2  15559  pwdif  15589  geomulcvg  15597  mertenslem1  15605  mertens  15607  fprodmul  15679  fprodn0f  15710  iprodmul  15722  binomfallfaclem1  15758  binomfallfaclem2  15759  binomrisefac  15761  bpolycl  15771  bpolysum  15772  bpolydiflem  15773  bpoly4  15778  efaddlem  15811  sinadd  15882  cosadd  15883  tanaddlem  15884  tanadd  15885  addsin  15888  sincossq  15894  sin2t  15895  dvds2ln  16007  oddm1even  16061  pwp1fsum  16109  flodddiv4  16131  sadadd2lem2  16166  bezoutlem2  16257  bezoutlem3  16258  bezoutlem4  16259  lcmgcdlem  16320  phiprmpw  16486  pythagtriplem12  16536  pythagtriplem14  16538  pythagtriplem16  16540  pcpremul  16553  pcaddlem  16598  fldivp1  16607  mul4sqlem  16663  4sqlem14  16668  vdwapun  16684  vdwlem2  16692  vdwlem6  16696  ablsimpgfindlem1  19719  zringlpirlem3  20695  znunit  20780  blcvx  23970  icopnfcnv  24114  cphipipcj  24373  cphipval2  24414  4cphipval2  24415  cphipval  24416  mbfmulc2re  24821  mbfmulc2  24836  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  itg1mulc  24878  mbfmul  24900  itgcl  24957  itgcnlem  24963  iblmulc2  25004  itgmulc2  25007  itgabs  25008  itgsplit  25009  dvmulbr  25112  dvcmul  25117  dvcmulf  25118  dvexp  25126  dvmptcmul  25137  dvmptdiv  25147  dvexp3  25151  dvsincos  25154  cmvth  25164  dvlipcn  25167  dvfsumabs  25196  dvfsumlem1  25199  ftc1lem4  25212  itgparts  25220  itgpowd  25223  plyf  25368  ply1termlem  25373  plyeq0lem  25380  plypf1  25382  plyaddlem1  25383  plymullem1  25384  coeeulem  25394  coeidlem  25407  coeid3  25410  plyco  25411  coemullem  25420  coemulhi  25424  coemulc  25425  dgrcolem2  25444  plycjlem  25446  plyrecj  25449  dvply1  25453  vieta1lem2  25480  vieta1  25481  elqaalem3  25490  aareccl  25495  aalioulem1  25501  taylfvallem1  25525  tayl0  25530  dvtaylp  25538  taylthlem2  25542  psergf  25580  radcnvlem1  25581  dvradcnv  25589  psercn2  25591  pserdvlem2  25596  pserdv2  25598  abelthlem4  25602  abelthlem5  25603  abelthlem6  25604  abelthlem7  25606  abelthlem9  25608  tanregt0  25704  efgh  25706  efabl  25715  efsubm  25716  cosargd  25772  abslogle  25782  tanarg  25783  advlogexp  25819  logtayllem  25823  logtayl  25824  cxpadd  25843  mulcxp  25849  cxpmul  25852  cxpmul2  25853  cxpmul2z  25855  abscxp  25856  abscxp2  25857  dvcxp2  25903  abscxpbnd  25915  root1eq1  25917  cxpeq  25919  angcan  25961  pythag  25976  ssscongptld  25981  affineequiv  25982  affineequiv2  25983  affineequiv3  25984  affineequiv4  25985  chordthmlem2  25992  chordthmlem3  25993  chordthmlem4  25994  chordthmlem5  25995  heron  25997  quad2  25998  quad  25999  dcubic1lem  26002  dcubic2  26003  dcubic1  26004  dcubic  26005  mcubic  26006  cubic2  26007  cubic  26008  binom4  26009  dquartlem1  26010  dquartlem2  26011  dquart  26012  quart1cl  26013  quart1lem  26014  quart1  26015  quartlem1  26016  quartlem2  26017  atantayl3  26098  leibpi  26101  birthdaylem2  26111  divsqrtsumo1  26142  cvxcl  26143  jensenlem2  26146  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem4  26190  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamgulm2  26194  lgamcvg2  26213  gamcvg  26214  gamcvg2lem  26217  wilthlem2  26227  ftalem1  26231  ftalem2  26232  ftalem4  26234  ftalem5  26235  basellem2  26240  basellem3  26241  basellem8  26246  muinv  26351  fsumdvdsmul  26353  logfacrlim  26381  logexprlim  26382  perfectlem2  26387  bposlem9  26449  gausslemma2dlem4  26526  lgsquad2lem1  26541  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2sqlem3  26577  2sqmod  26593  rplogsumlem1  26641  dchrisumlem2  26647  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasum2lem  26653  dchrvmasum2if  26654  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  dchrvmasumiflem2  26659  rpvmasum2  26669  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrmusumlem  26679  dchrvmasumlem  26680  rplogsum  26684  mudivsum  26687  mulogsumlem  26688  mulogsum  26689  mulog2sumlem1  26691  mulog2sumlem2  26692  mulog2sumlem3  26693  vmalogdivsum  26696  logsqvma  26699  log2sumbnd  26701  selberglem1  26702  selberglem2  26703  selberglem3  26704  selberg  26705  selberg2lem  26707  selberg2  26708  selberg3lem1  26714  selberg3  26716  selberg4lem1  26717  selberg4  26718  pntrsumo1  26722  selbergr  26725  selberg3r  26726  selberg4r  26727  selberg34r  26728  pntsval2  26733  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntlemb  26754  pntlemf  26762  pntlemo  26764  ostth2lem2  26791  ostth2lem3  26792  ttgcontlem1  27261  brbtwn2  27282  colinearalg  27287  ax5seglem2  27306  ax5seglem9  27314  axeuclidlem  27339  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  axcontlem8  27348  finsumvtxdg2ssteplem4  27924  ex-ind-dvds  28834  ipval2  29078  dipcl  29083  riesz3i  30433  dpfrac1  31175  wrdt2ind  31234  ccfldsrarelvec  31750  ccfldextdgrr  31751  cnre2csqima  31870  rmulccn  31887  indsum  31998  indsumin  31999  dya2icoseg  32253  oddpwdc  32330  eulerpartlems  32336  eulerpartlemsv3  32337  eulerpartlemgs2  32356  signsplypnf  32538  itgexpif  32595  breprexplemc  32621  breprexp  32622  vtscl  32627  vtsprod  32628  circlemeth  32629  logdivsqrle  32639  hgt750lemf  32642  hgt750leme  32647  subfacval2  33158  subfaclim  33159  resconn  33217  iprodgam  33717  fwddifnp1  34476  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem9  34709  knoppndvlem11  34711  knoppndvlem14  34714  knoppndvlem16  34716  knoppndvlem17  34717  bj-subcom  35488  bj-bary1lem  35490  bj-bary1lem1  35491  bj-bary1  35492  iblmulc2nc  35851  itgmulc2nc  35854  itgabsnc  35855  ftc1cnnclem  35857  ftc1anclem3  35861  dvasin  35870  areacirclem1  35874  areacirclem4  35877  areacirc  35879  cntotbnd  35963  3factsumint1  40036  3factsumint3  40038  3factsumint4  40039  lcmineqlem2  40045  lcmineqlem6  40049  lcmineqlem8  40051  lcmineqlem10  40053  lcmineqlem11  40054  lcmineqlem12  40055  lcmineqlem16  40059  lcmineqlem18  40061  lcmineqlem23  40066  3lexlogpow5ineq5  40075  aks4d1p1p1  40078  dvrelogpow2b  40083  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  2np3bcnp1  40107  2ap1caineq  40108  sn-addid2  40394  sn-it0e0  40404  sn-negex12  40405  sn-mul01  40414  sn-mulid2  40424  sn-0tie0  40428  sn-mul02  40429  cnreeu  40445  fltnltalem  40506  fltnlta  40507  cu3addd  40509  3cubeslem2  40514  3cubeslem3l  40515  3cubeslem3r  40516  3cubeslem4  40518  pellexlem1  40658  pellexlem2  40659  pellexlem6  40663  pell1234qrne0  40682  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell1234qrdich  40690  pell14qrdich  40698  pell1qrge1  40699  pell1qrgaplem  40702  rmspecsqrtnq  40735  qirropth  40737  rmxyneg  40749  rmxyadd  40750  rmxm1  40763  rmym1  40764  rmxluc  40765  rmyluc  40766  rmxdbl  40768  rmydbl  40769  jm2.18  40817  jm2.19lem1  40818  jm2.19lem2  40819  jm2.19lem4  40821  jm2.19  40822  jm2.22  40824  jm2.23  40825  jm2.25  40828  jm2.27c  40836  jm3.1lem2  40847  flcidc  41006  areaquad  41054  sqrtcval  41256  inductionexd  41772  imo72b2lem0  41783  int-leftdistd  41797  radcnvrat  41939  expgrowth  41960  binomcxplemwb  41973  binomcxplemnn0  41974  binomcxplemfrat  41976  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  sineq0ALT  42564  mul13d  42825  fperiodmullem  42849  fperiodmul  42850  divcan8d  42858  dmmcand  42859  ltdiv23neg  42941  mulc1cncfg  43137  mccllem  43145  clim1fr1  43149  mullimc  43164  mullimcf  43171  sumnnodd  43178  reclimc  43201  sinmulcos  43413  coskpi2  43414  cosknegpi  43417  dvsinexp  43459  dvasinbx  43468  dvdivf  43470  dvdivbd  43471  dvdivcncf  43475  dvbdfbdioolem2  43477  dvxpaek  43488  dvnxpaek  43490  dvnmul  43491  dvmptfprodlem  43492  dvnprodlem2  43495  itgsinexplem1  43502  itgsinexp  43503  itgcoscmulx  43517  itgsincmulx  43522  itgiccshift  43528  itgperiod  43529  stoweidlem1  43549  stoweidlem11  43559  stoweidlem13  43561  stoweidlem14  43562  stoweidlem17  43565  stoweidlem25  43573  stoweidlem26  43574  stoweidlem42  43590  wallispilem4  43616  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  dirker2re  43640  dirkerdenne0  43641  dirkerper  43644  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkeritg  43650  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem26  43681  fourierdlem30  43685  fourierdlem39  43694  fourierdlem42  43697  fourierdlem47  43701  fourierdlem48  43702  fourierdlem56  43710  fourierdlem57  43711  fourierdlem58  43712  fourierdlem62  43716  fourierdlem65  43719  fourierdlem66  43720  fourierdlem68  43722  fourierdlem72  43726  fourierdlem73  43727  fourierdlem76  43730  fourierdlem80  43734  fourierdlem83  43737  fourierdlem85  43739  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem95  43749  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  elaa2lem  43781  etransclem8  43790  etransclem18  43800  etransclem20  43802  etransclem21  43803  etransclem23  43805  etransclem24  43806  etransclem31  43813  etransclem33  43815  etransclem35  43817  etransclem45  43827  etransclem46  43828  etransclem47  43829  etransclem48  43830  hoicvrrex  44101  hoidmvlelem2  44141  smfmullem1  44336  sigarim  44378  sigarac  44379  sigaraf  44380  sigarmf  44381  sigarls  44384  sigardiv  44388  sigarcol  44391  cevathlem1  44394  fmtnorec2lem  45005  fmtnorec3  45011  fmtnorec4  45012  fmtnoprmfac1  45028  fmtnoprmfac2  45030  fmtnofac2lem  45031  sfprmdvdsmersenne  45066  lighneallem3  45070  quad1  45083  requad01  45084  requad2  45086  opeoALTV  45147  perfectALTVlem2  45185  fppr2odd  45194  0nodd  45375  2nodd  45377  2zlidl  45503  2zrngnmlid  45518  altgsumbcALT  45700  fldivmod  45875  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdiglem2  45979  nn0mullong  45982  itcovalt2lem2lem2  46031  ackval2  46039  submuladdmuld  46058  affinecomb2  46060  affineid  46061  1subrec1sub  46062  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2linest  46099  line2x  46111  line2y  46112  itschlc0yqe  46117  itsclc0yqsollem1  46119  itsclc0yqsol  46121  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  itschlc0xyqsol  46124  itsclc0xyqsolr  46126  2itscplem1  46135  2itscplem2  46136  2itscplem3  46137  2itscp  46138  itscnhlinecirc02plem1  46139  itscnhlinecirc02plem2  46140  inlinecirc02plem  46143  inlinecirc02p  46144  i2linesd  46494  aacllem  46516  amgmwlem  46517  amgmlemALT  46518