Theorem mulcld 11278

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

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

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

This theorem is referenced by:  mul02lem1  11434  addrid  11438  cnegex  11439  kcnktkm1cn  11691  subaddmulsub  11723  mulsubaddmulsub  11724  receu  11905  divrec  11935  divcan3  11945  muldivdir  11957  subdivcomb1  11959  subdivcomb2  11960  divdivdiv  11965  divsubdiv  11980  lineq  12101  cru  12255  mul2lt0rlt0  13134  lincmb01cmp  13531  iccf1o  13532  flpmodeq  13910  moddiffl  13918  modvalp1  13926  modcyc  13942  modadd1  13944  modmuladdnn0  13952  modmul1  13961  modaddmulmod  13975  mulexpz  14139  expmulz  14145  binom3  14259  bernneq  14264  mulsubdivbinom2  14297  muldivbinom2  14298  remullem  15163  cjreim2  15196  absimle  15344  abstri  15365  sqreulem  15394  sqreu  15395  bhmafibid1cn  15498  bhmafibid2cn  15499  bhmafibid1  15500  bhmafibid2  15501  mulcn2  15628  reccn2  15629  o1rlimmul  15651  rlimmul  15677  isummulc2  15794  fsummulc2  15816  fsumparts  15838  binomlem  15861  binom1dif  15865  incexclem  15868  incexc  15869  incexc2  15870  pwdif  15900  geomulcvg  15908  mertenslem1  15916  mertens  15918  fprodmul  15992  fprodn0f  16023  iprodmul  16035  binomfallfaclem1  16071  binomfallfaclem2  16072  binomrisefac  16074  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  bpoly4  16091  efaddlem  16125  sinadd  16196  cosadd  16197  tanaddlem  16198  tanadd  16199  addsin  16202  sincossq  16208  sin2t  16209  dvds2ln  16322  oddm1even  16376  pwp1fsum  16424  flodddiv4  16448  sadadd2lem2  16483  bezoutlem2  16573  bezoutlem3  16574  bezoutlem4  16575  lcmgcdlem  16639  phiprmpw  16809  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem16  16863  pcpremul  16876  pcaddlem  16921  fldivp1  16930  mul4sqlem  16986  4sqlem14  16991  vdwapun  17007  vdwlem2  17015  vdwlem6  17019  ablsimpgfindlem1  20141  zringlpirlem3  21492  znunit  21599  blcvx  24833  icopnfcnv  24986  cphipipcj  25247  cphipval2  25288  4cphipval2  25289  cphipval  25290  mbfmulc2re  25696  mbfmulc2  25711  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  itg1mulc  25753  mbfmul  25775  itgcl  25833  itgcnlem  25839  iblmulc2  25880  itgmulc2  25883  itgabs  25884  itgsplit  25885  dvmulbr  25989  dvmulbrOLD  25990  dvcmul  25995  dvcmulf  25996  dvexp  26005  dvmptcmul  26016  dvmptdiv  26026  dvexp3  26030  dvsincos  26033  cmvth  26043  cmvthOLD  26044  dvlipcn  26047  dvfsumabs  26077  dvfsumlem1  26080  ftc1lem4  26094  itgparts  26102  itgpowd  26105  plyf  26251  ply1termlem  26256  plyeq0lem  26263  plypf1  26265  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coeidlem  26290  coeid3  26293  plyco  26294  coemullem  26303  coemulhi  26307  coemulc  26308  dgrcolem2  26328  plycjlem  26330  plyrecj  26335  dvply1  26339  vieta1lem2  26367  vieta1  26368  elqaalem3  26377  aareccl  26382  aalioulem1  26388  taylfvallem1  26412  tayl0  26417  dvtaylp  26426  taylthlem2  26430  taylthlem2OLD  26431  psergf  26469  radcnvlem1  26470  dvradcnv  26478  psercn2  26480  psercn2OLD  26481  pserdvlem2  26486  pserdv2  26488  abelthlem4  26492  abelthlem5  26493  abelthlem6  26494  abelthlem7  26496  abelthlem9  26498  tanregt0  26595  efgh  26597  efabl  26606  efsubm  26607  cosargd  26664  abslogle  26674  tanarg  26675  advlogexp  26711  logtayllem  26715  logtayl  26716  cxpadd  26735  mulcxp  26741  cxpmul  26744  cxpmul2  26745  cxpmul2z  26747  abscxp  26748  abscxp2  26749  dvcxp2  26797  abscxpbnd  26810  root1eq1  26812  cxpeq  26814  angcan  26859  pythag  26874  ssscongptld  26879  affineequiv  26880  affineequiv2  26881  affineequiv3  26882  affineequiv4  26883  chordthmlem2  26890  chordthmlem3  26891  chordthmlem4  26892  chordthmlem5  26893  heron  26895  quad2  26896  quad  26897  dcubic1lem  26900  dcubic2  26901  dcubic1  26902  dcubic  26903  mcubic  26904  cubic2  26905  cubic  26906  binom4  26907  dquartlem1  26908  dquartlem2  26909  dquart  26910  quart1cl  26911  quart1lem  26912  quart1  26913  quartlem1  26914  quartlem2  26915  atantayl3  26996  leibpi  26999  birthdaylem2  27009  divsqrtsumo1  27041  cvxcl  27042  jensenlem2  27045  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgamcvg2  27112  gamcvg  27113  gamcvg2lem  27116  wilthlem2  27126  ftalem1  27130  ftalem2  27131  ftalem4  27133  ftalem5  27134  basellem2  27139  basellem3  27140  basellem8  27145  muinv  27250  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  logfacrlim  27282  logexprlim  27283  perfectlem2  27288  bposlem9  27350  gausslemma2dlem4  27427  lgsquad2lem1  27442  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2sqlem3  27478  2sqmod  27494  rplogsumlem1  27542  dchrisumlem2  27548  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2lem  27554  dchrvmasum2if  27555  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  dchrvmasumiflem2  27560  rpvmasum2  27570  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrmusumlem  27580  dchrvmasumlem  27581  rplogsum  27585  mudivsum  27588  mulogsumlem  27589  mulogsum  27590  mulog2sumlem1  27592  mulog2sumlem2  27593  mulog2sumlem3  27594  vmalogdivsum  27597  logsqvma  27600  log2sumbnd  27602  selberglem1  27603  selberglem2  27604  selberglem3  27605  selberg  27606  selberg2lem  27608  selberg2  27609  selberg3lem1  27615  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrsumo1  27623  selbergr  27626  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntsval2  27634  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntlemb  27655  pntlemf  27663  pntlemo  27665  ostth2lem2  27692  ostth2lem3  27693  ttgcontlem1  28913  brbtwn2  28934  colinearalg  28939  ax5seglem2  28958  ax5seglem9  28966  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  finsumvtxdg2ssteplem4  29580  ex-ind-dvds  30489  nrt2irr  30501  ipval2  30735  dipcl  30740  riesz3i  32090  re0cj  32759  quad3d  32760  dpfrac1  32858  wrdt2ind  32922  zringfrac  33561  ccfldsrarelvec  33695  ccfldextdgrr  33696  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  constrconj  33749  constrfin  33750  constrelextdg2  33751  cnre2csqima  33871  rmulccn  33888  indsum  34001  indsumin  34002  dya2icoseg  34258  oddpwdc  34335  eulerpartlems  34341  eulerpartlemsv3  34342  eulerpartlemgs2  34361  signsplypnf  34543  itgexpif  34599  breprexplemc  34625  breprexp  34626  vtscl  34631  vtsprod  34632  circlemeth  34633  logdivsqrle  34643  hgt750lemf  34646  hgt750leme  34651  subfacval2  35171  subfaclim  35172  resconn  35230  iprodgam  35721  fwddifnp1  36146  knoppcnlem10  36484  knoppndvlem2  36495  knoppndvlem7  36500  knoppndvlem9  36502  knoppndvlem11  36504  knoppndvlem14  36507  knoppndvlem16  36509  knoppndvlem17  36510  bj-subcom  37290  bj-bary1lem  37292  bj-bary1lem1  37293  bj-bary1  37294  iblmulc2nc  37671  itgmulc2nc  37674  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem3  37681  dvasin  37690  areacirclem1  37694  areacirclem4  37697  areacirc  37699  cntotbnd  37782  3factsumint1  42002  3factsumint3  42004  3factsumint4  42005  lcmineqlem2  42011  lcmineqlem6  42015  lcmineqlem8  42017  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem12  42021  lcmineqlem16  42025  lcmineqlem18  42027  lcmineqlem23  42032  3lexlogpow5ineq5  42041  aks4d1p1p1  42044  dvrelogpow2b  42049  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij  42083  primrootspoweq0  42087  2np3bcnp1  42125  2ap1caineq  42126  oddnumth  42323  nicomachus  42324  sumcubes  42325  ef11d  42353  cxp112d  42355  cxp111d  42356  readvrec2  42369  sn-addlid  42410  sn-it0e0  42421  sn-negex12  42422  sn-mul01  42431  sn-mullid  42441  sn-0tie0  42445  sn-mul02  42446  cnreeu  42476  fltnltalem  42648  fltnlta  42649  cu3addd  42667  3cubeslem2  42672  3cubeslem3l  42673  3cubeslem3r  42674  3cubeslem4  42676  pellexlem1  42816  pellexlem2  42817  pellexlem6  42821  pell1234qrne0  42840  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell1234qrdich  42848  pell14qrdich  42856  pell1qrge1  42857  pell1qrgaplem  42860  rmspecsqrtnq  42893  qirropth  42895  rmxyneg  42908  rmxyadd  42909  rmxm1  42922  rmym1  42923  rmxluc  42924  rmyluc  42925  rmxdbl  42927  rmydbl  42928  jm2.18  42976  jm2.19lem1  42977  jm2.19lem2  42978  jm2.19lem4  42980  jm2.19  42981  jm2.22  42983  jm2.23  42984  jm2.25  42987  jm2.27c  42995  jm3.1lem2  43006  flcidc  43158  areaquad  43204  sqrtcval  43630  inductionexd  44144  imo72b2lem0  44154  int-leftdistd  44168  radcnvrat  44309  expgrowth  44330  binomcxplemwb  44343  binomcxplemnn0  44344  binomcxplemfrat  44346  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  sineq0ALT  44934  mul13d  45229  fperiodmullem  45253  fperiodmul  45254  divcan8d  45262  dmmcand  45263  ltdiv23neg  45343  mulc1cncfg  45544  mccllem  45552  clim1fr1  45556  mullimc  45571  mullimcf  45578  sumnnodd  45585  reclimc  45608  sinmulcos  45820  coskpi2  45821  cosknegpi  45824  dvsinexp  45866  dvasinbx  45875  dvdivf  45877  dvdivbd  45878  dvdivcncf  45882  dvbdfbdioolem2  45884  dvxpaek  45895  dvnxpaek  45897  dvnmul  45898  dvmptfprodlem  45899  dvnprodlem2  45902  itgsinexplem1  45909  itgsinexp  45910  itgcoscmulx  45924  itgsincmulx  45929  itgiccshift  45935  itgperiod  45936  stoweidlem1  45956  stoweidlem11  45966  stoweidlem13  45968  stoweidlem14  45969  stoweidlem17  45972  stoweidlem25  45980  stoweidlem26  45981  stoweidlem42  45997  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  dirker2re  46047  dirkerdenne0  46048  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkeritg  46057  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem26  46088  fourierdlem30  46092  fourierdlem39  46101  fourierdlem42  46104  fourierdlem47  46108  fourierdlem48  46109  fourierdlem56  46117  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem65  46126  fourierdlem66  46127  fourierdlem68  46129  fourierdlem72  46133  fourierdlem73  46134  fourierdlem76  46137  fourierdlem80  46141  fourierdlem83  46144  fourierdlem85  46146  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem95  46156  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  etransclem8  46197  etransclem18  46207  etransclem20  46209  etransclem21  46210  etransclem23  46212  etransclem24  46213  etransclem31  46220  etransclem33  46222  etransclem35  46224  etransclem45  46234  etransclem46  46235  etransclem47  46236  etransclem48  46237  hoicvrrex  46511  hoidmvlelem2  46551  smfmullem1  46746  sigarim  46806  sigarac  46807  sigaraf  46808  sigarmf  46809  sigarls  46812  sigardiv  46816  sigarcol  46819  cevathlem1  46822  fldivmod  47277  fmtnorec2lem  47466  fmtnorec3  47472  fmtnorec4  47473  fmtnoprmfac1  47489  fmtnoprmfac2  47491  fmtnofac2lem  47492  sfprmdvdsmersenne  47527  lighneallem3  47531  quad1  47544  requad01  47545  requad2  47547  opeoALTV  47608  perfectALTVlem2  47646  fppr2odd  47655  0nodd  48013  2nodd  48015  2zlidl  48083  2zrngnmlid  48098  altgsumbcALT  48197  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem2  48471  nn0mullong  48474  itcovalt2lem2lem2  48523  ackval2  48531  submuladdmuld  48550  affinecomb2  48552  affineid  48553  1subrec1sub  48554  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2linest  48591  line2x  48603  line2y  48604  itschlc0yqe  48609  itsclc0yqsollem1  48611  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itschlc0xyqsol  48616  itsclc0xyqsolr  48618  2itscplem1  48627  2itscplem2  48628  2itscplem3  48629  2itscp  48630  itscnhlinecirc02plem1  48631  itscnhlinecirc02plem2  48632  inlinecirc02plem  48635  inlinecirc02p  48636  i2linesd  49009  aacllem  49031  amgmwlem  49032  amgmlemALT  49033