Theorem mulcld 11281

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

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

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

This theorem is referenced by:  mul02lem1  11437  addrid  11441  cnegex  11442  kcnktkm1cn  11694  subaddmulsub  11726  mulsubaddmulsub  11727  receu  11908  divrec  11938  divcan3  11948  muldivdir  11960  subdivcomb1  11962  subdivcomb2  11963  divdivdiv  11968  divsubdiv  11983  lineq  12104  cru  12258  mul2lt0rlt0  13137  lincmb01cmp  13535  iccf1o  13536  flpmodeq  13914  moddiffl  13922  modvalp1  13930  modcyc  13946  modadd1  13948  modmuladdnn0  13956  modmul1  13965  modaddmulmod  13979  mulexpz  14143  expmulz  14149  binom3  14263  bernneq  14268  mulsubdivbinom2  14301  muldivbinom2  14302  remullem  15167  cjreim2  15200  absimle  15348  abstri  15369  sqreulem  15398  sqreu  15399  bhmafibid1cn  15502  bhmafibid2cn  15503  bhmafibid1  15504  bhmafibid2  15505  mulcn2  15632  reccn2  15633  o1rlimmul  15655  rlimmul  15681  isummulc2  15798  fsummulc2  15820  fsumparts  15842  binomlem  15865  binom1dif  15869  incexclem  15872  incexc  15873  incexc2  15874  pwdif  15904  geomulcvg  15912  mertenslem1  15920  mertens  15922  fprodmul  15996  fprodn0f  16027  iprodmul  16039  binomfallfaclem1  16075  binomfallfaclem2  16076  binomrisefac  16078  bpolycl  16088  bpolysum  16089  bpolydiflem  16090  bpoly4  16095  efaddlem  16129  sinadd  16200  cosadd  16201  tanaddlem  16202  tanadd  16203  addsin  16206  sincossq  16212  sin2t  16213  dvds2ln  16326  oddm1even  16380  pwp1fsum  16428  flodddiv4  16452  sadadd2lem2  16487  bezoutlem2  16577  bezoutlem3  16578  bezoutlem4  16579  lcmgcdlem  16643  phiprmpw  16813  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem16  16868  pcpremul  16881  pcaddlem  16926  fldivp1  16935  mul4sqlem  16991  4sqlem14  16996  vdwapun  17012  vdwlem2  17020  vdwlem6  17024  ablsimpgfindlem1  20127  zringlpirlem3  21475  znunit  21582  blcvx  24819  icopnfcnv  24973  cphipipcj  25234  cphipval2  25275  4cphipval2  25276  cphipval  25277  mbfmulc2re  25683  mbfmulc2  25698  itg1addlem4  25734  itg1addlem5  25735  itg1mulc  25739  mbfmul  25761  itgcl  25819  itgcnlem  25825  iblmulc2  25866  itgmulc2  25869  itgabs  25870  itgsplit  25871  dvmulbr  25975  dvmulbrOLD  25976  dvcmul  25981  dvcmulf  25982  dvexp  25991  dvmptcmul  26002  dvmptdiv  26012  dvexp3  26016  dvsincos  26019  cmvth  26029  cmvthOLD  26030  dvlipcn  26033  dvfsumabs  26063  dvfsumlem1  26066  ftc1lem4  26080  itgparts  26088  itgpowd  26091  plyf  26237  ply1termlem  26242  plyeq0lem  26249  plypf1  26251  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeidlem  26276  coeid3  26279  plyco  26280  coemullem  26289  coemulhi  26293  coemulc  26294  dgrcolem2  26314  plycjlem  26316  plyrecj  26321  dvply1  26325  vieta1lem2  26353  vieta1  26354  elqaalem3  26363  aareccl  26368  aalioulem1  26374  taylfvallem1  26398  tayl0  26403  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  psergf  26455  radcnvlem1  26456  dvradcnv  26464  psercn2  26466  psercn2OLD  26467  pserdvlem2  26472  pserdv2  26474  abelthlem4  26478  abelthlem5  26479  abelthlem6  26480  abelthlem7  26482  abelthlem9  26484  tanregt0  26581  efgh  26583  efabl  26592  efsubm  26593  cosargd  26650  abslogle  26660  tanarg  26661  advlogexp  26697  logtayllem  26701  logtayl  26702  cxpadd  26721  mulcxp  26727  cxpmul  26730  cxpmul2  26731  cxpmul2z  26733  abscxp  26734  abscxp2  26735  dvcxp2  26783  abscxpbnd  26796  root1eq1  26798  cxpeq  26800  angcan  26845  pythag  26860  ssscongptld  26865  affineequiv  26866  affineequiv2  26867  affineequiv3  26868  affineequiv4  26869  chordthmlem2  26876  chordthmlem3  26877  chordthmlem4  26878  chordthmlem5  26879  heron  26881  quad2  26882  quad  26883  dcubic1lem  26886  dcubic2  26887  dcubic1  26888  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  binom4  26893  dquartlem1  26894  dquartlem2  26895  dquart  26896  quart1cl  26897  quart1lem  26898  quart1  26899  quartlem1  26900  quartlem2  26901  atantayl3  26982  leibpi  26985  birthdaylem2  26995  divsqrtsumo1  27027  cvxcl  27028  jensenlem2  27031  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  wilthlem2  27112  ftalem1  27116  ftalem2  27117  ftalem4  27119  ftalem5  27120  basellem2  27125  basellem3  27126  basellem8  27131  muinv  27236  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  logfacrlim  27268  logexprlim  27269  perfectlem2  27274  bposlem9  27336  gausslemma2dlem4  27413  lgsquad2lem1  27428  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2sqlem3  27464  2sqmod  27480  rplogsumlem1  27528  dchrisumlem2  27534  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrvmasum2if  27541  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  rpvmasum2  27556  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrmusumlem  27566  dchrvmasumlem  27567  rplogsum  27571  mudivsum  27574  mulogsumlem  27575  mulogsum  27576  mulog2sumlem1  27578  mulog2sumlem2  27579  mulog2sumlem3  27580  vmalogdivsum  27583  logsqvma  27586  log2sumbnd  27588  selberglem1  27589  selberglem2  27590  selberglem3  27591  selberg  27592  selberg2lem  27594  selberg2  27595  selberg3lem1  27601  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrsumo1  27609  selbergr  27612  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntsval2  27620  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntlemb  27641  pntlemf  27649  pntlemo  27651  ostth2lem2  27678  ostth2lem3  27679  ttgcontlem1  28899  brbtwn2  28920  colinearalg  28925  ax5seglem2  28944  ax5seglem9  28952  axeuclidlem  28977  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  finsumvtxdg2ssteplem4  29566  ex-ind-dvds  30480  nrt2irr  30492  ipval2  30726  dipcl  30731  riesz3i  32081  re0cj  32753  quad3d  32754  indsum  32846  indsumin  32847  dpfrac1  32874  wrdt2ind  32938  zringfrac  33582  ccfldsrarelvec  33721  ccfldextdgrr  33722  constrrtll  33772  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  constrconj  33786  constrfin  33787  constrelextdg2  33788  cnre2csqima  33910  rmulccn  33927  dya2icoseg  34279  oddpwdc  34356  eulerpartlems  34362  eulerpartlemsv3  34363  eulerpartlemgs2  34382  signsplypnf  34565  itgexpif  34621  breprexplemc  34647  breprexp  34648  vtscl  34653  vtsprod  34654  circlemeth  34655  logdivsqrle  34665  hgt750lemf  34668  hgt750leme  34673  subfacval2  35192  subfaclim  35193  resconn  35251  iprodgam  35742  fwddifnp1  36166  knoppcnlem10  36503  knoppndvlem2  36514  knoppndvlem7  36519  knoppndvlem9  36521  knoppndvlem11  36523  knoppndvlem14  36526  knoppndvlem16  36528  knoppndvlem17  36529  bj-subcom  37309  bj-bary1lem  37311  bj-bary1lem1  37312  bj-bary1  37313  iblmulc2nc  37692  itgmulc2nc  37695  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem3  37702  dvasin  37711  areacirclem1  37715  areacirclem4  37718  areacirc  37720  cntotbnd  37803  3factsumint1  42022  3factsumint3  42024  3factsumint4  42025  lcmineqlem2  42031  lcmineqlem6  42035  lcmineqlem8  42037  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem12  42041  lcmineqlem16  42045  lcmineqlem18  42047  lcmineqlem23  42052  3lexlogpow5ineq5  42061  aks4d1p1p1  42064  dvrelogpow2b  42069  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij  42103  primrootspoweq0  42107  2np3bcnp1  42145  2ap1caineq  42146  oddnumth  42345  nicomachus  42346  sumcubes  42347  ef11d  42375  cxp112d  42377  cxp111d  42378  readvrec2  42391  sn-addlid  42434  sn-it0e0  42445  sn-negex12  42446  sn-mul01  42455  sn-mullid  42465  sn-0tie0  42469  sn-mul02  42470  cnreeu  42500  fltnltalem  42672  fltnlta  42673  cu3addd  42691  3cubeslem2  42696  3cubeslem3l  42697  3cubeslem3r  42698  3cubeslem4  42700  pellexlem1  42840  pellexlem2  42841  pellexlem6  42845  pell1234qrne0  42864  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell1234qrdich  42872  pell14qrdich  42880  pell1qrge1  42881  pell1qrgaplem  42884  rmspecsqrtnq  42917  qirropth  42919  rmxyneg  42932  rmxyadd  42933  rmxm1  42946  rmym1  42947  rmxluc  42948  rmyluc  42949  rmxdbl  42951  rmydbl  42952  jm2.18  43000  jm2.19lem1  43001  jm2.19lem2  43002  jm2.19lem4  43004  jm2.19  43005  jm2.22  43007  jm2.23  43008  jm2.25  43011  jm2.27c  43019  jm3.1lem2  43030  flcidc  43182  areaquad  43228  sqrtcval  43654  inductionexd  44168  imo72b2lem0  44178  int-leftdistd  44192  radcnvrat  44333  expgrowth  44354  binomcxplemwb  44367  binomcxplemnn0  44368  binomcxplemfrat  44370  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  sineq0ALT  44957  mul13d  45291  fperiodmullem  45315  fperiodmul  45316  divcan8d  45324  dmmcand  45325  ltdiv23neg  45405  mulc1cncfg  45604  mccllem  45612  clim1fr1  45616  mullimc  45631  mullimcf  45638  sumnnodd  45645  reclimc  45668  sinmulcos  45880  coskpi2  45881  cosknegpi  45884  dvsinexp  45926  dvasinbx  45935  dvdivf  45937  dvdivbd  45938  dvdivcncf  45942  dvbdfbdioolem2  45944  dvxpaek  45955  dvnxpaek  45957  dvnmul  45958  dvmptfprodlem  45959  dvnprodlem2  45962  itgsinexplem1  45969  itgsinexp  45970  itgcoscmulx  45984  itgsincmulx  45989  itgiccshift  45995  itgperiod  45996  stoweidlem1  46016  stoweidlem11  46026  stoweidlem13  46028  stoweidlem14  46029  stoweidlem17  46032  stoweidlem25  46040  stoweidlem26  46041  stoweidlem42  46057  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  dirker2re  46107  dirkerdenne0  46108  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem26  46148  fourierdlem30  46152  fourierdlem39  46161  fourierdlem42  46164  fourierdlem47  46168  fourierdlem48  46169  fourierdlem56  46177  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem65  46186  fourierdlem66  46187  fourierdlem68  46189  fourierdlem72  46193  fourierdlem73  46194  fourierdlem76  46197  fourierdlem80  46201  fourierdlem83  46204  fourierdlem85  46206  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem95  46216  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  elaa2lem  46248  etransclem8  46257  etransclem18  46267  etransclem20  46269  etransclem21  46270  etransclem23  46272  etransclem24  46273  etransclem31  46280  etransclem33  46282  etransclem35  46284  etransclem45  46294  etransclem46  46295  etransclem47  46296  etransclem48  46297  hoicvrrex  46571  hoidmvlelem2  46611  smfmullem1  46806  sigarim  46866  sigarac  46867  sigaraf  46868  sigarmf  46869  sigarls  46872  sigardiv  46876  sigarcol  46879  cevathlem1  46882  fldivmod  47340  fmtnorec2lem  47529  fmtnorec3  47535  fmtnorec4  47536  fmtnoprmfac1  47552  fmtnoprmfac2  47554  fmtnofac2lem  47555  sfprmdvdsmersenne  47590  lighneallem3  47594  quad1  47607  requad01  47608  requad2  47610  opeoALTV  47671  perfectALTVlem2  47709  fppr2odd  47718  0nodd  48086  2nodd  48088  2zlidl  48156  2zrngnmlid  48171  altgsumbcALT  48269  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem2  48543  nn0mullong  48546  itcovalt2lem2lem2  48595  ackval2  48603  submuladdmuld  48622  affinecomb2  48624  affineid  48625  1subrec1sub  48626  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2linest  48663  line2x  48675  line2y  48676  itschlc0yqe  48681  itsclc0yqsollem1  48683  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  itsclc0xyqsolr  48690  2itscplem1  48699  2itscplem2  48700  2itscplem3  48701  2itscp  48702  itscnhlinecirc02plem1  48703  itscnhlinecirc02plem2  48704  inlinecirc02plem  48707  inlinecirc02p  48708  i2linesd  49298  aacllem  49320  amgmwlem  49321  amgmlemALT  49322