Theorem mulcld 11202

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

Syntax hints:   → wi 4   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071   · cmul 11078

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  mul02lem1  11359  addrid  11363  cnegex  11364  kcnktkm1cn  11618  subaddmulsub  11650  mulsubaddmulsub  11651  receu  11832  divrec  11861  divcan3  11871  muldivdir  11883  subdivcomb1  11886  subdivcomb2  11887  divdivdiv  11892  divsubdiv  11907  lineq  12028  cru  12187  mul2lt0rlt0  13097  lincmb01cmp  13499  iccf1o  13500  flpmodeq  13884  moddiffl  13892  modvalp1  13900  modcyc  13916  modadd1  13918  modmuladdnn0  13928  modmul1  13937  modaddmulmod  13951  mulexpz  14115  expmulz  14121  binom3  14237  bernneq  14242  mulsubdivbinom2  14275  muldivbinom2  14276  remullem  15155  cjreim2  15188  absimle  15336  abstri  15358  sqreulem  15387  sqreu  15388  bhmafibid1cn  15493  bhmafibid2cn  15494  bhmafibid1  15495  bhmafibid2  15496  mulcn2  15623  reccn2  15624  o1rlimmul  15646  rlimmul  15672  isummulc2  15789  fsummulc2  15811  fsumparts  15834  indsum  15856  binomlem  15859  binom1dif  15863  incexclem  15866  incexc  15867  incexc2  15868  pwdif  15898  geomulcvg  15906  mertenslem1  15914  mertens  15916  fprodmul  15990  fprodn0f  16021  iprodmul  16033  binomfallfaclem1  16069  binomfallfaclem2  16070  binomrisefac  16072  bpolycl  16082  bpolysum  16083  bpolydiflem  16084  bpoly4  16089  efaddlem  16123  sinadd  16196  cosadd  16197  tanaddlem  16198  tanadd  16199  addsin  16202  sincossq  16208  sin2t  16209  dvds2ln  16323  oddm1even  16377  pwp1fsum  16425  flodddiv4  16449  sadadd2lem2  16484  bezoutlem2  16574  bezoutlem3  16575  bezoutlem4  16576  lcmgcdlem  16640  phiprmpw  16811  pythagtriplem12  16862  pythagtriplem14  16864  pythagtriplem16  16866  pcpremul  16879  pcaddlem  16924  fldivp1  16933  mul4sqlem  16989  4sqlem14  16994  vdwapun  17010  vdwlem2  17018  vdwlem6  17022  ablsimpgfindlem1  20149  zringlpirlem3  21516  znunit  21615  blcvx  24858  icopnfcnv  25004  cphipipcj  25262  cphipval2  25303  4cphipval2  25304  cphipval  25305  mbfmulc2re  25710  mbfmulc2  25725  itg1addlem4  25761  itg1addlem5  25762  itg1mulc  25766  mbfmul  25788  itgcl  25846  itgcnlem  25852  iblmulc2  25893  itgmulc2  25896  itgabs  25897  itgsplit  25898  dvmulbr  26001  dvcmul  26006  dvcmulf  26007  dvexp  26015  dvmptcmul  26026  dvmptdiv  26036  dvexp3  26040  dvsincos  26043  cmvth  26053  dvlipcn  26056  dvfsumabs  26085  dvfsumlem1  26088  ftc1lem4  26101  itgparts  26109  itgpowd  26112  plyf  26258  ply1termlem  26263  plyeq0lem  26270  plypf1  26272  plyaddlem1  26273  plymullem1  26274  coeeulem  26284  coeidlem  26297  coeid3  26300  plyco  26301  coemullem  26310  coemulhi  26314  coemulc  26315  dgrcolem2  26334  plycjlem  26336  plyrecj  26341  dvply1  26348  vieta1lem2  26375  vieta1  26376  elqaalem3  26385  aareccl  26390  aalioulem1  26396  taylfvallem1  26420  tayl0  26425  dvtaylp  26433  taylthlem2  26437  psergf  26475  radcnvlem1  26476  dvradcnv  26484  psercn2  26486  pserdvlem2  26491  pserdv2  26493  abelthlem4  26497  abelthlem5  26498  abelthlem6  26499  abelthlem7  26501  abelthlem9  26503  tanregt0  26604  efgh  26606  efabl  26615  efsubm  26616  cosargd  26673  abslogle  26683  tanarg  26684  advlogexp  26720  logtayllem  26724  logtayl  26725  cxpadd  26744  mulcxp  26750  cxpmul  26753  cxpmul2  26754  cxpmul2z  26756  abscxp  26757  abscxp2  26758  dvcxp2  26806  abscxpbnd  26818  root1eq1  26820  cxpeq  26822  angcan  26867  pythag  26882  ssscongptld  26887  affineequiv  26888  affineequiv2  26889  affineequiv3  26890  affineequiv4  26891  chordthmlem2  26898  chordthmlem3  26899  chordthmlem4  26900  chordthmlem5  26901  heron  26903  quad2  26904  quad  26905  dcubic1lem  26908  dcubic2  26909  dcubic1  26910  dcubic  26911  mcubic  26912  cubic2  26913  cubic  26914  binom4  26915  dquartlem1  26916  dquartlem2  26917  dquart  26918  quart1cl  26919  quart1lem  26920  quart1  26921  quartlem1  26922  quartlem2  26923  atantayl3  27004  leibpi  27007  birthdaylem2  27017  divsqrtsumo1  27048  cvxcl  27049  jensenlem2  27052  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamgulmlem4  27096  lgamgulmlem5  27097  lgamgulmlem6  27098  lgamgulm2  27100  lgamcvg2  27119  gamcvg  27120  gamcvg2lem  27123  wilthlem2  27133  ftalem1  27137  ftalem2  27138  ftalem4  27140  ftalem5  27141  basellem2  27146  basellem3  27147  basellem8  27152  muinv  27257  fsumdvdsmul  27259  logfacrlim  27288  logexprlim  27289  perfectlem2  27294  bposlem9  27356  gausslemma2dlem4  27433  lgsquad2lem1  27448  2lgslem3b  27461  2lgslem3c  27462  2lgslem3d  27463  2sqlem3  27484  2sqmod  27500  rplogsumlem1  27548  dchrisumlem2  27554  dchrisumlem3  27555  dchrmusum2  27558  dchrvmasumlem1  27559  dchrvmasum2lem  27560  dchrvmasum2if  27561  dchrvmasumlem3  27563  dchrvmasumiflem1  27565  dchrvmasumiflem2  27566  rpvmasum2  27576  dchrisum0lem1  27580  dchrisum0lem2a  27581  dchrisum0lem2  27582  dchrmusumlem  27586  dchrvmasumlem  27587  rplogsum  27591  mudivsum  27594  mulogsumlem  27595  mulogsum  27596  mulog2sumlem1  27598  mulog2sumlem2  27599  mulog2sumlem3  27600  vmalogdivsum  27603  logsqvma  27606  log2sumbnd  27608  selberglem1  27609  selberglem2  27610  selberglem3  27611  selberg  27612  selberg2lem  27614  selberg2  27615  selberg3lem1  27621  selberg3  27623  selberg4lem1  27624  selberg4  27625  pntrsumo1  27629  selbergr  27632  selberg3r  27633  selberg4r  27634  selberg34r  27635  pntsval2  27640  pntrlog2bndlem1  27641  pntrlog2bndlem2  27642  pntrlog2bndlem3  27643  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntrlog2bndlem6  27647  pntrlog2bnd  27648  pntlemb  27661  pntlemf  27669  pntlemo  27671  ostth2lem2  27698  ostth2lem3  27699  ttgcontlem1  29085  brbtwn2  29106  colinearalg  29111  ax5seglem2  29130  ax5seglem9  29138  axeuclidlem  29163  axcontlem2  29166  axcontlem4  29168  axcontlem7  29171  axcontlem8  29172  finsumvtxdg2ssteplem4  29749  ex-ind-dvds  30663  nrt2irr  30675  ipval2  30910  dipcl  30915  riesz3i  32265  re0cj  32945  pythagreim  32947  quad3d  32951  indsumin  33039  dpfrac1  33069  wrdt2ind  33131  zringfrac  33750  ccfldsrarelvec  33968  ccfldextdgrr  33969  constrrtll  34028  constrrtlc1  34029  constrrtcclem  34031  constrrtcc  34032  constrconj  34042  constrfin  34043  constrelextdg2  34044  nn0constr  34058  constraddcl  34059  constrnegcl  34060  constrdircl  34062  iconstr  34063  constrremulcl  34064  constrrecl  34066  constrimcl  34067  constrmulcl  34068  constrreinvcl  34069  constrinvcl  34070  constrresqrtcl  34074  constrabscl  34075  constrsqrtcl  34076  cos9thpiminplylem1  34079  cos9thpiminplylem2  34080  cos9thpiminplylem3  34081  cos9thpiminply  34085  cos9thpinconstrlem1  34086  cos9thpinconstrlem2  34087  cos9thpinconstr  34088  cnre2csqima  34208  rmulccn  34225  dya2icoseg  34574  oddpwdc  34651  eulerpartlems  34657  eulerpartlemsv3  34658  eulerpartlemgs2  34677  signsplypnf  34844  itgexpif  34900  breprexplemc  34926  breprexp  34927  vtscl  34932  vtsprod  34933  circlemeth  34934  logdivsqrle  34944  hgt750lemf  34947  hgt750leme  34952  subfacval2  35537  subfaclim  35538  resconn  35596  iprodgam  36092  fwddifnp1  36515  knoppcnlem10  36940  knoppndvlem2  36951  knoppndvlem7  36956  knoppndvlem9  36958  knoppndvlem11  36960  knoppndvlem14  36963  knoppndvlem16  36965  knoppndvlem17  36966  bj-subcom  37800  bj-bary1lem  37802  bj-bary1lem1  37803  bj-bary1  37804  qdiff  37819  iblmulc2nc  38184  itgmulc2nc  38187  itgabsnc  38188  ftc1cnnclem  38190  ftc1anclem3  38194  dvasin  38203  areacirclem1  38207  areacirclem4  38210  areacirc  38212  cntotbnd  38295  3factsumint1  42638  3factsumint3  42640  3factsumint4  42641  lcmineqlem2  42647  lcmineqlem6  42651  lcmineqlem8  42653  lcmineqlem10  42655  lcmineqlem11  42656  lcmineqlem12  42657  lcmineqlem16  42661  lcmineqlem18  42663  lcmineqlem23  42668  3lexlogpow5ineq5  42677  aks4d1p1p1  42680  dvrelogpow2b  42685  aks4d1p1p6  42690  aks4d1p1p7  42691  aks4d1p1p5  42692  primrootscoprmpow  42716  posbezout  42717  primrootscoprbij  42719  primrootspoweq0  42723  2np3bcnp1  42761  2ap1caineq  42762  oddnumth  42920  nicomachus  42921  sumcubes  42922  ef11d  42948  cxp112d  42950  cxp111d  42951  readvrec2  42970  sn-addlid  43013  sn-it0e0  43025  sn-negex12  43026  sn-mul01  43035  sn-mullid  43045  sn-0tie0  43073  sn-mul02  43074  cnreeu  43112  fltnltalem  43244  fltnlta  43245  cu3addd  43262  3cubeslem2  43266  3cubeslem3l  43267  3cubeslem3r  43268  3cubeslem4  43270  pellexlem1  43406  pellexlem2  43407  pellexlem6  43411  pell1234qrne0  43430  pell1234qrreccl  43431  pell1234qrmulcl  43432  pell1234qrdich  43438  pell14qrdich  43446  pell1qrge1  43447  pell1qrgaplem  43450  rmspecsqrtnq  43483  qirropth  43485  rmxyneg  43497  rmxyadd  43498  rmxm1  43511  rmym1  43512  rmxluc  43513  rmyluc  43514  rmxdbl  43516  rmydbl  43517  jm2.18  43565  jm2.19lem1  43566  jm2.19lem2  43567  jm2.19lem4  43569  jm2.19  43570  jm2.22  43572  jm2.23  43573  jm2.25  43576  jm2.27c  43584  jm3.1lem2  43595  flcidc  43747  areaquad  43793  sqrtcval  44217  inductionexd  44731  imo72b2lem0  44741  int-leftdistd  44755  radcnvrat  44890  expgrowth  44911  binomcxplemwb  44924  binomcxplemnn0  44925  binomcxplemfrat  44927  binomcxplemdvbinom  44929  binomcxplemnotnn0  44932  sineq0ALT  45512  mul13d  45859  fperiodmullem  45882  fperiodmul  45883  divcan8d  45891  dmmcand  45892  ltdiv23neg  45969  mulc1cncfg  46165  mccllem  46173  clim1fr1  46177  mullimc  46192  mullimcf  46199  sumnnodd  46206  reclimc  46227  sinmulcos  46439  coskpi2  46440  cosknegpi  46443  dvsinexp  46485  dvasinbx  46494  dvdivf  46496  dvdivbd  46497  dvdivcncf  46501  dvbdfbdioolem2  46503  dvxpaek  46514  dvnxpaek  46516  dvnmul  46517  dvmptfprodlem  46518  dvnprodlem2  46521  itgsinexplem1  46528  itgsinexp  46529  itgcoscmulx  46543  itgsincmulx  46548  itgiccshift  46554  itgperiod  46555  stoweidlem1  46575  stoweidlem11  46585  stoweidlem13  46587  stoweidlem14  46588  stoweidlem17  46591  stoweidlem25  46599  stoweidlem26  46600  stoweidlem42  46616  wallispilem4  46642  wallispilem5  46643  wallispi  46644  wallispi2lem1  46645  wallispi2lem2  46646  wallispi2  46647  stirlinglem1  46648  stirlinglem3  46650  stirlinglem4  46651  stirlinglem5  46652  stirlinglem6  46653  stirlinglem7  46654  stirlinglem8  46655  stirlinglem10  46657  stirlinglem11  46658  stirlinglem12  46659  stirlinglem13  46660  stirlinglem14  46661  stirlinglem15  46662  dirker2re  46666  dirkerdenne0  46667  dirkerper  46670  dirkertrigeqlem1  46672  dirkertrigeqlem2  46673  dirkertrigeqlem3  46674  dirkertrigeq  46675  dirkeritg  46676  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem26  46707  fourierdlem30  46711  fourierdlem39  46720  fourierdlem42  46723  fourierdlem47  46727  fourierdlem48  46728  fourierdlem56  46736  fourierdlem57  46737  fourierdlem58  46738  fourierdlem62  46742  fourierdlem65  46745  fourierdlem66  46746  fourierdlem68  46748  fourierdlem72  46752  fourierdlem73  46753  fourierdlem76  46756  fourierdlem80  46760  fourierdlem83  46763  fourierdlem85  46765  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  fourierdlem95  46775  fourierdlem97  46777  fourierdlem101  46781  fourierdlem103  46783  fourierdlem104  46784  fourierdlem111  46791  sqwvfoura  46802  sqwvfourb  46803  fourierswlem  46804  fouriersw  46805  elaa2lem  46807  etransclem8  46816  etransclem18  46826  etransclem20  46828  etransclem21  46829  etransclem23  46831  etransclem24  46832  etransclem31  46839  etransclem33  46841  etransclem35  46843  etransclem45  46853  etransclem46  46854  etransclem47  46855  etransclem48  46856  hoicvrrex  47130  hoidmvlelem2  47170  smfmullem1  47365  sigarim  47425  sigarac  47426  sigaraf  47427  sigarmf  47428  sigarls  47431  sigardiv  47435  sigarcol  47438  cevathlem1  47441  sin3t  47465  cos3t  47466  sin5tlem1  47467  sin5tlem2  47468  sin5tlem3  47469  sin5tlem4  47470  sin5tlem5  47471  sin5t  47472  cos5t  47473  fldivmod  47938  fmtnorec2lem  48151  fmtnorec3  48157  fmtnorec4  48158  fmtnoprmfac1  48174  fmtnoprmfac2  48176  fmtnofac2lem  48177  sfprmdvdsmersenne  48212  lighneallem3  48216  quad1  48242  requad01  48243  requad2  48245  opeoALTV  48306  perfectALTVlem2  48344  fppr2odd  48353  0nodd  48792  2nodd  48794  2zlidl  48862  2zrngnmlid  48877  altgsumbcALT  48975  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  nn0sumshdiglem2  49244  nn0mullong  49247  itcovalt2lem2lem2  49296  ackval2  49304  submuladdmuld  49323  affinecomb2  49325  affineid  49326  1subrec1sub  49327  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  rrx2linest  49364  line2x  49376  line2y  49377  itschlc0yqe  49382  itsclc0yqsollem1  49384  itsclc0yqsol  49386  itscnhlc0xyqsol  49387  itschlc0xyqsol1  49388  itschlc0xyqsol  49389  itsclc0xyqsolr  49391  2itscplem1  49400  2itscplem2  49401  2itscplem3  49402  2itscp  49403  itscnhlinecirc02plem1  49404  itscnhlinecirc02plem2  49405  inlinecirc02plem  49408  inlinecirc02p  49409  i2linesd  50400  aacllem  50422  amgmwlem  50423  amgmlemALT  50424