Theorem mulcld 11224

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   · cmul 11100

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mul02lem1  11381  addrid  11385  cnegex  11386  kcnktkm1cn  11640  subaddmulsub  11672  mulsubaddmulsub  11673  receu  11854  divrec  11883  divcan3  11893  muldivdir  11902  subdivcomb1  11905  subdivcomb2  11906  divdivdiv  11911  divsubdiv  11926  lineq  12047  cru  12205  mul2lt0rlt0  13115  lincmb01cmp  13517  iccf1o  13518  flpmodeq  13903  moddiffl  13911  modvalp1  13919  modcyc  13935  modadd1  13937  modmuladdnn0  13947  modmul1  13956  modaddmulmod  13970  mulexpz  14134  expmulz  14140  binom3  14256  bernneq  14261  mulsubdivbinom2  14294  muldivbinom2  14295  remullem  15175  cjreim2  15208  absimle  15356  abstri  15378  sqreulem  15407  sqreu  15408  bhmafibid1cn  15513  bhmafibid2cn  15514  bhmafibid1  15515  bhmafibid2  15516  mulcn2  15643  reccn2  15644  o1rlimmul  15666  rlimmul  15692  isummulc2  15809  fsummulc2  15831  fsumparts  15854  indsum  15876  binomlem  15879  binom1dif  15883  incexclem  15886  incexc  15887  incexc2  15888  pwdif  15918  geomulcvg  15926  mertenslem1  15934  mertens  15936  fprodmul  16010  fprodn0f  16041  iprodmul  16053  binomfallfaclem1  16088  binomfallfaclem2  16089  binomrisefac  16091  bpolycl  16101  bpolysum  16102  bpolydiflem  16103  bpoly4  16108  efaddlem  16142  sinadd  16215  cosadd  16216  tanaddlem  16217  tanadd  16218  addsin  16221  sincossq  16227  sin2t  16228  dvds2ln  16342  oddm1even  16396  pwp1fsum  16444  flodddiv4  16468  sadadd2lem2  16503  bezoutlem2  16593  bezoutlem3  16594  bezoutlem4  16595  lcmgcdlem  16659  phiprmpw  16830  pythagtriplem12  16881  pythagtriplem14  16883  pythagtriplem16  16885  pcpremul  16898  pcaddlem  16943  fldivp1  16952  mul4sqlem  17008  4sqlem14  17013  vdwapun  17029  vdwlem2  17037  vdwlem6  17041  ablsimpgfindlem1  20174  zringlpirlem3  21614  znunit  21713  blcvx  24955  icopnfcnv  25101  cphipipcj  25359  cphipval2  25400  4cphipval2  25401  cphipval  25402  mbfmulc2re  25807  mbfmulc2  25822  itg1addlem4  25858  itg1addlem5  25859  itg1mulc  25863  mbfmul  25885  itgcl  25943  itgcnlem  25949  iblmulc2  25990  itgmulc2  25993  itgabs  25994  itgsplit  25995  dvmulbr  26098  dvcmul  26103  dvcmulf  26104  dvexp  26112  dvmptcmul  26123  dvmptdiv  26133  dvexp3  26137  dvsincos  26140  cmvth  26150  dvlipcn  26153  dvfsumabs  26182  dvfsumlem1  26185  ftc1lem4  26198  itgparts  26206  itgpowd  26209  plyf  26355  ply1termlem  26360  plyeq0lem  26367  plypf1  26369  plyaddlem1  26370  plymullem1  26371  coeeulem  26381  coeidlem  26394  coeid3  26397  plyco  26398  coemullem  26407  coemulhi  26411  coemulc  26412  dgrcolem2  26431  plycjlem  26433  plyrecj  26438  dvply1  26445  vieta1lem2  26472  vieta1  26473  elqaalem3  26482  aareccl  26489  aalioulem1  26495  taylfvallem1  26520  tayl0  26525  dvtaylp  26533  taylthlem2  26537  psergf  26575  radcnvlem1  26576  dvradcnv  26584  psercn2  26586  pserdvlem2  26591  pserdv2  26593  abelthlem4  26597  abelthlem5  26598  abelthlem6  26599  abelthlem7  26601  abelthlem9  26603  tanregt0  26704  efgh  26706  efabl  26715  efsubm  26716  cosargd  26773  abslogle  26783  tanarg  26784  advlogexp  26820  logtayllem  26824  logtayl  26825  cxpadd  26844  mulcxp  26850  cxpmul  26853  cxpmul2  26854  cxpmul2z  26856  abscxp  26857  abscxp2  26858  dvcxp2  26906  abscxpbnd  26918  root1eq1  26920  cxpeq  26922  angcan  26967  pythag  26982  ssscongptld  26987  affineequiv  26988  affineequiv2  26989  affineequiv3  26990  affineequiv4  26991  chordthmlem2  26998  chordthmlem3  26999  chordthmlem4  27000  chordthmlem5  27001  heron  27003  quad2  27004  quad  27005  dcubic1lem  27008  dcubic2  27009  dcubic1  27010  dcubic  27011  mcubic  27012  cubic2  27013  cubic  27014  binom4  27015  dquartlem1  27016  dquartlem2  27017  dquart  27018  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem1  27022  quartlem2  27023  atantayl3  27104  leibpi  27107  birthdaylem2  27117  divsqrtsumo1  27148  cvxcl  27149  jensenlem2  27152  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem4  27196  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgamcvg2  27219  gamcvg  27220  gamcvg2lem  27223  wilthlem2  27233  ftalem1  27237  ftalem2  27238  ftalem4  27240  ftalem5  27241  basellem2  27246  basellem3  27247  basellem8  27252  muinv  27357  fsumdvdsmul  27359  logfacrlim  27388  logexprlim  27389  perfectlem2  27394  bposlem9  27456  gausslemma2dlem4  27533  lgsquad2lem1  27548  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2sqlem3  27584  2sqmod  27600  rplogsumlem1  27648  dchrisumlem2  27654  dchrisumlem3  27655  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasum2lem  27660  dchrvmasum2if  27661  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  rpvmasum2  27676  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrmusumlem  27686  dchrvmasumlem  27687  rplogsum  27691  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  mulog2sumlem1  27698  mulog2sumlem2  27699  mulog2sumlem3  27700  vmalogdivsum  27703  logsqvma  27706  log2sumbnd  27708  selberglem1  27709  selberglem2  27710  selberglem3  27711  selberg  27712  selberg2lem  27714  selberg2  27715  selberg3lem1  27721  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrsumo1  27729  selbergr  27732  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntsval2  27740  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntlemb  27761  pntlemf  27769  pntlemo  27771  ostth2lem2  27798  ostth2lem3  27799  ttgcontlem1  29234  brbtwn2  29255  colinearalg  29260  ax5seglem2  29279  ax5seglem9  29287  axeuclidlem  29312  axcontlem2  29315  axcontlem4  29317  axcontlem7  29320  axcontlem8  29321  finsumvtxdg2ssteplem4  29898  ex-ind-dvds  30812  nrt2irr  30824  ipval2  31059  dipcl  31064  riesz3i  32414  re0cj  33088  pythagreim  33090  quad3d  33094  indsumin  33181  dpfrac1  33211  wrdt2ind  33273  zringfrac  33844  ccfldsrarelvec  34061  ccfldextdgrr  34062  constrrtll  34121  constrrtlc1  34122  constrrtcclem  34124  constrrtcc  34125  constrconj  34135  constrfin  34136  constrelextdg2  34137  nn0constr  34151  constraddcl  34152  constrnegcl  34153  constrdircl  34155  iconstr  34156  constrremulcl  34157  constrrecl  34159  constrimcl  34160  constrmulcl  34161  constrreinvcl  34162  constrinvcl  34163  constrresqrtcl  34167  constrabscl  34168  constrsqrtcl  34169  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminply  34178  cos9thpinconstrlem1  34179  cos9thpinconstrlem2  34180  cos9thpinconstr  34181  cnre2csqima  34301  rmulccn  34318  dya2icoseg  34667  oddpwdc  34744  eulerpartlems  34750  eulerpartlemsv3  34751  eulerpartlemgs2  34770  signsplypnf  34937  itgexpif  34993  breprexplemc  35019  breprexp  35020  vtscl  35025  vtsprod  35026  circlemeth  35027  logdivsqrle  35037  hgt750lemf  35040  hgt750leme  35045  subfacval2  35679  subfaclim  35680  resconn  35738  iprodgam  36234  fwddifnp1  36657  knoppcnlem10  37111  knoppndvlem2  37122  knoppndvlem7  37127  knoppndvlem9  37129  knoppndvlem11  37131  knoppndvlem14  37134  knoppndvlem16  37136  knoppndvlem17  37137  bj-subcom  37972  bj-bary1lem  37974  bj-bary1lem1  37975  bj-bary1  37976  qdiff  37991  iblmulc2nc  38356  itgmulc2nc  38359  itgabsnc  38360  ftc1cnnclem  38362  ftc1anclem3  38366  dvasin  38375  areacirclem1  38379  areacirclem4  38382  areacirc  38384  cntotbnd  38467  3factsumint1  42808  3factsumint3  42810  3factsumint4  42811  lcmineqlem2  42817  lcmineqlem6  42821  lcmineqlem8  42823  lcmineqlem10  42825  lcmineqlem11  42826  lcmineqlem12  42827  lcmineqlem16  42831  lcmineqlem18  42833  lcmineqlem23  42838  3lexlogpow5ineq5  42847  aks4d1p1p1  42850  dvrelogpow2b  42855  aks4d1p1p6  42860  aks4d1p1p7  42861  aks4d1p1p5  42862  primrootscoprmpow  42886  posbezout  42887  primrootscoprbij  42889  primrootspoweq0  42893  2np3bcnp1  42931  2ap1caineq  42932  quadfac  42992  oddnumth  43092  nicomachus  43093  sumcubes  43094  ef11d  43120  cxp112d  43122  cxp111d  43123  readvrec2  43142  sn-addlid  43185  sn-it0e0  43197  sn-negex12  43198  sn-mul01  43207  sn-mullid  43217  sn-0tie0  43245  sn-mul02  43246  cnreeu  43284  fltnltalem  43414  fltnlta  43415  cu3addd  43432  3cubeslem2  43436  3cubeslem3l  43437  3cubeslem3r  43438  3cubeslem4  43440  pellexlem1  43576  pellexlem2  43577  pellexlem6  43581  pell1234qrne0  43600  pell1234qrreccl  43601  pell1234qrmulcl  43602  pell1234qrdich  43608  pell14qrdich  43616  pell1qrge1  43617  pell1qrgaplem  43620  rmspecsqrtnq  43653  qirropth  43655  rmxyneg  43667  rmxyadd  43668  rmxm1  43681  rmym1  43682  rmxluc  43683  rmyluc  43684  rmxdbl  43686  rmydbl  43687  jm2.18  43735  jm2.19lem1  43736  jm2.19lem2  43737  jm2.19lem4  43739  jm2.19  43740  jm2.22  43742  jm2.23  43743  jm2.25  43746  jm2.27c  43754  jm3.1lem2  43765  flcidc  43917  areaquad  43963  sqrtcval  44387  inductionexd  44901  imo72b2lem0  44911  int-leftdistd  44925  radcnvrat  45044  expgrowth  45065  binomcxplemwb  45078  binomcxplemnn0  45079  binomcxplemfrat  45081  binomcxplemdvbinom  45083  binomcxplemnotnn0  45086  sineq0ALT  45665  mul13d  46019  fperiodmullem  46042  fperiodmul  46043  divcan8d  46051  dmmcand  46052  ltdiv23neg  46129  mulc1cncfg  46325  mccllem  46333  clim1fr1  46337  mullimc  46352  mullimcf  46359  sumnnodd  46366  reclimc  46387  sinmulcos  46599  coskpi2  46600  cosknegpi  46603  dvsinexp  46645  dvasinbx  46654  dvdivf  46656  dvdivbd  46657  dvdivcncf  46661  dvbdfbdioolem2  46663  dvxpaek  46674  dvnxpaek  46676  dvnmul  46677  dvmptfprodlem  46678  dvnprodlem2  46681  itgsinexplem1  46688  itgsinexp  46689  itgcoscmulx  46703  itgsincmulx  46708  itgiccshift  46714  itgperiod  46715  stoweidlem1  46735  stoweidlem11  46745  stoweidlem13  46747  stoweidlem14  46748  stoweidlem17  46751  stoweidlem25  46759  stoweidlem26  46760  stoweidlem42  46776  wallispilem4  46802  wallispilem5  46803  wallispi  46804  wallispi2lem1  46805  wallispi2lem2  46806  wallispi2  46807  stirlinglem1  46808  stirlinglem3  46810  stirlinglem4  46811  stirlinglem5  46812  stirlinglem6  46813  stirlinglem7  46814  stirlinglem8  46815  stirlinglem10  46817  stirlinglem11  46818  stirlinglem12  46819  stirlinglem13  46820  stirlinglem14  46821  stirlinglem15  46822  dirker2re  46826  dirkerdenne0  46827  dirkerper  46830  dirkertrigeqlem1  46832  dirkertrigeqlem2  46833  dirkertrigeqlem3  46834  dirkertrigeq  46835  dirkeritg  46836  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem26  46867  fourierdlem30  46871  fourierdlem39  46880  fourierdlem42  46883  fourierdlem47  46887  fourierdlem48  46888  fourierdlem56  46896  fourierdlem57  46897  fourierdlem58  46898  fourierdlem62  46902  fourierdlem65  46905  fourierdlem66  46906  fourierdlem68  46908  fourierdlem72  46912  fourierdlem73  46913  fourierdlem76  46916  fourierdlem80  46920  fourierdlem83  46923  fourierdlem85  46925  fourierdlem89  46929  fourierdlem90  46930  fourierdlem91  46931  fourierdlem95  46935  fourierdlem97  46937  fourierdlem101  46941  fourierdlem103  46943  fourierdlem104  46944  fourierdlem111  46951  sqwvfoura  46962  sqwvfourb  46963  fourierswlem  46964  fouriersw  46965  elaa2lem  46967  etransclem8  46976  etransclem18  46986  etransclem20  46988  etransclem21  46989  etransclem23  46991  etransclem24  46992  etransclem31  46999  etransclem33  47001  etransclem35  47003  etransclem45  47013  etransclem46  47014  etransclem47  47015  etransclem48  47016  hoicvrrex  47290  hoidmvlelem2  47330  smfmullem1  47525  sigarim  47585  sigarac  47586  sigaraf  47587  sigarmf  47588  sigarls  47591  sigardiv  47595  sigarcol  47598  cevathlem1  47601  sin3t  47628  cos3t  47629  sin5tlem1  47630  sin5tlem2  47631  sin5tlem3  47632  sin5tlem4  47633  sin5tlem5  47634  sin5t  47635  cos5t  47636  fldivmod  48101  fmtnorec2lem  48314  fmtnorec3  48320  fmtnorec4  48321  fmtnoprmfac1  48337  fmtnoprmfac2  48339  fmtnofac2lem  48340  sfprmdvdsmersenne  48375  lighneallem3  48379  quad1  48405  requad01  48406  requad2  48408  opeoALTV  48469  perfectALTVlem2  48507  fppr2odd  48516  0nodd  48955  2nodd  48957  2zlidl  49025  2zrngnmlid  49040  altgsumbcALT  49153  nn0sumshdiglemA  49419  nn0sumshdiglemB  49420  nn0sumshdiglem2  49422  nn0mullong  49425  itcovalt2lem2lem2  49474  ackval2  49482  submuladdmuld  49501  affinecomb2  49503  affineid  49504  1subrec1sub  49505  eenglngeehlnmlem1  49537  eenglngeehlnmlem2  49538  rrx2linest  49542  line2x  49554  line2y  49555  itschlc0yqe  49560  itsclc0yqsollem1  49562  itsclc0yqsol  49564  itscnhlc0xyqsol  49565  itschlc0xyqsol1  49566  itschlc0xyqsol  49567  itsclc0xyqsolr  49569  2itscplem1  49578  2itscplem2  49579  2itscplem3  49580  2itscp  49581  itscnhlinecirc02plem1  49582  itscnhlinecirc02plem2  49583  inlinecirc02plem  49586  inlinecirc02p  49587  i2linesd  50577  aacllem  50641  amgmwlem  50669  amgmlemALT  50670