Theorem mulcld 11154

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   · cmul 11032

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

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

This theorem is referenced by:  mul02lem1  11311  addrid  11315  cnegex  11316  kcnktkm1cn  11570  subaddmulsub  11602  mulsubaddmulsub  11603  receu  11784  divrec  11814  divcan3  11824  muldivdir  11836  subdivcomb1  11839  subdivcomb2  11840  divdivdiv  11845  divsubdiv  11860  lineq  11981  cru  12140  mul2lt0rlt0  13035  lincmb01cmp  13437  iccf1o  13438  flpmodeq  13822  moddiffl  13830  modvalp1  13838  modcyc  13854  modadd1  13856  modmuladdnn0  13866  modmul1  13875  modaddmulmod  13889  mulexpz  14053  expmulz  14059  binom3  14175  bernneq  14180  mulsubdivbinom2  14213  muldivbinom2  14214  remullem  15079  cjreim2  15112  absimle  15260  abstri  15282  sqreulem  15311  sqreu  15312  bhmafibid1cn  15417  bhmafibid2cn  15418  bhmafibid1  15419  bhmafibid2  15420  mulcn2  15547  reccn2  15548  o1rlimmul  15570  rlimmul  15596  isummulc2  15713  fsummulc2  15735  fsumparts  15758  indsum  15780  binomlem  15783  binom1dif  15787  incexclem  15790  incexc  15791  incexc2  15792  pwdif  15822  geomulcvg  15830  mertenslem1  15838  mertens  15840  fprodmul  15914  fprodn0f  15945  iprodmul  15957  binomfallfaclem1  15993  binomfallfaclem2  15994  binomrisefac  15996  bpolycl  16006  bpolysum  16007  bpolydiflem  16008  bpoly4  16013  efaddlem  16047  sinadd  16120  cosadd  16121  tanaddlem  16122  tanadd  16123  addsin  16126  sincossq  16132  sin2t  16133  dvds2ln  16247  oddm1even  16301  pwp1fsum  16349  flodddiv4  16373  sadadd2lem2  16408  bezoutlem2  16498  bezoutlem3  16499  bezoutlem4  16500  lcmgcdlem  16564  phiprmpw  16735  pythagtriplem12  16786  pythagtriplem14  16788  pythagtriplem16  16790  pcpremul  16803  pcaddlem  16848  fldivp1  16857  mul4sqlem  16913  4sqlem14  16918  vdwapun  16934  vdwlem2  16942  vdwlem6  16946  ablsimpgfindlem1  20073  zringlpirlem3  21452  znunit  21551  blcvx  24772  icopnfcnv  24918  cphipipcj  25176  cphipval2  25217  4cphipval2  25218  cphipval  25219  mbfmulc2re  25624  mbfmulc2  25639  itg1addlem4  25675  itg1addlem5  25676  itg1mulc  25680  mbfmul  25702  itgcl  25760  itgcnlem  25766  iblmulc2  25807  itgmulc2  25810  itgabs  25811  itgsplit  25812  dvmulbr  25915  dvcmul  25920  dvcmulf  25921  dvexp  25929  dvmptcmul  25940  dvmptdiv  25950  dvexp3  25954  dvsincos  25957  cmvth  25967  cmvthOLD  25968  dvlipcn  25971  dvfsumabs  26001  dvfsumlem1  26004  ftc1lem4  26018  itgparts  26026  itgpowd  26029  plyf  26175  ply1termlem  26180  plyeq0lem  26187  plypf1  26189  plyaddlem1  26190  plymullem1  26191  coeeulem  26201  coeidlem  26214  coeid3  26217  plyco  26218  coemullem  26227  coemulhi  26231  coemulc  26232  dgrcolem2  26251  plycjlem  26253  plyrecj  26258  dvply1  26262  vieta1lem2  26290  vieta1  26291  elqaalem3  26300  aareccl  26305  aalioulem1  26311  taylfvallem1  26335  tayl0  26340  dvtaylp  26349  taylthlem2  26353  taylthlem2OLD  26354  psergf  26392  radcnvlem1  26393  dvradcnv  26401  psercn2  26403  psercn2OLD  26404  pserdvlem2  26409  pserdv2  26411  abelthlem4  26415  abelthlem5  26416  abelthlem6  26417  abelthlem7  26419  abelthlem9  26421  tanregt0  26519  efgh  26521  efabl  26530  efsubm  26531  cosargd  26588  abslogle  26598  tanarg  26599  advlogexp  26635  logtayllem  26639  logtayl  26640  cxpadd  26659  mulcxp  26665  cxpmul  26668  cxpmul2  26669  cxpmul2z  26671  abscxp  26672  abscxp2  26673  dvcxp2  26721  abscxpbnd  26734  root1eq1  26736  cxpeq  26738  angcan  26783  pythag  26798  ssscongptld  26803  affineequiv  26804  affineequiv2  26805  affineequiv3  26806  affineequiv4  26807  chordthmlem2  26814  chordthmlem3  26815  chordthmlem4  26816  chordthmlem5  26817  heron  26819  quad2  26820  quad  26821  dcubic1lem  26824  dcubic2  26825  dcubic1  26826  dcubic  26827  mcubic  26828  cubic2  26829  cubic  26830  binom4  26831  dquartlem1  26832  dquartlem2  26833  dquart  26834  quart1cl  26835  quart1lem  26836  quart1  26837  quartlem1  26838  quartlem2  26839  atantayl3  26920  leibpi  26923  birthdaylem2  26933  divsqrtsumo1  26965  cvxcl  26966  jensenlem2  26969  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  wilthlem2  27050  ftalem1  27054  ftalem2  27055  ftalem4  27057  ftalem5  27058  basellem2  27063  basellem3  27064  basellem8  27069  muinv  27174  fsumdvdsmul  27176  fsumdvdsmulOLD  27178  logfacrlim  27206  logexprlim  27207  perfectlem2  27212  bposlem9  27274  gausslemma2dlem4  27351  lgsquad2lem1  27366  2lgslem3b  27379  2lgslem3c  27380  2lgslem3d  27381  2sqlem3  27402  2sqmod  27418  rplogsumlem1  27466  dchrisumlem2  27472  dchrisumlem3  27473  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  dchrvmasum2if  27479  dchrvmasumlem3  27481  dchrvmasumiflem1  27483  dchrvmasumiflem2  27484  rpvmasum2  27494  dchrisum0lem1  27498  dchrisum0lem2a  27499  dchrisum0lem2  27500  dchrmusumlem  27504  dchrvmasumlem  27505  rplogsum  27509  mudivsum  27512  mulogsumlem  27513  mulogsum  27514  mulog2sumlem1  27516  mulog2sumlem2  27517  mulog2sumlem3  27518  vmalogdivsum  27521  logsqvma  27524  log2sumbnd  27526  selberglem1  27527  selberglem2  27528  selberglem3  27529  selberg  27530  selberg2lem  27532  selberg2  27533  selberg3lem1  27539  selberg3  27541  selberg4lem1  27542  selberg4  27543  pntrsumo1  27547  selbergr  27550  selberg3r  27551  selberg4r  27552  selberg34r  27553  pntsval2  27558  pntrlog2bndlem1  27559  pntrlog2bndlem2  27560  pntrlog2bndlem3  27561  pntrlog2bndlem4  27562  pntrlog2bndlem5  27563  pntrlog2bndlem6  27565  pntrlog2bnd  27566  pntlemb  27579  pntlemf  27587  pntlemo  27589  ostth2lem2  27616  ostth2lem3  27617  ttgcontlem1  28972  brbtwn2  28993  colinearalg  28998  ax5seglem2  29017  ax5seglem9  29025  axeuclidlem  29050  axcontlem2  29053  axcontlem4  29055  axcontlem7  29058  axcontlem8  29059  finsumvtxdg2ssteplem4  29637  ex-ind-dvds  30551  nrt2irr  30563  ipval2  30798  dipcl  30803  riesz3i  32153  re0cj  32836  pythagreim  32838  quad3d  32842  indsumin  32941  dpfrac1  32971  wrdt2ind  33033  zringfrac  33634  ccfldsrarelvec  33836  ccfldextdgrr  33837  constrrtll  33896  constrrtlc1  33897  constrrtcclem  33899  constrrtcc  33900  constrconj  33910  constrfin  33911  constrelextdg2  33912  nn0constr  33926  constraddcl  33927  constrnegcl  33928  constrdircl  33930  iconstr  33931  constrremulcl  33932  constrrecl  33934  constrimcl  33935  constrmulcl  33936  constrreinvcl  33937  constrinvcl  33938  constrresqrtcl  33942  constrabscl  33943  constrsqrtcl  33944  cos9thpiminplylem1  33947  cos9thpiminplylem2  33948  cos9thpiminplylem3  33949  cos9thpiminply  33953  cos9thpinconstrlem1  33954  cos9thpinconstrlem2  33955  cos9thpinconstr  33956  cnre2csqima  34076  rmulccn  34093  dya2icoseg  34442  oddpwdc  34519  eulerpartlems  34525  eulerpartlemsv3  34526  eulerpartlemgs2  34545  signsplypnf  34715  itgexpif  34771  breprexplemc  34797  breprexp  34798  vtscl  34803  vtsprod  34804  circlemeth  34805  logdivsqrle  34815  hgt750lemf  34818  hgt750leme  34823  subfacval2  35390  subfaclim  35391  resconn  35449  iprodgam  35945  fwddifnp1  36368  knoppcnlem10  36775  knoppndvlem2  36786  knoppndvlem7  36791  knoppndvlem9  36793  knoppndvlem11  36795  knoppndvlem14  36798  knoppndvlem16  36800  knoppndvlem17  36801  bj-subcom  37635  bj-bary1lem  37637  bj-bary1lem1  37638  bj-bary1  37639  iblmulc2nc  38017  itgmulc2nc  38020  itgabsnc  38021  ftc1cnnclem  38023  ftc1anclem3  38027  dvasin  38036  areacirclem1  38040  areacirclem4  38043  areacirc  38045  cntotbnd  38128  3factsumint1  42471  3factsumint3  42473  3factsumint4  42474  lcmineqlem2  42480  lcmineqlem6  42484  lcmineqlem8  42486  lcmineqlem10  42488  lcmineqlem11  42489  lcmineqlem12  42490  lcmineqlem16  42494  lcmineqlem18  42496  lcmineqlem23  42501  3lexlogpow5ineq5  42510  aks4d1p1p1  42513  dvrelogpow2b  42518  aks4d1p1p6  42523  aks4d1p1p7  42524  aks4d1p1p5  42525  primrootscoprmpow  42549  posbezout  42550  primrootscoprbij  42552  primrootspoweq0  42556  2np3bcnp1  42594  2ap1caineq  42595  oddnumth  42754  nicomachus  42755  sumcubes  42756  ef11d  42782  cxp112d  42784  cxp111d  42785  readvrec2  42804  sn-addlid  42847  sn-it0e0  42859  sn-negex12  42860  sn-mul01  42869  sn-mullid  42879  sn-0tie0  42907  sn-mul02  42908  cnreeu  42946  fltnltalem  43106  fltnlta  43107  cu3addd  43124  3cubeslem2  43128  3cubeslem3l  43129  3cubeslem3r  43130  3cubeslem4  43132  pellexlem1  43272  pellexlem2  43273  pellexlem6  43277  pell1234qrne0  43296  pell1234qrreccl  43297  pell1234qrmulcl  43298  pell1234qrdich  43304  pell14qrdich  43312  pell1qrge1  43313  pell1qrgaplem  43316  rmspecsqrtnq  43349  qirropth  43351  rmxyneg  43363  rmxyadd  43364  rmxm1  43377  rmym1  43378  rmxluc  43379  rmyluc  43380  rmxdbl  43382  rmydbl  43383  jm2.18  43431  jm2.19lem1  43432  jm2.19lem2  43433  jm2.19lem4  43435  jm2.19  43436  jm2.22  43438  jm2.23  43439  jm2.25  43442  jm2.27c  43450  jm3.1lem2  43461  flcidc  43613  areaquad  43659  sqrtcval  44083  inductionexd  44597  imo72b2lem0  44607  int-leftdistd  44621  radcnvrat  44756  expgrowth  44777  binomcxplemwb  44790  binomcxplemnn0  44791  binomcxplemfrat  44793  binomcxplemdvbinom  44795  binomcxplemnotnn0  44798  sineq0ALT  45378  mul13d  45728  fperiodmullem  45751  fperiodmul  45752  divcan8d  45760  dmmcand  45761  ltdiv23neg  45838  mulc1cncfg  46034  mccllem  46042  clim1fr1  46046  mullimc  46061  mullimcf  46068  sumnnodd  46075  reclimc  46096  sinmulcos  46308  coskpi2  46309  cosknegpi  46312  dvsinexp  46354  dvasinbx  46363  dvdivf  46365  dvdivbd  46366  dvdivcncf  46370  dvbdfbdioolem2  46372  dvxpaek  46383  dvnxpaek  46385  dvnmul  46386  dvmptfprodlem  46387  dvnprodlem2  46390  itgsinexplem1  46397  itgsinexp  46398  itgcoscmulx  46412  itgsincmulx  46417  itgiccshift  46423  itgperiod  46424  stoweidlem1  46444  stoweidlem11  46454  stoweidlem13  46456  stoweidlem14  46457  stoweidlem17  46460  stoweidlem25  46468  stoweidlem26  46469  stoweidlem42  46485  wallispilem4  46511  wallispilem5  46512  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem8  46524  stirlinglem10  46526  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  dirker2re  46535  dirkerdenne0  46536  dirkerper  46539  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkeritg  46545  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem26  46576  fourierdlem30  46580  fourierdlem39  46589  fourierdlem42  46592  fourierdlem47  46596  fourierdlem48  46597  fourierdlem56  46605  fourierdlem57  46606  fourierdlem58  46607  fourierdlem62  46611  fourierdlem65  46614  fourierdlem66  46615  fourierdlem68  46617  fourierdlem72  46621  fourierdlem73  46622  fourierdlem76  46625  fourierdlem80  46629  fourierdlem83  46632  fourierdlem85  46634  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem95  46644  fourierdlem97  46646  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  elaa2lem  46676  etransclem8  46685  etransclem18  46695  etransclem20  46697  etransclem21  46698  etransclem23  46700  etransclem24  46701  etransclem31  46708  etransclem33  46710  etransclem35  46712  etransclem45  46722  etransclem46  46723  etransclem47  46724  etransclem48  46725  hoicvrrex  46999  hoidmvlelem2  47039  smfmullem1  47234  sigarim  47294  sigarac  47295  sigaraf  47296  sigarmf  47297  sigarls  47300  sigardiv  47304  sigarcol  47307  cevathlem1  47310  fldivmod  47789  fmtnorec2lem  48002  fmtnorec3  48008  fmtnorec4  48009  fmtnoprmfac1  48025  fmtnoprmfac2  48027  fmtnofac2lem  48028  sfprmdvdsmersenne  48063  lighneallem3  48067  quad1  48093  requad01  48094  requad2  48096  opeoALTV  48157  perfectALTVlem2  48195  fppr2odd  48204  0nodd  48643  2nodd  48645  2zlidl  48713  2zrngnmlid  48728  altgsumbcALT  48826  nn0sumshdiglemA  49092  nn0sumshdiglemB  49093  nn0sumshdiglem2  49095  nn0mullong  49098  itcovalt2lem2lem2  49147  ackval2  49155  submuladdmuld  49174  affinecomb2  49176  affineid  49177  1subrec1sub  49178  eenglngeehlnmlem1  49210  eenglngeehlnmlem2  49211  rrx2linest  49215  line2x  49227  line2y  49228  itschlc0yqe  49233  itsclc0yqsollem1  49235  itsclc0yqsol  49237  itscnhlc0xyqsol  49238  itschlc0xyqsol1  49239  itschlc0xyqsol  49240  itsclc0xyqsolr  49242  2itscplem1  49251  2itscplem2  49252  2itscplem3  49253  2itscp  49254  itscnhlinecirc02plem1  49255  itscnhlinecirc02plem2  49256  inlinecirc02plem  49259  inlinecirc02p  49260  i2linesd  50251  aacllem  50273  amgmwlem  50274  amgmlemALT  50275