Theorem mulcld 11310

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

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

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

This theorem is referenced by:  mul02lem1  11466  addrid  11470  cnegex  11471  kcnktkm1cn  11721  subaddmulsub  11753  mulsubaddmulsub  11754  receu  11935  divrec  11965  divcan3  11975  muldivdir  11987  subdivcomb1  11989  subdivcomb2  11990  divdivdiv  11995  divsubdiv  12010  lineq  12131  cru  12285  mul2lt0rlt0  13159  lincmb01cmp  13555  iccf1o  13556  flpmodeq  13925  moddiffl  13933  modvalp1  13941  modcyc  13957  modadd1  13959  modmuladdnn0  13966  modmul1  13975  modaddmulmod  13989  mulexpz  14153  expmulz  14159  binom3  14273  bernneq  14278  mulsubdivbinom2  14311  muldivbinom2  14312  remullem  15177  cjreim2  15210  absimle  15358  abstri  15379  sqreulem  15408  sqreu  15409  bhmafibid1cn  15512  bhmafibid2cn  15513  bhmafibid1  15514  bhmafibid2  15515  mulcn2  15642  reccn2  15643  o1rlimmul  15665  rlimmul  15692  isummulc2  15810  fsummulc2  15832  fsumparts  15854  binomlem  15877  binom1dif  15881  incexclem  15884  incexc  15885  incexc2  15886  pwdif  15916  geomulcvg  15924  mertenslem1  15932  mertens  15934  fprodmul  16008  fprodn0f  16039  iprodmul  16051  binomfallfaclem1  16087  binomfallfaclem2  16088  binomrisefac  16090  bpolycl  16100  bpolysum  16101  bpolydiflem  16102  bpoly4  16107  efaddlem  16141  sinadd  16212  cosadd  16213  tanaddlem  16214  tanadd  16215  addsin  16218  sincossq  16224  sin2t  16225  dvds2ln  16337  oddm1even  16391  pwp1fsum  16439  flodddiv4  16461  sadadd2lem2  16496  bezoutlem2  16587  bezoutlem3  16588  bezoutlem4  16589  lcmgcdlem  16653  phiprmpw  16823  pythagtriplem12  16873  pythagtriplem14  16875  pythagtriplem16  16877  pcpremul  16890  pcaddlem  16935  fldivp1  16944  mul4sqlem  17000  4sqlem14  17005  vdwapun  17021  vdwlem2  17029  vdwlem6  17033  ablsimpgfindlem1  20151  zringlpirlem3  21498  znunit  21605  blcvx  24839  icopnfcnv  24992  cphipipcj  25253  cphipval2  25294  4cphipval2  25295  cphipval  25296  mbfmulc2re  25702  mbfmulc2  25717  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  itg1mulc  25759  mbfmul  25781  itgcl  25839  itgcnlem  25845  iblmulc2  25886  itgmulc2  25889  itgabs  25890  itgsplit  25891  dvmulbr  25995  dvmulbrOLD  25996  dvcmul  26001  dvcmulf  26002  dvexp  26011  dvmptcmul  26022  dvmptdiv  26032  dvexp3  26036  dvsincos  26039  cmvth  26049  cmvthOLD  26050  dvlipcn  26053  dvfsumabs  26083  dvfsumlem1  26086  ftc1lem4  26100  itgparts  26108  itgpowd  26111  plyf  26257  ply1termlem  26262  plyeq0lem  26269  plypf1  26271  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coeidlem  26296  coeid3  26299  plyco  26300  coemullem  26309  coemulhi  26313  coemulc  26314  dgrcolem2  26334  plycjlem  26336  plyrecj  26339  dvply1  26343  vieta1lem2  26371  vieta1  26372  elqaalem3  26381  aareccl  26386  aalioulem1  26392  taylfvallem1  26416  tayl0  26421  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  psergf  26473  radcnvlem1  26474  dvradcnv  26482  psercn2  26484  psercn2OLD  26485  pserdvlem2  26490  pserdv2  26492  abelthlem4  26496  abelthlem5  26497  abelthlem6  26498  abelthlem7  26500  abelthlem9  26502  tanregt0  26599  efgh  26601  efabl  26610  efsubm  26611  cosargd  26668  abslogle  26678  tanarg  26679  advlogexp  26715  logtayllem  26719  logtayl  26720  cxpadd  26739  mulcxp  26745  cxpmul  26748  cxpmul2  26749  cxpmul2z  26751  abscxp  26752  abscxp2  26753  dvcxp2  26801  abscxpbnd  26814  root1eq1  26816  cxpeq  26818  angcan  26863  pythag  26878  ssscongptld  26883  affineequiv  26884  affineequiv2  26885  affineequiv3  26886  affineequiv4  26887  chordthmlem2  26894  chordthmlem3  26895  chordthmlem4  26896  chordthmlem5  26897  heron  26899  quad2  26900  quad  26901  dcubic1lem  26904  dcubic2  26905  dcubic1  26906  dcubic  26907  mcubic  26908  cubic2  26909  cubic  26910  binom4  26911  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem1  26918  quartlem2  26919  atantayl3  27000  leibpi  27003  birthdaylem2  27013  divsqrtsumo1  27045  cvxcl  27046  jensenlem2  27049  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgamcvg2  27116  gamcvg  27117  gamcvg2lem  27120  wilthlem2  27130  ftalem1  27134  ftalem2  27135  ftalem4  27137  ftalem5  27138  basellem2  27143  basellem3  27144  basellem8  27149  muinv  27254  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  logfacrlim  27286  logexprlim  27287  perfectlem2  27292  bposlem9  27354  gausslemma2dlem4  27431  lgsquad2lem1  27446  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2sqlem3  27482  2sqmod  27498  rplogsumlem1  27546  dchrisumlem2  27552  dchrisumlem3  27553  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasum2if  27559  dchrvmasumlem3  27561  dchrvmasumiflem1  27563  dchrvmasumiflem2  27564  rpvmasum2  27574  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrmusumlem  27584  dchrvmasumlem  27585  rplogsum  27589  mudivsum  27592  mulogsumlem  27593  mulogsum  27594  mulog2sumlem1  27596  mulog2sumlem2  27597  mulog2sumlem3  27598  vmalogdivsum  27601  logsqvma  27604  log2sumbnd  27606  selberglem1  27607  selberglem2  27608  selberglem3  27609  selberg  27610  selberg2lem  27612  selberg2  27613  selberg3lem1  27619  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrsumo1  27627  selbergr  27630  selberg3r  27631  selberg4r  27632  selberg34r  27633  pntsval2  27638  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntlemb  27659  pntlemf  27667  pntlemo  27669  ostth2lem2  27696  ostth2lem3  27697  ttgcontlem1  28917  brbtwn2  28938  colinearalg  28943  ax5seglem2  28962  ax5seglem9  28970  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  finsumvtxdg2ssteplem4  29584  ex-ind-dvds  30493  nrt2irr  30505  ipval2  30739  dipcl  30744  riesz3i  32094  re0cj  32756  quad3d  32757  dpfrac1  32856  wrdt2ind  32920  zringfrac  33547  ccfldsrarelvec  33681  ccfldextdgrr  33682  constrrtll  33722  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  constrconj  33735  constrfin  33736  constrelextdg2  33737  cnre2csqima  33857  rmulccn  33874  indsum  33985  indsumin  33986  dya2icoseg  34242  oddpwdc  34319  eulerpartlems  34325  eulerpartlemsv3  34326  eulerpartlemgs2  34345  signsplypnf  34527  itgexpif  34583  breprexplemc  34609  breprexp  34610  vtscl  34615  vtsprod  34616  circlemeth  34617  logdivsqrle  34627  hgt750lemf  34630  hgt750leme  34635  subfacval2  35155  subfaclim  35156  resconn  35214  iprodgam  35704  fwddifnp1  36129  knoppcnlem10  36468  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem9  36486  knoppndvlem11  36488  knoppndvlem14  36491  knoppndvlem16  36493  knoppndvlem17  36494  bj-subcom  37274  bj-bary1lem  37276  bj-bary1lem1  37277  bj-bary1  37278  iblmulc2nc  37645  itgmulc2nc  37648  itgabsnc  37649  ftc1cnnclem  37651  ftc1anclem3  37655  dvasin  37664  areacirclem1  37668  areacirclem4  37671  areacirc  37673  cntotbnd  37756  3factsumint1  41978  3factsumint3  41980  3factsumint4  41981  lcmineqlem2  41987  lcmineqlem6  41991  lcmineqlem8  41993  lcmineqlem10  41995  lcmineqlem11  41996  lcmineqlem12  41997  lcmineqlem16  42001  lcmineqlem18  42003  lcmineqlem23  42008  3lexlogpow5ineq5  42017  aks4d1p1p1  42020  dvrelogpow2b  42025  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  primrootscoprmpow  42056  posbezout  42057  primrootscoprbij  42059  primrootspoweq0  42063  2np3bcnp1  42101  2ap1caineq  42102  oddnumth  42299  nicomachus  42300  sumcubes  42301  ef11d  42327  cxp112d  42329  cxp111d  42330  sn-addlid  42380  sn-it0e0  42391  sn-negex12  42392  sn-mul01  42401  sn-mullid  42411  sn-0tie0  42415  sn-mul02  42416  cnreeu  42446  fltnltalem  42617  fltnlta  42618  cu3addd  42636  3cubeslem2  42641  3cubeslem3l  42642  3cubeslem3r  42643  3cubeslem4  42645  pellexlem1  42785  pellexlem2  42786  pellexlem6  42790  pell1234qrne0  42809  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell1234qrdich  42817  pell14qrdich  42825  pell1qrge1  42826  pell1qrgaplem  42829  rmspecsqrtnq  42862  qirropth  42864  rmxyneg  42877  rmxyadd  42878  rmxm1  42891  rmym1  42892  rmxluc  42893  rmyluc  42894  rmxdbl  42896  rmydbl  42897  jm2.18  42945  jm2.19lem1  42946  jm2.19lem2  42947  jm2.19lem4  42949  jm2.19  42950  jm2.22  42952  jm2.23  42953  jm2.25  42956  jm2.27c  42964  jm3.1lem2  42975  flcidc  43131  areaquad  43177  sqrtcval  43603  inductionexd  44117  imo72b2lem0  44127  int-leftdistd  44141  radcnvrat  44283  expgrowth  44304  binomcxplemwb  44317  binomcxplemnn0  44318  binomcxplemfrat  44320  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  sineq0ALT  44908  mul13d  45194  fperiodmullem  45218  fperiodmul  45219  divcan8d  45227  dmmcand  45228  ltdiv23neg  45309  mulc1cncfg  45510  mccllem  45518  clim1fr1  45522  mullimc  45537  mullimcf  45544  sumnnodd  45551  reclimc  45574  sinmulcos  45786  coskpi2  45787  cosknegpi  45790  dvsinexp  45832  dvasinbx  45841  dvdivf  45843  dvdivbd  45844  dvdivcncf  45848  dvbdfbdioolem2  45850  dvxpaek  45861  dvnxpaek  45863  dvnmul  45864  dvmptfprodlem  45865  dvnprodlem2  45868  itgsinexplem1  45875  itgsinexp  45876  itgcoscmulx  45890  itgsincmulx  45895  itgiccshift  45901  itgperiod  45902  stoweidlem1  45922  stoweidlem11  45932  stoweidlem13  45934  stoweidlem14  45935  stoweidlem17  45938  stoweidlem25  45946  stoweidlem26  45947  stoweidlem42  45963  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  dirker2re  46013  dirkerdenne0  46014  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem26  46054  fourierdlem30  46058  fourierdlem39  46067  fourierdlem42  46070  fourierdlem47  46074  fourierdlem48  46075  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem65  46092  fourierdlem66  46093  fourierdlem68  46095  fourierdlem72  46099  fourierdlem73  46100  fourierdlem76  46103  fourierdlem80  46107  fourierdlem83  46110  fourierdlem85  46112  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem95  46122  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  etransclem8  46163  etransclem18  46173  etransclem20  46175  etransclem21  46176  etransclem23  46178  etransclem24  46179  etransclem31  46186  etransclem33  46188  etransclem35  46190  etransclem45  46200  etransclem46  46201  etransclem47  46202  etransclem48  46203  hoicvrrex  46477  hoidmvlelem2  46517  smfmullem1  46712  sigarim  46772  sigarac  46773  sigaraf  46774  sigarmf  46775  sigarls  46778  sigardiv  46782  sigarcol  46785  cevathlem1  46788  fmtnorec2lem  47416  fmtnorec3  47422  fmtnorec4  47423  fmtnoprmfac1  47439  fmtnoprmfac2  47441  fmtnofac2lem  47442  sfprmdvdsmersenne  47477  lighneallem3  47481  quad1  47494  requad01  47495  requad2  47497  opeoALTV  47558  perfectALTVlem2  47596  fppr2odd  47605  0nodd  47893  2nodd  47895  2zlidl  47963  2zrngnmlid  47978  altgsumbcALT  48078  fldivmod  48252  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem2  48356  nn0mullong  48359  itcovalt2lem2lem2  48408  ackval2  48416  submuladdmuld  48435  affinecomb2  48437  affineid  48438  1subrec1sub  48439  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2linest  48476  line2x  48488  line2y  48489  itschlc0yqe  48494  itsclc0yqsollem1  48496  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itschlc0xyqsol  48501  itsclc0xyqsolr  48503  2itscplem1  48512  2itscplem2  48513  2itscplem3  48514  2itscp  48515  itscnhlinecirc02plem1  48516  itscnhlinecirc02plem2  48517  inlinecirc02plem  48520  inlinecirc02p  48521  i2linesd  48873  aacllem  48895  amgmwlem  48896  amgmlemALT  48897