Theorem mulcld 11234

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

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

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

This theorem is referenced by:  mul02lem1  11390  addrid  11394  cnegex  11395  kcnktkm1cn  11645  subaddmulsub  11677  mulsubaddmulsub  11678  receu  11859  divrec  11888  divcan3  11898  muldivdir  11907  subdivcomb1  11909  subdivcomb2  11910  divdivdiv  11915  divsubdiv  11930  lineq  12051  cru  12204  mul2lt0rlt0  13076  lincmb01cmp  13472  iccf1o  13473  flpmodeq  13839  moddiffl  13847  modvalp1  13855  modcyc  13871  modadd1  13873  modmuladdnn0  13880  modmul1  13889  modaddmulmod  13903  mulexpz  14068  expmulz  14074  binom3  14187  bernneq  14192  mulsubdivbinom2  14222  muldivbinom2  14223  remullem  15075  cjreim2  15108  absimle  15256  abstri  15277  sqreulem  15306  sqreu  15307  bhmafibid1cn  15410  bhmafibid2cn  15411  bhmafibid1  15412  bhmafibid2  15413  mulcn2  15540  reccn2  15541  o1rlimmul  15563  rlimmul  15590  isummulc2  15708  fsummulc2  15730  fsumparts  15752  binomlem  15775  binom1dif  15779  incexclem  15782  incexc  15783  incexc2  15784  pwdif  15814  geomulcvg  15822  mertenslem1  15830  mertens  15832  fprodmul  15904  fprodn0f  15935  iprodmul  15947  binomfallfaclem1  15983  binomfallfaclem2  15984  binomrisefac  15986  bpolycl  15996  bpolysum  15997  bpolydiflem  15998  bpoly4  16003  efaddlem  16036  sinadd  16107  cosadd  16108  tanaddlem  16109  tanadd  16110  addsin  16113  sincossq  16119  sin2t  16120  dvds2ln  16232  oddm1even  16286  pwp1fsum  16334  flodddiv4  16356  sadadd2lem2  16391  bezoutlem2  16482  bezoutlem3  16483  bezoutlem4  16484  lcmgcdlem  16543  phiprmpw  16709  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  pcpremul  16776  pcaddlem  16821  fldivp1  16830  mul4sqlem  16886  4sqlem14  16891  vdwapun  16907  vdwlem2  16915  vdwlem6  16919  ablsimpgfindlem1  19977  zringlpirlem3  21034  znunit  21119  blcvx  24314  icopnfcnv  24458  cphipipcj  24717  cphipval2  24758  4cphipval2  24759  cphipval  24760  mbfmulc2re  25165  mbfmulc2  25180  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  itg1mulc  25222  mbfmul  25244  itgcl  25301  itgcnlem  25307  iblmulc2  25348  itgmulc2  25351  itgabs  25352  itgsplit  25353  dvmulbr  25456  dvcmul  25461  dvcmulf  25462  dvexp  25470  dvmptcmul  25481  dvmptdiv  25491  dvexp3  25495  dvsincos  25498  cmvth  25508  dvlipcn  25511  dvfsumabs  25540  dvfsumlem1  25543  ftc1lem4  25556  itgparts  25564  itgpowd  25567  plyf  25712  ply1termlem  25717  plyeq0lem  25724  plypf1  25726  plyaddlem1  25727  plymullem1  25728  coeeulem  25738  coeidlem  25751  coeid3  25754  plyco  25755  coemullem  25764  coemulhi  25768  coemulc  25769  dgrcolem2  25788  plycjlem  25790  plyrecj  25793  dvply1  25797  vieta1lem2  25824  vieta1  25825  elqaalem3  25834  aareccl  25839  aalioulem1  25845  taylfvallem1  25869  tayl0  25874  dvtaylp  25882  taylthlem2  25886  psergf  25924  radcnvlem1  25925  dvradcnv  25933  psercn2  25935  pserdvlem2  25940  pserdv2  25942  abelthlem4  25946  abelthlem5  25947  abelthlem6  25948  abelthlem7  25950  abelthlem9  25952  tanregt0  26048  efgh  26050  efabl  26059  efsubm  26060  cosargd  26116  abslogle  26126  tanarg  26127  advlogexp  26163  logtayllem  26167  logtayl  26168  cxpadd  26187  mulcxp  26193  cxpmul  26196  cxpmul2  26197  cxpmul2z  26199  abscxp  26200  abscxp2  26201  dvcxp2  26249  abscxpbnd  26261  root1eq1  26263  cxpeq  26265  angcan  26307  pythag  26322  ssscongptld  26327  affineequiv  26328  affineequiv2  26329  affineequiv3  26330  affineequiv4  26331  chordthmlem2  26338  chordthmlem3  26339  chordthmlem4  26340  chordthmlem5  26341  heron  26343  quad2  26344  quad  26345  dcubic1lem  26348  dcubic2  26349  dcubic1  26350  dcubic  26351  mcubic  26352  cubic2  26353  cubic  26354  binom4  26355  dquartlem1  26356  dquartlem2  26357  dquart  26358  quart1cl  26359  quart1lem  26360  quart1  26361  quartlem1  26362  quartlem2  26363  atantayl3  26444  leibpi  26447  birthdaylem2  26457  divsqrtsumo1  26488  cvxcl  26489  jensenlem2  26492  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamgulm2  26540  lgamcvg2  26559  gamcvg  26560  gamcvg2lem  26563  wilthlem2  26573  ftalem1  26577  ftalem2  26578  ftalem4  26580  ftalem5  26581  basellem2  26586  basellem3  26587  basellem8  26592  muinv  26697  fsumdvdsmul  26699  logfacrlim  26727  logexprlim  26728  perfectlem2  26733  bposlem9  26795  gausslemma2dlem4  26872  lgsquad2lem1  26887  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2sqlem3  26923  2sqmod  26939  rplogsumlem1  26987  dchrisumlem2  26993  dchrisumlem3  26994  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrvmasum2if  27000  dchrvmasumlem3  27002  dchrvmasumiflem1  27004  dchrvmasumiflem2  27005  rpvmasum2  27015  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrmusumlem  27025  dchrvmasumlem  27026  rplogsum  27030  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  mulog2sumlem1  27037  mulog2sumlem2  27038  mulog2sumlem3  27039  vmalogdivsum  27042  logsqvma  27045  log2sumbnd  27047  selberglem1  27048  selberglem2  27049  selberglem3  27050  selberg  27051  selberg2lem  27053  selberg2  27054  selberg3lem1  27060  selberg3  27062  selberg4lem1  27063  selberg4  27064  pntrsumo1  27068  selbergr  27071  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntsval2  27079  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntlemb  27100  pntlemf  27108  pntlemo  27110  ostth2lem2  27137  ostth2lem3  27138  ttgcontlem1  28173  brbtwn2  28194  colinearalg  28199  ax5seglem2  28218  ax5seglem9  28226  axeuclidlem  28251  axcontlem2  28254  axcontlem4  28256  axcontlem7  28259  axcontlem8  28260  finsumvtxdg2ssteplem4  28836  ex-ind-dvds  29745  nrt2irr  29757  ipval2  29991  dipcl  29996  riesz3i  31346  dpfrac1  32089  wrdt2ind  32148  ccfldsrarelvec  32776  ccfldextdgrr  32777  cnre2csqima  32922  rmulccn  32939  indsum  33050  indsumin  33051  dya2icoseg  33307  oddpwdc  33384  eulerpartlems  33390  eulerpartlemsv3  33391  eulerpartlemgs2  33410  signsplypnf  33592  itgexpif  33649  breprexplemc  33675  breprexp  33676  vtscl  33681  vtsprod  33682  circlemeth  33683  logdivsqrle  33693  hgt750lemf  33696  hgt750leme  33701  subfacval2  34209  subfaclim  34210  resconn  34268  iprodgam  34743  fwddifnp1  35168  gg-dvmulbr  35206  gg-psercn2  35209  gg-rmulccn  35210  gg-cmvth  35212  gg-cncrng  35231  knoppndvlem2  35437  knoppndvlem7  35442  knoppndvlem9  35444  knoppndvlem11  35446  knoppndvlem14  35449  knoppndvlem16  35451  knoppndvlem17  35452  bj-subcom  36237  bj-bary1lem  36239  bj-bary1lem1  36240  bj-bary1  36241  iblmulc2nc  36601  itgmulc2nc  36604  itgabsnc  36605  ftc1cnnclem  36607  ftc1anclem3  36611  dvasin  36620  areacirclem1  36624  areacirclem4  36627  areacirc  36629  cntotbnd  36712  3factsumint1  40934  3factsumint3  40936  3factsumint4  40937  lcmineqlem2  40943  lcmineqlem6  40947  lcmineqlem8  40949  lcmineqlem10  40951  lcmineqlem11  40952  lcmineqlem12  40953  lcmineqlem16  40957  lcmineqlem18  40959  lcmineqlem23  40964  3lexlogpow5ineq5  40973  aks4d1p1p1  40976  dvrelogpow2b  40981  aks4d1p1p6  40986  aks4d1p1p7  40987  aks4d1p1p5  40988  2np3bcnp1  41008  2ap1caineq  41009  oddnumth  41257  nicomachus  41258  sumcubes  41259  sn-addlid  41325  sn-it0e0  41336  sn-negex12  41337  sn-mul01  41346  sn-mullid  41356  sn-0tie0  41360  sn-mul02  41361  cnreeu  41389  fltnltalem  41452  fltnlta  41453  cu3addd  41466  3cubeslem2  41471  3cubeslem3l  41472  3cubeslem3r  41473  3cubeslem4  41475  pellexlem1  41615  pellexlem2  41616  pellexlem6  41620  pell1234qrne0  41639  pell1234qrreccl  41640  pell1234qrmulcl  41641  pell1234qrdich  41647  pell14qrdich  41655  pell1qrge1  41656  pell1qrgaplem  41659  rmspecsqrtnq  41692  qirropth  41694  rmxyneg  41707  rmxyadd  41708  rmxm1  41721  rmym1  41722  rmxluc  41723  rmyluc  41724  rmxdbl  41726  rmydbl  41727  jm2.18  41775  jm2.19lem1  41776  jm2.19lem2  41777  jm2.19lem4  41779  jm2.19  41780  jm2.22  41782  jm2.23  41783  jm2.25  41786  jm2.27c  41794  jm3.1lem2  41805  flcidc  41964  areaquad  42013  sqrtcval  42440  inductionexd  42954  imo72b2lem0  42965  int-leftdistd  42979  radcnvrat  43121  expgrowth  43142  binomcxplemwb  43155  binomcxplemnn0  43156  binomcxplemfrat  43158  binomcxplemdvbinom  43160  binomcxplemnotnn0  43163  sineq0ALT  43746  mul13d  44037  fperiodmullem  44061  fperiodmul  44062  divcan8d  44070  dmmcand  44071  ltdiv23neg  44152  mulc1cncfg  44353  mccllem  44361  clim1fr1  44365  mullimc  44380  mullimcf  44387  sumnnodd  44394  reclimc  44417  sinmulcos  44629  coskpi2  44630  cosknegpi  44633  dvsinexp  44675  dvasinbx  44684  dvdivf  44686  dvdivbd  44687  dvdivcncf  44691  dvbdfbdioolem2  44693  dvxpaek  44704  dvnxpaek  44706  dvnmul  44707  dvmptfprodlem  44708  dvnprodlem2  44711  itgsinexplem1  44718  itgsinexp  44719  itgcoscmulx  44733  itgsincmulx  44738  itgiccshift  44744  itgperiod  44745  stoweidlem1  44765  stoweidlem11  44775  stoweidlem13  44777  stoweidlem14  44778  stoweidlem17  44781  stoweidlem25  44789  stoweidlem26  44790  stoweidlem42  44806  wallispilem4  44832  wallispilem5  44833  wallispi  44834  wallispi2lem1  44835  wallispi2lem2  44836  wallispi2  44837  stirlinglem1  44838  stirlinglem3  44840  stirlinglem4  44841  stirlinglem5  44842  stirlinglem6  44843  stirlinglem7  44844  stirlinglem8  44845  stirlinglem10  44847  stirlinglem11  44848  stirlinglem12  44849  stirlinglem13  44850  stirlinglem14  44851  stirlinglem15  44852  dirker2re  44856  dirkerdenne0  44857  dirkerper  44860  dirkertrigeqlem1  44862  dirkertrigeqlem2  44863  dirkertrigeqlem3  44864  dirkertrigeq  44865  dirkeritg  44866  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem26  44897  fourierdlem30  44901  fourierdlem39  44910  fourierdlem42  44913  fourierdlem47  44917  fourierdlem48  44918  fourierdlem56  44926  fourierdlem57  44927  fourierdlem58  44928  fourierdlem62  44932  fourierdlem65  44935  fourierdlem66  44936  fourierdlem68  44938  fourierdlem72  44942  fourierdlem73  44943  fourierdlem76  44946  fourierdlem80  44950  fourierdlem83  44953  fourierdlem85  44955  fourierdlem89  44959  fourierdlem90  44960  fourierdlem91  44961  fourierdlem95  44965  fourierdlem97  44967  fourierdlem101  44971  fourierdlem103  44973  fourierdlem104  44974  fourierdlem111  44981  sqwvfoura  44992  sqwvfourb  44993  fourierswlem  44994  fouriersw  44995  elaa2lem  44997  etransclem8  45006  etransclem18  45016  etransclem20  45018  etransclem21  45019  etransclem23  45021  etransclem24  45022  etransclem31  45029  etransclem33  45031  etransclem35  45033  etransclem45  45043  etransclem46  45044  etransclem47  45045  etransclem48  45046  hoicvrrex  45320  hoidmvlelem2  45360  smfmullem1  45555  sigarim  45615  sigarac  45616  sigaraf  45617  sigarmf  45618  sigarls  45621  sigardiv  45625  sigarcol  45628  cevathlem1  45631  fmtnorec2lem  46258  fmtnorec3  46264  fmtnorec4  46265  fmtnoprmfac1  46281  fmtnoprmfac2  46283  fmtnofac2lem  46284  sfprmdvdsmersenne  46319  lighneallem3  46323  quad1  46336  requad01  46337  requad2  46339  opeoALTV  46400  perfectALTVlem2  46438  fppr2odd  46447  0nodd  46628  2nodd  46630  2zlidl  46880  2zrngnmlid  46895  altgsumbcALT  47077  fldivmod  47252  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354  nn0sumshdiglem2  47356  nn0mullong  47359  itcovalt2lem2lem2  47408  ackval2  47416  submuladdmuld  47435  affinecomb2  47437  affineid  47438  1subrec1sub  47439  eenglngeehlnmlem1  47471  eenglngeehlnmlem2  47472  rrx2linest  47476  line2x  47488  line2y  47489  itschlc0yqe  47494  itsclc0yqsollem1  47496  itsclc0yqsol  47498  itscnhlc0xyqsol  47499  itschlc0xyqsol1  47500  itschlc0xyqsol  47501  itsclc0xyqsolr  47503  2itscplem1  47512  2itscplem2  47513  2itscplem3  47514  2itscp  47515  itscnhlinecirc02plem1  47516  itscnhlinecirc02plem2  47517  inlinecirc02plem  47520  inlinecirc02p  47521  i2linesd  47874  aacllem  47896  amgmwlem  47897  amgmlemALT  47898