Theorem mulcld 11152

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

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

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

This theorem is referenced by:  mul02lem1  11309  addrid  11313  cnegex  11314  kcnktkm1cn  11568  subaddmulsub  11600  mulsubaddmulsub  11601  receu  11782  divrec  11812  divcan3  11822  muldivdir  11834  subdivcomb1  11836  subdivcomb2  11837  divdivdiv  11842  divsubdiv  11857  lineq  11978  cru  12137  mul2lt0rlt0  13009  lincmb01cmp  13411  iccf1o  13412  flpmodeq  13794  moddiffl  13802  modvalp1  13810  modcyc  13826  modadd1  13828  modmuladdnn0  13838  modmul1  13847  modaddmulmod  13861  mulexpz  14025  expmulz  14031  binom3  14147  bernneq  14152  mulsubdivbinom2  14185  muldivbinom2  14186  remullem  15051  cjreim2  15084  absimle  15232  abstri  15254  sqreulem  15283  sqreu  15284  bhmafibid1cn  15389  bhmafibid2cn  15390  bhmafibid1  15391  bhmafibid2  15392  mulcn2  15519  reccn2  15520  o1rlimmul  15542  rlimmul  15568  isummulc2  15685  fsummulc2  15707  fsumparts  15729  binomlem  15752  binom1dif  15756  incexclem  15759  incexc  15760  incexc2  15761  pwdif  15791  geomulcvg  15799  mertenslem1  15807  mertens  15809  fprodmul  15883  fprodn0f  15914  iprodmul  15926  binomfallfaclem1  15962  binomfallfaclem2  15963  binomrisefac  15965  bpolycl  15975  bpolysum  15976  bpolydiflem  15977  bpoly4  15982  efaddlem  16016  sinadd  16089  cosadd  16090  tanaddlem  16091  tanadd  16092  addsin  16095  sincossq  16101  sin2t  16102  dvds2ln  16216  oddm1even  16270  pwp1fsum  16318  flodddiv4  16342  sadadd2lem2  16377  bezoutlem2  16467  bezoutlem3  16468  bezoutlem4  16469  lcmgcdlem  16533  phiprmpw  16703  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem16  16758  pcpremul  16771  pcaddlem  16816  fldivp1  16825  mul4sqlem  16881  4sqlem14  16886  vdwapun  16902  vdwlem2  16910  vdwlem6  16914  ablsimpgfindlem1  20038  zringlpirlem3  21419  znunit  21518  blcvx  24742  icopnfcnv  24896  cphipipcj  25156  cphipval2  25197  4cphipval2  25198  cphipval  25199  mbfmulc2re  25605  mbfmulc2  25620  itg1addlem4  25656  itg1addlem5  25657  itg1mulc  25661  mbfmul  25683  itgcl  25741  itgcnlem  25747  iblmulc2  25788  itgmulc2  25791  itgabs  25792  itgsplit  25793  dvmulbr  25897  dvmulbrOLD  25898  dvcmul  25903  dvcmulf  25904  dvexp  25913  dvmptcmul  25924  dvmptdiv  25934  dvexp3  25938  dvsincos  25941  cmvth  25951  cmvthOLD  25952  dvlipcn  25955  dvfsumabs  25985  dvfsumlem1  25988  ftc1lem4  26002  itgparts  26010  itgpowd  26013  plyf  26159  ply1termlem  26164  plyeq0lem  26171  plypf1  26173  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  coeidlem  26198  coeid3  26201  plyco  26202  coemullem  26211  coemulhi  26215  coemulc  26216  dgrcolem2  26236  plycjlem  26238  plyrecj  26243  dvply1  26247  vieta1lem2  26275  vieta1  26276  elqaalem3  26285  aareccl  26290  aalioulem1  26296  taylfvallem1  26320  tayl0  26325  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  psergf  26377  radcnvlem1  26378  dvradcnv  26386  psercn2  26388  psercn2OLD  26389  pserdvlem2  26394  pserdv2  26396  abelthlem4  26400  abelthlem5  26401  abelthlem6  26402  abelthlem7  26404  abelthlem9  26406  tanregt0  26504  efgh  26506  efabl  26515  efsubm  26516  cosargd  26573  abslogle  26583  tanarg  26584  advlogexp  26620  logtayllem  26624  logtayl  26625  cxpadd  26644  mulcxp  26650  cxpmul  26653  cxpmul2  26654  cxpmul2z  26656  abscxp  26657  abscxp2  26658  dvcxp2  26706  abscxpbnd  26719  root1eq1  26721  cxpeq  26723  angcan  26768  pythag  26783  ssscongptld  26788  affineequiv  26789  affineequiv2  26790  affineequiv3  26791  affineequiv4  26792  chordthmlem2  26799  chordthmlem3  26800  chordthmlem4  26801  chordthmlem5  26802  heron  26804  quad2  26805  quad  26806  dcubic1lem  26809  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  binom4  26816  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem1  26823  quartlem2  26824  atantayl3  26905  leibpi  26908  birthdaylem2  26918  divsqrtsumo1  26950  cvxcl  26951  jensenlem2  26954  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgamcvg2  27021  gamcvg  27022  gamcvg2lem  27025  wilthlem2  27035  ftalem1  27039  ftalem2  27040  ftalem4  27042  ftalem5  27043  basellem2  27048  basellem3  27049  basellem8  27054  muinv  27159  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  logfacrlim  27191  logexprlim  27192  perfectlem2  27197  bposlem9  27259  gausslemma2dlem4  27336  lgsquad2lem1  27351  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2sqlem3  27387  2sqmod  27403  rplogsumlem1  27451  dchrisumlem2  27457  dchrisumlem3  27458  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasum2if  27464  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  rpvmasum2  27479  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrmusumlem  27489  dchrvmasumlem  27490  rplogsum  27494  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  mulog2sumlem1  27501  mulog2sumlem2  27502  mulog2sumlem3  27503  vmalogdivsum  27506  logsqvma  27509  log2sumbnd  27511  selberglem1  27512  selberglem2  27513  selberglem3  27514  selberg  27515  selberg2lem  27517  selberg2  27518  selberg3lem1  27524  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrsumo1  27532  selbergr  27535  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntsval2  27543  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntlemb  27564  pntlemf  27572  pntlemo  27574  ostth2lem2  27601  ostth2lem3  27602  ttgcontlem1  28957  brbtwn2  28978  colinearalg  28983  ax5seglem2  29002  ax5seglem9  29010  axeuclidlem  29035  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  finsumvtxdg2ssteplem4  29622  ex-ind-dvds  30536  nrt2irr  30548  ipval2  30782  dipcl  30787  riesz3i  32137  re0cj  32823  pythagreim  32825  quad3d  32829  indsum  32942  indsumin  32943  dpfrac1  32973  wrdt2ind  33035  zringfrac  33635  ccfldsrarelvec  33828  ccfldextdgrr  33829  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  constrconj  33902  constrfin  33903  constrelextdg2  33904  nn0constr  33918  constraddcl  33919  constrnegcl  33920  constrdircl  33922  iconstr  33923  constrremulcl  33924  constrrecl  33926  constrimcl  33927  constrmulcl  33928  constrreinvcl  33929  constrinvcl  33930  constrresqrtcl  33934  constrabscl  33935  constrsqrtcl  33936  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cos9thpinconstr  33948  cnre2csqima  34068  rmulccn  34085  dya2icoseg  34434  oddpwdc  34511  eulerpartlems  34517  eulerpartlemsv3  34518  eulerpartlemgs2  34537  signsplypnf  34707  itgexpif  34763  breprexplemc  34789  breprexp  34790  vtscl  34795  vtsprod  34796  circlemeth  34797  logdivsqrle  34807  hgt750lemf  34810  hgt750leme  34815  subfacval2  35381  subfaclim  35382  resconn  35440  iprodgam  35936  fwddifnp1  36359  knoppcnlem10  36702  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem9  36720  knoppndvlem11  36722  knoppndvlem14  36725  knoppndvlem16  36727  knoppndvlem17  36728  bj-subcom  37513  bj-bary1lem  37515  bj-bary1lem1  37516  bj-bary1  37517  iblmulc2nc  37886  itgmulc2nc  37889  itgabsnc  37890  ftc1cnnclem  37892  ftc1anclem3  37896  dvasin  37905  areacirclem1  37909  areacirclem4  37912  areacirc  37914  cntotbnd  37997  3factsumint1  42275  3factsumint3  42277  3factsumint4  42278  lcmineqlem2  42284  lcmineqlem6  42288  lcmineqlem8  42290  lcmineqlem10  42292  lcmineqlem11  42293  lcmineqlem12  42294  lcmineqlem16  42298  lcmineqlem18  42300  lcmineqlem23  42305  3lexlogpow5ineq5  42314  aks4d1p1p1  42317  dvrelogpow2b  42322  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  primrootscoprmpow  42353  posbezout  42354  primrootscoprbij  42356  primrootspoweq0  42360  2np3bcnp1  42398  2ap1caineq  42399  oddnumth  42566  nicomachus  42567  sumcubes  42568  ef11d  42594  cxp112d  42596  cxp111d  42597  readvrec2  42616  sn-addlid  42659  sn-it0e0  42671  sn-negex12  42672  sn-mul01  42681  sn-mullid  42691  sn-0tie0  42706  sn-mul02  42707  cnreeu  42745  fltnltalem  42905  fltnlta  42906  cu3addd  42923  3cubeslem2  42927  3cubeslem3l  42928  3cubeslem3r  42929  3cubeslem4  42931  pellexlem1  43071  pellexlem2  43072  pellexlem6  43076  pell1234qrne0  43095  pell1234qrreccl  43096  pell1234qrmulcl  43097  pell1234qrdich  43103  pell14qrdich  43111  pell1qrge1  43112  pell1qrgaplem  43115  rmspecsqrtnq  43148  qirropth  43150  rmxyneg  43162  rmxyadd  43163  rmxm1  43176  rmym1  43177  rmxluc  43178  rmyluc  43179  rmxdbl  43181  rmydbl  43182  jm2.18  43230  jm2.19lem1  43231  jm2.19lem2  43232  jm2.19lem4  43234  jm2.19  43235  jm2.22  43237  jm2.23  43238  jm2.25  43241  jm2.27c  43249  jm3.1lem2  43260  flcidc  43412  areaquad  43458  sqrtcval  43882  inductionexd  44396  imo72b2lem0  44406  int-leftdistd  44420  radcnvrat  44555  expgrowth  44576  binomcxplemwb  44589  binomcxplemnn0  44590  binomcxplemfrat  44592  binomcxplemdvbinom  44594  binomcxplemnotnn0  44597  sineq0ALT  45177  mul13d  45528  fperiodmullem  45551  fperiodmul  45552  divcan8d  45560  dmmcand  45561  ltdiv23neg  45638  mulc1cncfg  45835  mccllem  45843  clim1fr1  45847  mullimc  45862  mullimcf  45869  sumnnodd  45876  reclimc  45897  sinmulcos  46109  coskpi2  46110  cosknegpi  46113  dvsinexp  46155  dvasinbx  46164  dvdivf  46166  dvdivbd  46167  dvdivcncf  46171  dvbdfbdioolem2  46173  dvxpaek  46184  dvnxpaek  46186  dvnmul  46187  dvmptfprodlem  46188  dvnprodlem2  46191  itgsinexplem1  46198  itgsinexp  46199  itgcoscmulx  46213  itgsincmulx  46218  itgiccshift  46224  itgperiod  46225  stoweidlem1  46245  stoweidlem11  46255  stoweidlem13  46257  stoweidlem14  46258  stoweidlem17  46261  stoweidlem25  46269  stoweidlem26  46270  stoweidlem42  46286  wallispilem4  46312  wallispilem5  46313  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem1  46318  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem6  46323  stirlinglem7  46324  stirlinglem8  46325  stirlinglem10  46327  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  dirker2re  46336  dirkerdenne0  46337  dirkerper  46340  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  dirkertrigeq  46345  dirkeritg  46346  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem26  46377  fourierdlem30  46381  fourierdlem39  46390  fourierdlem42  46393  fourierdlem47  46397  fourierdlem48  46398  fourierdlem56  46406  fourierdlem57  46407  fourierdlem58  46408  fourierdlem62  46412  fourierdlem65  46415  fourierdlem66  46416  fourierdlem68  46418  fourierdlem72  46422  fourierdlem73  46423  fourierdlem76  46426  fourierdlem80  46430  fourierdlem83  46433  fourierdlem85  46435  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem95  46445  fourierdlem97  46447  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  elaa2lem  46477  etransclem8  46486  etransclem18  46496  etransclem20  46498  etransclem21  46499  etransclem23  46501  etransclem24  46502  etransclem31  46509  etransclem33  46511  etransclem35  46513  etransclem45  46523  etransclem46  46524  etransclem47  46525  etransclem48  46526  hoicvrrex  46800  hoidmvlelem2  46840  smfmullem1  47035  sigarim  47095  sigarac  47096  sigaraf  47097  sigarmf  47098  sigarls  47101  sigardiv  47105  sigarcol  47108  cevathlem1  47111  fldivmod  47584  fmtnorec2lem  47788  fmtnorec3  47794  fmtnorec4  47795  fmtnoprmfac1  47811  fmtnoprmfac2  47813  fmtnofac2lem  47814  sfprmdvdsmersenne  47849  lighneallem3  47853  quad1  47866  requad01  47867  requad2  47869  opeoALTV  47930  perfectALTVlem2  47968  fppr2odd  47977  0nodd  48416  2nodd  48418  2zlidl  48486  2zrngnmlid  48501  altgsumbcALT  48599  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  nn0sumshdiglem2  48868  nn0mullong  48871  itcovalt2lem2lem2  48920  ackval2  48928  submuladdmuld  48947  affinecomb2  48949  affineid  48950  1subrec1sub  48951  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  rrx2linest  48988  line2x  49000  line2y  49001  itschlc0yqe  49006  itsclc0yqsollem1  49008  itsclc0yqsol  49010  itscnhlc0xyqsol  49011  itschlc0xyqsol1  49012  itschlc0xyqsol  49013  itsclc0xyqsolr  49015  2itscplem1  49024  2itscplem2  49025  2itscplem3  49026  2itscp  49027  itscnhlinecirc02plem1  49028  itscnhlinecirc02plem2  49029  inlinecirc02plem  49032  inlinecirc02p  49033  i2linesd  50024  aacllem  50046  amgmwlem  50047  amgmlemALT  50048