Theorem mulcld 11266

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138   · cmul 11145

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

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  mul02lem1  11422  addrid  11426  cnegex  11427  kcnktkm1cn  11677  subaddmulsub  11709  mulsubaddmulsub  11710  receu  11891  divrec  11921  divcan3  11931  muldivdir  11940  subdivcomb1  11942  subdivcomb2  11943  divdivdiv  11948  divsubdiv  11963  lineq  12084  cru  12237  mul2lt0rlt0  13111  lincmb01cmp  13507  iccf1o  13508  flpmodeq  13875  moddiffl  13883  modvalp1  13891  modcyc  13907  modadd1  13909  modmuladdnn0  13916  modmul1  13925  modaddmulmod  13939  mulexpz  14103  expmulz  14109  binom3  14222  bernneq  14227  mulsubdivbinom2  14257  muldivbinom2  14258  remullem  15111  cjreim2  15144  absimle  15292  abstri  15313  sqreulem  15342  sqreu  15343  bhmafibid1cn  15446  bhmafibid2cn  15447  bhmafibid1  15448  bhmafibid2  15449  mulcn2  15576  reccn2  15577  o1rlimmul  15599  rlimmul  15626  isummulc2  15744  fsummulc2  15766  fsumparts  15788  binomlem  15811  binom1dif  15815  incexclem  15818  incexc  15819  incexc2  15820  pwdif  15850  geomulcvg  15858  mertenslem1  15866  mertens  15868  fprodmul  15940  fprodn0f  15971  iprodmul  15983  binomfallfaclem1  16019  binomfallfaclem2  16020  binomrisefac  16022  bpolycl  16032  bpolysum  16033  bpolydiflem  16034  bpoly4  16039  efaddlem  16073  sinadd  16144  cosadd  16145  tanaddlem  16146  tanadd  16147  addsin  16150  sincossq  16156  sin2t  16157  dvds2ln  16269  oddm1even  16323  pwp1fsum  16371  flodddiv4  16393  sadadd2lem2  16428  bezoutlem2  16519  bezoutlem3  16520  bezoutlem4  16521  lcmgcdlem  16580  phiprmpw  16748  pythagtriplem12  16798  pythagtriplem14  16800  pythagtriplem16  16802  pcpremul  16815  pcaddlem  16860  fldivp1  16869  mul4sqlem  16925  4sqlem14  16930  vdwapun  16946  vdwlem2  16954  vdwlem6  16958  ablsimpgfindlem1  20076  zringlpirlem3  21407  znunit  21514  blcvx  24758  icopnfcnv  24911  cphipipcj  25172  cphipval2  25213  4cphipval2  25214  cphipval  25215  mbfmulc2re  25621  mbfmulc2  25636  itg1addlem4  25672  itg1addlem4OLD  25673  itg1addlem5  25674  itg1mulc  25678  mbfmul  25700  itgcl  25757  itgcnlem  25763  iblmulc2  25804  itgmulc2  25807  itgabs  25808  itgsplit  25809  dvmulbr  25913  dvmulbrOLD  25914  dvcmul  25919  dvcmulf  25920  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  26177  ply1termlem  26182  plyeq0lem  26189  plypf1  26191  plyaddlem1  26192  plymullem1  26193  coeeulem  26203  coeidlem  26216  coeid3  26219  plyco  26220  coemullem  26229  coemulhi  26233  coemulc  26234  dgrcolem2  26254  plycjlem  26256  plyrecj  26259  dvply1  26263  vieta1lem2  26291  vieta1  26292  elqaalem3  26301  aareccl  26306  aalioulem1  26312  taylfvallem1  26336  tayl0  26341  dvtaylp  26350  taylthlem2  26354  taylthlem2OLD  26355  psergf  26393  radcnvlem1  26394  dvradcnv  26402  psercn2  26404  psercn2OLD  26405  pserdvlem2  26410  pserdv2  26412  abelthlem4  26416  abelthlem5  26417  abelthlem6  26418  abelthlem7  26420  abelthlem9  26422  tanregt0  26518  efgh  26520  efabl  26529  efsubm  26530  cosargd  26587  abslogle  26597  tanarg  26598  advlogexp  26634  logtayllem  26638  logtayl  26639  cxpadd  26658  mulcxp  26664  cxpmul  26667  cxpmul2  26668  cxpmul2z  26670  abscxp  26671  abscxp2  26672  dvcxp2  26720  abscxpbnd  26733  root1eq1  26735  cxpeq  26737  angcan  26779  pythag  26794  ssscongptld  26799  affineequiv  26800  affineequiv2  26801  affineequiv3  26802  affineequiv4  26803  chordthmlem2  26810  chordthmlem3  26811  chordthmlem4  26812  chordthmlem5  26813  heron  26815  quad2  26816  quad  26817  dcubic1lem  26820  dcubic2  26821  dcubic1  26822  dcubic  26823  mcubic  26824  cubic2  26825  cubic  26826  binom4  26827  dquartlem1  26828  dquartlem2  26829  dquart  26830  quart1cl  26831  quart1lem  26832  quart1  26833  quartlem1  26834  quartlem2  26835  atantayl3  26916  leibpi  26919  birthdaylem2  26929  divsqrtsumo1  26961  cvxcl  26962  jensenlem2  26965  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulmlem6  27011  lgamgulm2  27013  lgamcvg2  27032  gamcvg  27033  gamcvg2lem  27036  wilthlem2  27046  ftalem1  27050  ftalem2  27051  ftalem4  27053  ftalem5  27054  basellem2  27059  basellem3  27060  basellem8  27065  muinv  27170  fsumdvdsmul  27172  fsumdvdsmulOLD  27174  logfacrlim  27202  logexprlim  27203  perfectlem2  27208  bposlem9  27270  gausslemma2dlem4  27347  lgsquad2lem1  27362  2lgslem3b  27375  2lgslem3c  27376  2lgslem3d  27377  2sqlem3  27398  2sqmod  27414  rplogsumlem1  27462  dchrisumlem2  27468  dchrisumlem3  27469  dchrmusum2  27472  dchrvmasumlem1  27473  dchrvmasum2lem  27474  dchrvmasum2if  27475  dchrvmasumlem3  27477  dchrvmasumiflem1  27479  dchrvmasumiflem2  27480  rpvmasum2  27490  dchrisum0lem1  27494  dchrisum0lem2a  27495  dchrisum0lem2  27496  dchrmusumlem  27500  dchrvmasumlem  27501  rplogsum  27505  mudivsum  27508  mulogsumlem  27509  mulogsum  27510  mulog2sumlem1  27512  mulog2sumlem2  27513  mulog2sumlem3  27514  vmalogdivsum  27517  logsqvma  27520  log2sumbnd  27522  selberglem1  27523  selberglem2  27524  selberglem3  27525  selberg  27526  selberg2lem  27528  selberg2  27529  selberg3lem1  27535  selberg3  27537  selberg4lem1  27538  selberg4  27539  pntrsumo1  27543  selbergr  27546  selberg3r  27547  selberg4r  27548  selberg34r  27549  pntsval2  27554  pntrlog2bndlem1  27555  pntrlog2bndlem2  27556  pntrlog2bndlem3  27557  pntrlog2bndlem4  27558  pntrlog2bndlem5  27559  pntrlog2bndlem6  27561  pntrlog2bnd  27562  pntlemb  27575  pntlemf  27583  pntlemo  27585  ostth2lem2  27612  ostth2lem3  27613  ttgcontlem1  28767  brbtwn2  28788  colinearalg  28793  ax5seglem2  28812  ax5seglem9  28820  axeuclidlem  28845  axcontlem2  28848  axcontlem4  28850  axcontlem7  28853  axcontlem8  28854  finsumvtxdg2ssteplem4  29434  ex-ind-dvds  30343  nrt2irr  30355  ipval2  30589  dipcl  30594  riesz3i  31944  dpfrac1  32700  wrdt2ind  32763  zringfrac  33366  ccfldsrarelvec  33487  ccfldextdgrr  33488  cnre2csqima  33640  rmulccn  33657  indsum  33768  indsumin  33769  dya2icoseg  34025  oddpwdc  34102  eulerpartlems  34108  eulerpartlemsv3  34109  eulerpartlemgs2  34128  signsplypnf  34310  itgexpif  34366  breprexplemc  34392  breprexp  34393  vtscl  34398  vtsprod  34399  circlemeth  34400  logdivsqrle  34410  hgt750lemf  34413  hgt750leme  34418  subfacval2  34925  subfaclim  34926  resconn  34984  iprodgam  35464  fwddifnp1  35889  knoppcnlem10  36105  knoppndvlem2  36116  knoppndvlem7  36121  knoppndvlem9  36123  knoppndvlem11  36125  knoppndvlem14  36128  knoppndvlem16  36130  knoppndvlem17  36131  bj-subcom  36915  bj-bary1lem  36917  bj-bary1lem1  36918  bj-bary1  36919  iblmulc2nc  37286  itgmulc2nc  37289  itgabsnc  37290  ftc1cnnclem  37292  ftc1anclem3  37296  dvasin  37305  areacirclem1  37309  areacirclem4  37312  areacirc  37314  cntotbnd  37397  3factsumint1  41621  3factsumint3  41623  3factsumint4  41624  lcmineqlem2  41630  lcmineqlem6  41634  lcmineqlem8  41636  lcmineqlem10  41638  lcmineqlem11  41639  lcmineqlem12  41640  lcmineqlem16  41644  lcmineqlem18  41646  lcmineqlem23  41651  3lexlogpow5ineq5  41660  aks4d1p1p1  41663  dvrelogpow2b  41668  aks4d1p1p6  41673  aks4d1p1p7  41674  aks4d1p1p5  41675  primrootscoprmpow  41699  posbezout  41700  primrootscoprbij  41702  primrootspoweq0  41706  2np3bcnp1  41744  2ap1caineq  41745  oddnumth  42003  nicomachus  42004  sumcubes  42005  ef11d  42042  cxp112d  42044  cxp111d  42045  sn-addlid  42091  sn-it0e0  42102  sn-negex12  42103  sn-mul01  42112  sn-mullid  42122  sn-0tie0  42126  sn-mul02  42127  cnreeu  42155  fltnltalem  42218  fltnlta  42219  cu3addd  42239  3cubeslem2  42244  3cubeslem3l  42245  3cubeslem3r  42246  3cubeslem4  42248  pellexlem1  42388  pellexlem2  42389  pellexlem6  42393  pell1234qrne0  42412  pell1234qrreccl  42413  pell1234qrmulcl  42414  pell1234qrdich  42420  pell14qrdich  42428  pell1qrge1  42429  pell1qrgaplem  42432  rmspecsqrtnq  42465  qirropth  42467  rmxyneg  42480  rmxyadd  42481  rmxm1  42494  rmym1  42495  rmxluc  42496  rmyluc  42497  rmxdbl  42499  rmydbl  42500  jm2.18  42548  jm2.19lem1  42549  jm2.19lem2  42550  jm2.19lem4  42552  jm2.19  42553  jm2.22  42555  jm2.23  42556  jm2.25  42559  jm2.27c  42567  jm3.1lem2  42578  flcidc  42737  areaquad  42783  sqrtcval  43210  inductionexd  43724  imo72b2lem0  43734  int-leftdistd  43748  radcnvrat  43890  expgrowth  43911  binomcxplemwb  43924  binomcxplemnn0  43925  binomcxplemfrat  43927  binomcxplemdvbinom  43929  binomcxplemnotnn0  43932  sineq0ALT  44515  mul13d  44796  fperiodmullem  44820  fperiodmul  44821  divcan8d  44829  dmmcand  44830  ltdiv23neg  44911  mulc1cncfg  45112  mccllem  45120  clim1fr1  45124  mullimc  45139  mullimcf  45146  sumnnodd  45153  reclimc  45176  sinmulcos  45388  coskpi2  45389  cosknegpi  45392  dvsinexp  45434  dvasinbx  45443  dvdivf  45445  dvdivbd  45446  dvdivcncf  45450  dvbdfbdioolem2  45452  dvxpaek  45463  dvnxpaek  45465  dvnmul  45466  dvmptfprodlem  45467  dvnprodlem2  45470  itgsinexplem1  45477  itgsinexp  45478  itgcoscmulx  45492  itgsincmulx  45497  itgiccshift  45503  itgperiod  45504  stoweidlem1  45524  stoweidlem11  45534  stoweidlem13  45536  stoweidlem14  45537  stoweidlem17  45540  stoweidlem25  45548  stoweidlem26  45549  stoweidlem42  45565  wallispilem4  45591  wallispilem5  45592  wallispi  45593  wallispi2lem1  45594  wallispi2lem2  45595  wallispi2  45596  stirlinglem1  45597  stirlinglem3  45599  stirlinglem4  45600  stirlinglem5  45601  stirlinglem6  45602  stirlinglem7  45603  stirlinglem8  45604  stirlinglem10  45606  stirlinglem11  45607  stirlinglem12  45608  stirlinglem13  45609  stirlinglem14  45610  stirlinglem15  45611  dirker2re  45615  dirkerdenne0  45616  dirkerper  45619  dirkertrigeqlem1  45621  dirkertrigeqlem2  45622  dirkertrigeqlem3  45623  dirkertrigeq  45624  dirkeritg  45625  dirkercncflem2  45627  dirkercncflem4  45629  fourierdlem26  45656  fourierdlem30  45660  fourierdlem39  45669  fourierdlem42  45672  fourierdlem47  45676  fourierdlem48  45677  fourierdlem56  45685  fourierdlem57  45686  fourierdlem58  45687  fourierdlem62  45691  fourierdlem65  45694  fourierdlem66  45695  fourierdlem68  45697  fourierdlem72  45701  fourierdlem73  45702  fourierdlem76  45705  fourierdlem80  45709  fourierdlem83  45712  fourierdlem85  45714  fourierdlem89  45718  fourierdlem90  45719  fourierdlem91  45720  fourierdlem95  45724  fourierdlem97  45726  fourierdlem101  45730  fourierdlem103  45732  fourierdlem104  45733  fourierdlem111  45740  sqwvfoura  45751  sqwvfourb  45752  fourierswlem  45753  fouriersw  45754  elaa2lem  45756  etransclem8  45765  etransclem18  45775  etransclem20  45777  etransclem21  45778  etransclem23  45780  etransclem24  45781  etransclem31  45788  etransclem33  45790  etransclem35  45792  etransclem45  45802  etransclem46  45803  etransclem47  45804  etransclem48  45805  hoicvrrex  46079  hoidmvlelem2  46119  smfmullem1  46314  sigarim  46374  sigarac  46375  sigaraf  46376  sigarmf  46377  sigarls  46380  sigardiv  46384  sigarcol  46387  cevathlem1  46390  fmtnorec2lem  47016  fmtnorec3  47022  fmtnorec4  47023  fmtnoprmfac1  47039  fmtnoprmfac2  47041  fmtnofac2lem  47042  sfprmdvdsmersenne  47077  lighneallem3  47081  quad1  47094  requad01  47095  requad2  47097  opeoALTV  47158  perfectALTVlem2  47196  fppr2odd  47205  0nodd  47415  2nodd  47417  2zlidl  47485  2zrngnmlid  47500  altgsumbcALT  47600  fldivmod  47774  nn0sumshdiglemA  47875  nn0sumshdiglemB  47876  nn0sumshdiglem2  47878  nn0mullong  47881  itcovalt2lem2lem2  47930  ackval2  47938  submuladdmuld  47957  affinecomb2  47959  affineid  47960  1subrec1sub  47961  eenglngeehlnmlem1  47993  eenglngeehlnmlem2  47994  rrx2linest  47998  line2x  48010  line2y  48011  itschlc0yqe  48016  itsclc0yqsollem1  48018  itsclc0yqsol  48020  itscnhlc0xyqsol  48021  itschlc0xyqsol1  48022  itschlc0xyqsol  48023  itsclc0xyqsolr  48025  2itscplem1  48034  2itscplem2  48035  2itscplem3  48036  2itscp  48037  itscnhlinecirc02plem1  48038  itscnhlinecirc02plem2  48039  inlinecirc02plem  48042  inlinecirc02p  48043  i2linesd  48395  aacllem  48417  amgmwlem  48418  amgmlemALT  48419