Theorem mulcld 11263

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7413  ℂcc 11135   · cmul 11142

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

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

This theorem is referenced by:  mul02lem1  11419  addrid  11423  cnegex  11424  kcnktkm1cn  11676  subaddmulsub  11708  mulsubaddmulsub  11709  receu  11890  divrec  11920  divcan3  11930  muldivdir  11942  subdivcomb1  11944  subdivcomb2  11945  divdivdiv  11950  divsubdiv  11965  lineq  12086  cru  12240  mul2lt0rlt0  13119  lincmb01cmp  13517  iccf1o  13518  flpmodeq  13896  moddiffl  13904  modvalp1  13912  modcyc  13928  modadd1  13930  modmuladdnn0  13938  modmul1  13947  modaddmulmod  13961  mulexpz  14125  expmulz  14131  binom3  14245  bernneq  14250  mulsubdivbinom2  14283  muldivbinom2  14284  remullem  15149  cjreim2  15182  absimle  15330  abstri  15351  sqreulem  15380  sqreu  15381  bhmafibid1cn  15484  bhmafibid2cn  15485  bhmafibid1  15486  bhmafibid2  15487  mulcn2  15614  reccn2  15615  o1rlimmul  15637  rlimmul  15663  isummulc2  15780  fsummulc2  15802  fsumparts  15824  binomlem  15847  binom1dif  15851  incexclem  15854  incexc  15855  incexc2  15856  pwdif  15886  geomulcvg  15894  mertenslem1  15902  mertens  15904  fprodmul  15978  fprodn0f  16009  iprodmul  16021  binomfallfaclem1  16057  binomfallfaclem2  16058  binomrisefac  16060  bpolycl  16070  bpolysum  16071  bpolydiflem  16072  bpoly4  16077  efaddlem  16111  sinadd  16182  cosadd  16183  tanaddlem  16184  tanadd  16185  addsin  16188  sincossq  16194  sin2t  16195  dvds2ln  16308  oddm1even  16362  pwp1fsum  16410  flodddiv4  16434  sadadd2lem2  16469  bezoutlem2  16559  bezoutlem3  16560  bezoutlem4  16561  lcmgcdlem  16625  phiprmpw  16795  pythagtriplem12  16846  pythagtriplem14  16848  pythagtriplem16  16850  pcpremul  16863  pcaddlem  16908  fldivp1  16917  mul4sqlem  16973  4sqlem14  16978  vdwapun  16994  vdwlem2  17002  vdwlem6  17006  ablsimpgfindlem1  20095  zringlpirlem3  21437  znunit  21536  blcvx  24755  icopnfcnv  24909  cphipipcj  25170  cphipval2  25211  4cphipval2  25212  cphipval  25213  mbfmulc2re  25619  mbfmulc2  25634  itg1addlem4  25670  itg1addlem5  25671  itg1mulc  25675  mbfmul  25697  itgcl  25755  itgcnlem  25761  iblmulc2  25802  itgmulc2  25805  itgabs  25806  itgsplit  25807  dvmulbr  25911  dvmulbrOLD  25912  dvcmul  25917  dvcmulf  25918  dvexp  25927  dvmptcmul  25938  dvmptdiv  25948  dvexp3  25952  dvsincos  25955  cmvth  25965  cmvthOLD  25966  dvlipcn  25969  dvfsumabs  25999  dvfsumlem1  26002  ftc1lem4  26016  itgparts  26024  itgpowd  26027  plyf  26173  ply1termlem  26178  plyeq0lem  26185  plypf1  26187  plyaddlem1  26188  plymullem1  26189  coeeulem  26199  coeidlem  26212  coeid3  26215  plyco  26216  coemullem  26225  coemulhi  26229  coemulc  26230  dgrcolem2  26250  plycjlem  26252  plyrecj  26257  dvply1  26261  vieta1lem2  26289  vieta1  26290  elqaalem3  26299  aareccl  26304  aalioulem1  26310  taylfvallem1  26334  tayl0  26339  dvtaylp  26348  taylthlem2  26352  taylthlem2OLD  26353  psergf  26391  radcnvlem1  26392  dvradcnv  26400  psercn2  26402  psercn2OLD  26403  pserdvlem2  26408  pserdv2  26410  abelthlem4  26414  abelthlem5  26415  abelthlem6  26416  abelthlem7  26418  abelthlem9  26420  tanregt0  26517  efgh  26519  efabl  26528  efsubm  26529  cosargd  26586  abslogle  26596  tanarg  26597  advlogexp  26633  logtayllem  26637  logtayl  26638  cxpadd  26657  mulcxp  26663  cxpmul  26666  cxpmul2  26667  cxpmul2z  26669  abscxp  26670  abscxp2  26671  dvcxp2  26719  abscxpbnd  26732  root1eq1  26734  cxpeq  26736  angcan  26781  pythag  26796  ssscongptld  26801  affineequiv  26802  affineequiv2  26803  affineequiv3  26804  affineequiv4  26805  chordthmlem2  26812  chordthmlem3  26813  chordthmlem4  26814  chordthmlem5  26815  heron  26817  quad2  26818  quad  26819  dcubic1lem  26822  dcubic2  26823  dcubic1  26824  dcubic  26825  mcubic  26826  cubic2  26827  cubic  26828  binom4  26829  dquartlem1  26830  dquartlem2  26831  dquart  26832  quart1cl  26833  quart1lem  26834  quart1  26835  quartlem1  26836  quartlem2  26837  atantayl3  26918  leibpi  26921  birthdaylem2  26931  divsqrtsumo1  26963  cvxcl  26964  jensenlem2  26967  lgamgulmlem2  27009  lgamgulmlem3  27010  lgamgulmlem4  27011  lgamgulmlem5  27012  lgamgulmlem6  27013  lgamgulm2  27015  lgamcvg2  27034  gamcvg  27035  gamcvg2lem  27038  wilthlem2  27048  ftalem1  27052  ftalem2  27053  ftalem4  27055  ftalem5  27056  basellem2  27061  basellem3  27062  basellem8  27067  muinv  27172  fsumdvdsmul  27174  fsumdvdsmulOLD  27176  logfacrlim  27204  logexprlim  27205  perfectlem2  27210  bposlem9  27272  gausslemma2dlem4  27349  lgsquad2lem1  27364  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2sqlem3  27400  2sqmod  27416  rplogsumlem1  27464  dchrisumlem2  27470  dchrisumlem3  27471  dchrmusum2  27474  dchrvmasumlem1  27475  dchrvmasum2lem  27476  dchrvmasum2if  27477  dchrvmasumlem3  27479  dchrvmasumiflem1  27481  dchrvmasumiflem2  27482  rpvmasum2  27492  dchrisum0lem1  27496  dchrisum0lem2a  27497  dchrisum0lem2  27498  dchrmusumlem  27502  dchrvmasumlem  27503  rplogsum  27507  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  mulog2sumlem1  27514  mulog2sumlem2  27515  mulog2sumlem3  27516  vmalogdivsum  27519  logsqvma  27522  log2sumbnd  27524  selberglem1  27525  selberglem2  27526  selberglem3  27527  selberg  27528  selberg2lem  27530  selberg2  27531  selberg3lem1  27537  selberg3  27539  selberg4lem1  27540  selberg4  27541  pntrsumo1  27545  selbergr  27548  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntsval2  27556  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntlemb  27577  pntlemf  27585  pntlemo  27587  ostth2lem2  27614  ostth2lem3  27615  ttgcontlem1  28830  brbtwn2  28850  colinearalg  28855  ax5seglem2  28874  ax5seglem9  28882  axeuclidlem  28907  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  axcontlem8  28916  finsumvtxdg2ssteplem4  29494  ex-ind-dvds  30408  nrt2irr  30420  ipval2  30654  dipcl  30659  riesz3i  32009  re0cj  32688  pythagreim  32689  quad3d  32690  indsum  32786  indsumin  32787  dpfrac1  32814  wrdt2ind  32878  zringfrac  33517  ccfldsrarelvec  33658  ccfldextdgrr  33659  constrrtll  33711  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  constrconj  33725  constrfin  33726  constrelextdg2  33727  nn0constr  33741  constraddcl  33742  constrnegcl  33743  constrdircl  33745  iconstr  33746  constrremulcl  33747  cnre2csqima  33869  rmulccn  33886  dya2icoseg  34238  oddpwdc  34315  eulerpartlems  34321  eulerpartlemsv3  34322  eulerpartlemgs2  34341  signsplypnf  34524  itgexpif  34580  breprexplemc  34606  breprexp  34607  vtscl  34612  vtsprod  34613  circlemeth  34614  logdivsqrle  34624  hgt750lemf  34627  hgt750leme  34632  subfacval2  35151  subfaclim  35152  resconn  35210  iprodgam  35701  fwddifnp1  36125  knoppcnlem10  36462  knoppndvlem2  36473  knoppndvlem7  36478  knoppndvlem9  36480  knoppndvlem11  36482  knoppndvlem14  36485  knoppndvlem16  36487  knoppndvlem17  36488  bj-subcom  37268  bj-bary1lem  37270  bj-bary1lem1  37271  bj-bary1  37272  iblmulc2nc  37651  itgmulc2nc  37654  itgabsnc  37655  ftc1cnnclem  37657  ftc1anclem3  37661  dvasin  37670  areacirclem1  37674  areacirclem4  37677  areacirc  37679  cntotbnd  37762  3factsumint1  41981  3factsumint3  41983  3factsumint4  41984  lcmineqlem2  41990  lcmineqlem6  41994  lcmineqlem8  41996  lcmineqlem10  41998  lcmineqlem11  41999  lcmineqlem12  42000  lcmineqlem16  42004  lcmineqlem18  42006  lcmineqlem23  42011  3lexlogpow5ineq5  42020  aks4d1p1p1  42023  dvrelogpow2b  42028  aks4d1p1p6  42033  aks4d1p1p7  42034  aks4d1p1p5  42035  primrootscoprmpow  42059  posbezout  42060  primrootscoprbij  42062  primrootspoweq0  42066  2np3bcnp1  42104  2ap1caineq  42105  oddnumth  42308  nicomachus  42309  sumcubes  42310  ef11d  42338  cxp112d  42340  cxp111d  42341  readvrec2  42354  sn-addlid  42397  sn-it0e0  42408  sn-negex12  42409  sn-mul01  42418  sn-mullid  42428  sn-0tie0  42432  sn-mul02  42433  cnreeu  42463  fltnltalem  42635  fltnlta  42636  cu3addd  42654  3cubeslem2  42659  3cubeslem3l  42660  3cubeslem3r  42661  3cubeslem4  42663  pellexlem1  42803  pellexlem2  42804  pellexlem6  42808  pell1234qrne0  42827  pell1234qrreccl  42828  pell1234qrmulcl  42829  pell1234qrdich  42835  pell14qrdich  42843  pell1qrge1  42844  pell1qrgaplem  42847  rmspecsqrtnq  42880  qirropth  42882  rmxyneg  42895  rmxyadd  42896  rmxm1  42909  rmym1  42910  rmxluc  42911  rmyluc  42912  rmxdbl  42914  rmydbl  42915  jm2.18  42963  jm2.19lem1  42964  jm2.19lem2  42965  jm2.19lem4  42967  jm2.19  42968  jm2.22  42970  jm2.23  42971  jm2.25  42974  jm2.27c  42982  jm3.1lem2  42993  flcidc  43145  areaquad  43191  sqrtcval  43616  inductionexd  44130  imo72b2lem0  44140  int-leftdistd  44154  radcnvrat  44290  expgrowth  44311  binomcxplemwb  44324  binomcxplemnn0  44325  binomcxplemfrat  44327  binomcxplemdvbinom  44329  binomcxplemnotnn0  44332  sineq0ALT  44914  mul13d  45248  fperiodmullem  45272  fperiodmul  45273  divcan8d  45281  dmmcand  45282  ltdiv23neg  45362  mulc1cncfg  45561  mccllem  45569  clim1fr1  45573  mullimc  45588  mullimcf  45595  sumnnodd  45602  reclimc  45625  sinmulcos  45837  coskpi2  45838  cosknegpi  45841  dvsinexp  45883  dvasinbx  45892  dvdivf  45894  dvdivbd  45895  dvdivcncf  45899  dvbdfbdioolem2  45901  dvxpaek  45912  dvnxpaek  45914  dvnmul  45915  dvmptfprodlem  45916  dvnprodlem2  45919  itgsinexplem1  45926  itgsinexp  45927  itgcoscmulx  45941  itgsincmulx  45946  itgiccshift  45952  itgperiod  45953  stoweidlem1  45973  stoweidlem11  45983  stoweidlem13  45985  stoweidlem14  45986  stoweidlem17  45989  stoweidlem25  45997  stoweidlem26  45998  stoweidlem42  46014  wallispilem4  46040  wallispilem5  46041  wallispi  46042  wallispi2lem1  46043  wallispi2lem2  46044  wallispi2  46045  stirlinglem1  46046  stirlinglem3  46048  stirlinglem4  46049  stirlinglem5  46050  stirlinglem6  46051  stirlinglem7  46052  stirlinglem8  46053  stirlinglem10  46055  stirlinglem11  46056  stirlinglem12  46057  stirlinglem13  46058  stirlinglem14  46059  stirlinglem15  46060  dirker2re  46064  dirkerdenne0  46065  dirkerper  46068  dirkertrigeqlem1  46070  dirkertrigeqlem2  46071  dirkertrigeqlem3  46072  dirkertrigeq  46073  dirkeritg  46074  dirkercncflem2  46076  dirkercncflem4  46078  fourierdlem26  46105  fourierdlem30  46109  fourierdlem39  46118  fourierdlem42  46121  fourierdlem47  46125  fourierdlem48  46126  fourierdlem56  46134  fourierdlem57  46135  fourierdlem58  46136  fourierdlem62  46140  fourierdlem65  46143  fourierdlem66  46144  fourierdlem68  46146  fourierdlem72  46150  fourierdlem73  46151  fourierdlem76  46154  fourierdlem80  46158  fourierdlem83  46161  fourierdlem85  46163  fourierdlem89  46167  fourierdlem90  46168  fourierdlem91  46169  fourierdlem95  46173  fourierdlem97  46175  fourierdlem101  46179  fourierdlem103  46181  fourierdlem104  46182  fourierdlem111  46189  sqwvfoura  46200  sqwvfourb  46201  fourierswlem  46202  fouriersw  46203  elaa2lem  46205  etransclem8  46214  etransclem18  46224  etransclem20  46226  etransclem21  46227  etransclem23  46229  etransclem24  46230  etransclem31  46237  etransclem33  46239  etransclem35  46241  etransclem45  46251  etransclem46  46252  etransclem47  46253  etransclem48  46254  hoicvrrex  46528  hoidmvlelem2  46568  smfmullem1  46763  sigarim  46823  sigarac  46824  sigaraf  46825  sigarmf  46826  sigarls  46829  sigardiv  46833  sigarcol  46836  cevathlem1  46839  fldivmod  47298  fmtnorec2lem  47487  fmtnorec3  47493  fmtnorec4  47494  fmtnoprmfac1  47510  fmtnoprmfac2  47512  fmtnofac2lem  47513  sfprmdvdsmersenne  47548  lighneallem3  47552  quad1  47565  requad01  47566  requad2  47568  opeoALTV  47629  perfectALTVlem2  47667  fppr2odd  47676  0nodd  48044  2nodd  48046  2zlidl  48114  2zrngnmlid  48129  altgsumbcALT  48227  nn0sumshdiglemA  48498  nn0sumshdiglemB  48499  nn0sumshdiglem2  48501  nn0mullong  48504  itcovalt2lem2lem2  48553  ackval2  48561  submuladdmuld  48580  affinecomb2  48582  affineid  48583  1subrec1sub  48584  eenglngeehlnmlem1  48616  eenglngeehlnmlem2  48617  rrx2linest  48621  line2x  48633  line2y  48634  itschlc0yqe  48639  itsclc0yqsollem1  48641  itsclc0yqsol  48643  itscnhlc0xyqsol  48644  itschlc0xyqsol1  48645  itschlc0xyqsol  48646  itsclc0xyqsolr  48648  2itscplem1  48657  2itscplem2  48658  2itscplem3  48659  2itscp  48660  itscnhlinecirc02plem1  48661  itscnhlinecirc02plem2  48662  inlinecirc02plem  48665  inlinecirc02p  48666  i2linesd  49306  aacllem  49328  amgmwlem  49329  amgmlemALT  49330