Theorem mulcld 11150

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022   · cmul 11029

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

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

This theorem is referenced by:  mul02lem1  11307  addrid  11311  cnegex  11312  kcnktkm1cn  11566  subaddmulsub  11598  mulsubaddmulsub  11599  receu  11780  divrec  11810  divcan3  11820  muldivdir  11832  subdivcomb1  11834  subdivcomb2  11835  divdivdiv  11840  divsubdiv  11855  lineq  11976  cru  12135  mul2lt0rlt0  13007  lincmb01cmp  13409  iccf1o  13410  flpmodeq  13792  moddiffl  13800  modvalp1  13808  modcyc  13824  modadd1  13826  modmuladdnn0  13836  modmul1  13845  modaddmulmod  13859  mulexpz  14023  expmulz  14029  binom3  14145  bernneq  14150  mulsubdivbinom2  14183  muldivbinom2  14184  remullem  15049  cjreim2  15082  absimle  15230  abstri  15252  sqreulem  15281  sqreu  15282  bhmafibid1cn  15387  bhmafibid2cn  15388  bhmafibid1  15389  bhmafibid2  15390  mulcn2  15517  reccn2  15518  o1rlimmul  15540  rlimmul  15566  isummulc2  15683  fsummulc2  15705  fsumparts  15727  binomlem  15750  binom1dif  15754  incexclem  15757  incexc  15758  incexc2  15759  pwdif  15789  geomulcvg  15797  mertenslem1  15805  mertens  15807  fprodmul  15881  fprodn0f  15912  iprodmul  15924  binomfallfaclem1  15960  binomfallfaclem2  15961  binomrisefac  15963  bpolycl  15973  bpolysum  15974  bpolydiflem  15975  bpoly4  15980  efaddlem  16014  sinadd  16087  cosadd  16088  tanaddlem  16089  tanadd  16090  addsin  16093  sincossq  16099  sin2t  16100  dvds2ln  16214  oddm1even  16268  pwp1fsum  16316  flodddiv4  16340  sadadd2lem2  16375  bezoutlem2  16465  bezoutlem3  16466  bezoutlem4  16467  lcmgcdlem  16531  phiprmpw  16701  pythagtriplem12  16752  pythagtriplem14  16754  pythagtriplem16  16756  pcpremul  16769  pcaddlem  16814  fldivp1  16823  mul4sqlem  16879  4sqlem14  16884  vdwapun  16900  vdwlem2  16908  vdwlem6  16912  ablsimpgfindlem1  20036  zringlpirlem3  21417  znunit  21516  blcvx  24740  icopnfcnv  24894  cphipipcj  25154  cphipval2  25195  4cphipval2  25196  cphipval  25197  mbfmulc2re  25603  mbfmulc2  25618  itg1addlem4  25654  itg1addlem5  25655  itg1mulc  25659  mbfmul  25681  itgcl  25739  itgcnlem  25745  iblmulc2  25786  itgmulc2  25789  itgabs  25790  itgsplit  25791  dvmulbr  25895  dvmulbrOLD  25896  dvcmul  25901  dvcmulf  25902  dvexp  25911  dvmptcmul  25922  dvmptdiv  25932  dvexp3  25936  dvsincos  25939  cmvth  25949  cmvthOLD  25950  dvlipcn  25953  dvfsumabs  25983  dvfsumlem1  25986  ftc1lem4  26000  itgparts  26008  itgpowd  26011  plyf  26157  ply1termlem  26162  plyeq0lem  26169  plypf1  26171  plyaddlem1  26172  plymullem1  26173  coeeulem  26183  coeidlem  26196  coeid3  26199  plyco  26200  coemullem  26209  coemulhi  26213  coemulc  26214  dgrcolem2  26234  plycjlem  26236  plyrecj  26241  dvply1  26245  vieta1lem2  26273  vieta1  26274  elqaalem3  26283  aareccl  26288  aalioulem1  26294  taylfvallem1  26318  tayl0  26323  dvtaylp  26332  taylthlem2  26336  taylthlem2OLD  26337  psergf  26375  radcnvlem1  26376  dvradcnv  26384  psercn2  26386  psercn2OLD  26387  pserdvlem2  26392  pserdv2  26394  abelthlem4  26398  abelthlem5  26399  abelthlem6  26400  abelthlem7  26402  abelthlem9  26404  tanregt0  26502  efgh  26504  efabl  26513  efsubm  26514  cosargd  26571  abslogle  26581  tanarg  26582  advlogexp  26618  logtayllem  26622  logtayl  26623  cxpadd  26642  mulcxp  26648  cxpmul  26651  cxpmul2  26652  cxpmul2z  26654  abscxp  26655  abscxp2  26656  dvcxp2  26704  abscxpbnd  26717  root1eq1  26719  cxpeq  26721  angcan  26766  pythag  26781  ssscongptld  26786  affineequiv  26787  affineequiv2  26788  affineequiv3  26789  affineequiv4  26790  chordthmlem2  26797  chordthmlem3  26798  chordthmlem4  26799  chordthmlem5  26800  heron  26802  quad2  26803  quad  26804  dcubic1lem  26807  dcubic2  26808  dcubic1  26809  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  binom4  26814  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  atantayl3  26903  leibpi  26906  birthdaylem2  26916  divsqrtsumo1  26948  cvxcl  26949  jensenlem2  26952  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem4  26996  lgamgulmlem5  26997  lgamgulmlem6  26998  lgamgulm2  27000  lgamcvg2  27019  gamcvg  27020  gamcvg2lem  27023  wilthlem2  27033  ftalem1  27037  ftalem2  27038  ftalem4  27040  ftalem5  27041  basellem2  27046  basellem3  27047  basellem8  27052  muinv  27157  fsumdvdsmul  27159  fsumdvdsmulOLD  27161  logfacrlim  27189  logexprlim  27190  perfectlem2  27195  bposlem9  27257  gausslemma2dlem4  27334  lgsquad2lem1  27349  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2sqlem3  27385  2sqmod  27401  rplogsumlem1  27449  dchrisumlem2  27455  dchrisumlem3  27456  dchrmusum2  27459  dchrvmasumlem1  27460  dchrvmasum2lem  27461  dchrvmasum2if  27462  dchrvmasumlem3  27464  dchrvmasumiflem1  27466  dchrvmasumiflem2  27467  rpvmasum2  27477  dchrisum0lem1  27481  dchrisum0lem2a  27482  dchrisum0lem2  27483  dchrmusumlem  27487  dchrvmasumlem  27488  rplogsum  27492  mudivsum  27495  mulogsumlem  27496  mulogsum  27497  mulog2sumlem1  27499  mulog2sumlem2  27500  mulog2sumlem3  27501  vmalogdivsum  27504  logsqvma  27507  log2sumbnd  27509  selberglem1  27510  selberglem2  27511  selberglem3  27512  selberg  27513  selberg2lem  27515  selberg2  27516  selberg3lem1  27522  selberg3  27524  selberg4lem1  27525  selberg4  27526  pntrsumo1  27530  selbergr  27533  selberg3r  27534  selberg4r  27535  selberg34r  27536  pntsval2  27541  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntlemb  27562  pntlemf  27570  pntlemo  27572  ostth2lem2  27599  ostth2lem3  27600  ttgcontlem1  28906  brbtwn2  28927  colinearalg  28932  ax5seglem2  28951  ax5seglem9  28959  axeuclidlem  28984  axcontlem2  28987  axcontlem4  28989  axcontlem7  28992  axcontlem8  28993  finsumvtxdg2ssteplem4  29571  ex-ind-dvds  30485  nrt2irr  30497  ipval2  30731  dipcl  30736  riesz3i  32086  re0cj  32772  pythagreim  32774  quad3d  32778  indsum  32891  indsumin  32892  dpfrac1  32922  wrdt2ind  32984  zringfrac  33584  ccfldsrarelvec  33777  ccfldextdgrr  33778  constrrtll  33837  constrrtlc1  33838  constrrtcclem  33840  constrrtcc  33841  constrconj  33851  constrfin  33852  constrelextdg2  33853  nn0constr  33867  constraddcl  33868  constrnegcl  33869  constrdircl  33871  iconstr  33872  constrremulcl  33873  constrrecl  33875  constrimcl  33876  constrmulcl  33877  constrreinvcl  33878  constrinvcl  33879  constrresqrtcl  33883  constrabscl  33884  constrsqrtcl  33885  cos9thpiminplylem1  33888  cos9thpiminplylem2  33889  cos9thpiminplylem3  33890  cos9thpiminply  33894  cos9thpinconstrlem1  33895  cos9thpinconstrlem2  33896  cos9thpinconstr  33897  cnre2csqima  34017  rmulccn  34034  dya2icoseg  34383  oddpwdc  34460  eulerpartlems  34466  eulerpartlemsv3  34467  eulerpartlemgs2  34486  signsplypnf  34656  itgexpif  34712  breprexplemc  34738  breprexp  34739  vtscl  34744  vtsprod  34745  circlemeth  34746  logdivsqrle  34756  hgt750lemf  34759  hgt750leme  34764  subfacval2  35330  subfaclim  35331  resconn  35389  iprodgam  35885  fwddifnp1  36308  knoppcnlem10  36645  knoppndvlem2  36656  knoppndvlem7  36661  knoppndvlem9  36663  knoppndvlem11  36665  knoppndvlem14  36668  knoppndvlem16  36670  knoppndvlem17  36671  bj-subcom  37452  bj-bary1lem  37454  bj-bary1lem1  37455  bj-bary1  37456  iblmulc2nc  37825  itgmulc2nc  37828  itgabsnc  37829  ftc1cnnclem  37831  ftc1anclem3  37835  dvasin  37844  areacirclem1  37848  areacirclem4  37851  areacirc  37853  cntotbnd  37936  3factsumint1  42214  3factsumint3  42216  3factsumint4  42217  lcmineqlem2  42223  lcmineqlem6  42227  lcmineqlem8  42229  lcmineqlem10  42231  lcmineqlem11  42232  lcmineqlem12  42233  lcmineqlem16  42237  lcmineqlem18  42239  lcmineqlem23  42244  3lexlogpow5ineq5  42253  aks4d1p1p1  42256  dvrelogpow2b  42261  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  primrootscoprmpow  42292  posbezout  42293  primrootscoprbij  42295  primrootspoweq0  42299  2np3bcnp1  42337  2ap1caineq  42338  oddnumth  42508  nicomachus  42509  sumcubes  42510  ef11d  42536  cxp112d  42538  cxp111d  42539  readvrec2  42558  sn-addlid  42601  sn-it0e0  42613  sn-negex12  42614  sn-mul01  42623  sn-mullid  42633  sn-0tie0  42648  sn-mul02  42649  cnreeu  42687  fltnltalem  42847  fltnlta  42848  cu3addd  42865  3cubeslem2  42869  3cubeslem3l  42870  3cubeslem3r  42871  3cubeslem4  42873  pellexlem1  43013  pellexlem2  43014  pellexlem6  43018  pell1234qrne0  43037  pell1234qrreccl  43038  pell1234qrmulcl  43039  pell1234qrdich  43045  pell14qrdich  43053  pell1qrge1  43054  pell1qrgaplem  43057  rmspecsqrtnq  43090  qirropth  43092  rmxyneg  43104  rmxyadd  43105  rmxm1  43118  rmym1  43119  rmxluc  43120  rmyluc  43121  rmxdbl  43123  rmydbl  43124  jm2.18  43172  jm2.19lem1  43173  jm2.19lem2  43174  jm2.19lem4  43176  jm2.19  43177  jm2.22  43179  jm2.23  43180  jm2.25  43183  jm2.27c  43191  jm3.1lem2  43202  flcidc  43354  areaquad  43400  sqrtcval  43824  inductionexd  44338  imo72b2lem0  44348  int-leftdistd  44362  radcnvrat  44497  expgrowth  44518  binomcxplemwb  44531  binomcxplemnn0  44532  binomcxplemfrat  44534  binomcxplemdvbinom  44536  binomcxplemnotnn0  44539  sineq0ALT  45119  mul13d  45470  fperiodmullem  45493  fperiodmul  45494  divcan8d  45502  dmmcand  45503  ltdiv23neg  45580  mulc1cncfg  45777  mccllem  45785  clim1fr1  45789  mullimc  45804  mullimcf  45811  sumnnodd  45818  reclimc  45839  sinmulcos  46051  coskpi2  46052  cosknegpi  46055  dvsinexp  46097  dvasinbx  46106  dvdivf  46108  dvdivbd  46109  dvdivcncf  46113  dvbdfbdioolem2  46115  dvxpaek  46126  dvnxpaek  46128  dvnmul  46129  dvmptfprodlem  46130  dvnprodlem2  46133  itgsinexplem1  46140  itgsinexp  46141  itgcoscmulx  46155  itgsincmulx  46160  itgiccshift  46166  itgperiod  46167  stoweidlem1  46187  stoweidlem11  46197  stoweidlem13  46199  stoweidlem14  46200  stoweidlem17  46203  stoweidlem25  46211  stoweidlem26  46212  stoweidlem42  46228  wallispilem4  46254  wallispilem5  46255  wallispi  46256  wallispi2lem1  46257  wallispi2lem2  46258  wallispi2  46259  stirlinglem1  46260  stirlinglem3  46262  stirlinglem4  46263  stirlinglem5  46264  stirlinglem6  46265  stirlinglem7  46266  stirlinglem8  46267  stirlinglem10  46269  stirlinglem11  46270  stirlinglem12  46271  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  dirker2re  46278  dirkerdenne0  46279  dirkerper  46282  dirkertrigeqlem1  46284  dirkertrigeqlem2  46285  dirkertrigeqlem3  46286  dirkertrigeq  46287  dirkeritg  46288  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem26  46319  fourierdlem30  46323  fourierdlem39  46332  fourierdlem42  46335  fourierdlem47  46339  fourierdlem48  46340  fourierdlem56  46348  fourierdlem57  46349  fourierdlem58  46350  fourierdlem62  46354  fourierdlem65  46357  fourierdlem66  46358  fourierdlem68  46360  fourierdlem72  46364  fourierdlem73  46365  fourierdlem76  46368  fourierdlem80  46372  fourierdlem83  46375  fourierdlem85  46377  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem95  46387  fourierdlem97  46389  fourierdlem101  46393  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  sqwvfoura  46414  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  elaa2lem  46419  etransclem8  46428  etransclem18  46438  etransclem20  46440  etransclem21  46441  etransclem23  46443  etransclem24  46444  etransclem31  46451  etransclem33  46453  etransclem35  46455  etransclem45  46465  etransclem46  46466  etransclem47  46467  etransclem48  46468  hoicvrrex  46742  hoidmvlelem2  46782  smfmullem1  46977  sigarim  47037  sigarac  47038  sigaraf  47039  sigarmf  47040  sigarls  47043  sigardiv  47047  sigarcol  47050  cevathlem1  47053  fldivmod  47526  fmtnorec2lem  47730  fmtnorec3  47736  fmtnorec4  47737  fmtnoprmfac1  47753  fmtnoprmfac2  47755  fmtnofac2lem  47756  sfprmdvdsmersenne  47791  lighneallem3  47795  quad1  47808  requad01  47809  requad2  47811  opeoALTV  47872  perfectALTVlem2  47910  fppr2odd  47919  0nodd  48358  2nodd  48360  2zlidl  48428  2zrngnmlid  48443  altgsumbcALT  48541  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  nn0sumshdiglem2  48810  nn0mullong  48813  itcovalt2lem2lem2  48862  ackval2  48870  submuladdmuld  48889  affinecomb2  48891  affineid  48892  1subrec1sub  48893  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  rrx2linest  48930  line2x  48942  line2y  48943  itschlc0yqe  48948  itsclc0yqsollem1  48950  itsclc0yqsol  48952  itscnhlc0xyqsol  48953  itschlc0xyqsol1  48954  itschlc0xyqsol  48955  itsclc0xyqsolr  48957  2itscplem1  48966  2itscplem2  48967  2itscplem3  48968  2itscp  48969  itscnhlinecirc02plem1  48970  itscnhlinecirc02plem2  48971  inlinecirc02plem  48974  inlinecirc02p  48975  i2linesd  49966  aacllem  49988  amgmwlem  49989  amgmlemALT  49990