Theorem mulcld 11194

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

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

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

This theorem is referenced by:  mul02lem1  11350  addrid  11354  cnegex  11355  kcnktkm1cn  11609  subaddmulsub  11641  mulsubaddmulsub  11642  receu  11823  divrec  11853  divcan3  11863  muldivdir  11875  subdivcomb1  11877  subdivcomb2  11878  divdivdiv  11883  divsubdiv  11898  lineq  12019  cru  12178  mul2lt0rlt0  13055  lincmb01cmp  13456  iccf1o  13457  flpmodeq  13836  moddiffl  13844  modvalp1  13852  modcyc  13868  modadd1  13870  modmuladdnn0  13880  modmul1  13889  modaddmulmod  13903  mulexpz  14067  expmulz  14073  binom3  14189  bernneq  14194  mulsubdivbinom2  14227  muldivbinom2  14228  remullem  15094  cjreim2  15127  absimle  15275  abstri  15297  sqreulem  15326  sqreu  15327  bhmafibid1cn  15432  bhmafibid2cn  15433  bhmafibid1  15434  bhmafibid2  15435  mulcn2  15562  reccn2  15563  o1rlimmul  15585  rlimmul  15611  isummulc2  15728  fsummulc2  15750  fsumparts  15772  binomlem  15795  binom1dif  15799  incexclem  15802  incexc  15803  incexc2  15804  pwdif  15834  geomulcvg  15842  mertenslem1  15850  mertens  15852  fprodmul  15926  fprodn0f  15957  iprodmul  15969  binomfallfaclem1  16005  binomfallfaclem2  16006  binomrisefac  16008  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  bpoly4  16025  efaddlem  16059  sinadd  16132  cosadd  16133  tanaddlem  16134  tanadd  16135  addsin  16138  sincossq  16144  sin2t  16145  dvds2ln  16259  oddm1even  16313  pwp1fsum  16361  flodddiv4  16385  sadadd2lem2  16420  bezoutlem2  16510  bezoutlem3  16511  bezoutlem4  16512  lcmgcdlem  16576  phiprmpw  16746  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  pcpremul  16814  pcaddlem  16859  fldivp1  16868  mul4sqlem  16924  4sqlem14  16929  vdwapun  16945  vdwlem2  16953  vdwlem6  16957  ablsimpgfindlem1  20039  zringlpirlem3  21374  znunit  21473  blcvx  24686  icopnfcnv  24840  cphipipcj  25100  cphipval2  25141  4cphipval2  25142  cphipval  25143  mbfmulc2re  25549  mbfmulc2  25564  itg1addlem4  25600  itg1addlem5  25601  itg1mulc  25605  mbfmul  25627  itgcl  25685  itgcnlem  25691  iblmulc2  25732  itgmulc2  25735  itgabs  25736  itgsplit  25737  dvmulbr  25841  dvmulbrOLD  25842  dvcmul  25847  dvcmulf  25848  dvexp  25857  dvmptcmul  25868  dvmptdiv  25878  dvexp3  25882  dvsincos  25885  cmvth  25895  cmvthOLD  25896  dvlipcn  25899  dvfsumabs  25929  dvfsumlem1  25932  ftc1lem4  25946  itgparts  25954  itgpowd  25957  plyf  26103  ply1termlem  26108  plyeq0lem  26115  plypf1  26117  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeidlem  26142  coeid3  26145  plyco  26146  coemullem  26155  coemulhi  26159  coemulc  26160  dgrcolem2  26180  plycjlem  26182  plyrecj  26187  dvply1  26191  vieta1lem2  26219  vieta1  26220  elqaalem3  26229  aareccl  26234  aalioulem1  26240  taylfvallem1  26264  tayl0  26269  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  psergf  26321  radcnvlem1  26322  dvradcnv  26330  psercn2  26332  psercn2OLD  26333  pserdvlem2  26338  pserdv2  26340  abelthlem4  26344  abelthlem5  26345  abelthlem6  26346  abelthlem7  26348  abelthlem9  26350  tanregt0  26448  efgh  26450  efabl  26459  efsubm  26460  cosargd  26517  abslogle  26527  tanarg  26528  advlogexp  26564  logtayllem  26568  logtayl  26569  cxpadd  26588  mulcxp  26594  cxpmul  26597  cxpmul2  26598  cxpmul2z  26600  abscxp  26601  abscxp2  26602  dvcxp2  26650  abscxpbnd  26663  root1eq1  26665  cxpeq  26667  angcan  26712  pythag  26727  ssscongptld  26732  affineequiv  26733  affineequiv2  26734  affineequiv3  26735  affineequiv4  26736  chordthmlem2  26743  chordthmlem3  26744  chordthmlem4  26745  chordthmlem5  26746  heron  26748  quad2  26749  quad  26750  dcubic1lem  26753  dcubic2  26754  dcubic1  26755  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  binom4  26760  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  atantayl3  26849  leibpi  26852  birthdaylem2  26862  divsqrtsumo1  26894  cvxcl  26895  jensenlem2  26898  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgamcvg2  26965  gamcvg  26966  gamcvg2lem  26969  wilthlem2  26979  ftalem1  26983  ftalem2  26984  ftalem4  26986  ftalem5  26987  basellem2  26992  basellem3  26993  basellem8  26998  muinv  27103  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  logfacrlim  27135  logexprlim  27136  perfectlem2  27141  bposlem9  27203  gausslemma2dlem4  27280  lgsquad2lem1  27295  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2sqlem3  27331  2sqmod  27347  rplogsumlem1  27395  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasum2if  27408  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  rpvmasum2  27423  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrmusumlem  27433  dchrvmasumlem  27434  rplogsum  27438  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem1  27445  mulog2sumlem2  27446  mulog2sumlem3  27447  vmalogdivsum  27450  logsqvma  27453  log2sumbnd  27455  selberglem1  27456  selberglem2  27457  selberglem3  27458  selberg  27459  selberg2lem  27461  selberg2  27462  selberg3lem1  27468  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrsumo1  27476  selbergr  27479  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntsval2  27487  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntlemb  27508  pntlemf  27516  pntlemo  27518  ostth2lem2  27545  ostth2lem3  27546  ttgcontlem1  28812  brbtwn2  28832  colinearalg  28837  ax5seglem2  28856  ax5seglem9  28864  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  finsumvtxdg2ssteplem4  29476  ex-ind-dvds  30390  nrt2irr  30402  ipval2  30636  dipcl  30641  riesz3i  31991  re0cj  32667  pythagreim  32669  quad3d  32673  indsum  32784  indsumin  32785  dpfrac1  32812  wrdt2ind  32875  zringfrac  33525  ccfldsrarelvec  33666  ccfldextdgrr  33667  constrrtll  33721  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  constrconj  33735  constrfin  33736  constrelextdg2  33737  nn0constr  33751  constraddcl  33752  constrnegcl  33753  constrdircl  33755  iconstr  33756  constrremulcl  33757  constrrecl  33759  constrimcl  33760  constrmulcl  33761  constrreinvcl  33762  constrinvcl  33763  constrresqrtcl  33767  constrabscl  33768  constrsqrtcl  33769  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminply  33778  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  cos9thpinconstr  33781  cnre2csqima  33901  rmulccn  33918  dya2icoseg  34268  oddpwdc  34345  eulerpartlems  34351  eulerpartlemsv3  34352  eulerpartlemgs2  34371  signsplypnf  34541  itgexpif  34597  breprexplemc  34623  breprexp  34624  vtscl  34629  vtsprod  34630  circlemeth  34631  logdivsqrle  34641  hgt750lemf  34644  hgt750leme  34649  subfacval2  35174  subfaclim  35175  resconn  35233  iprodgam  35729  fwddifnp1  36153  knoppcnlem10  36490  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem9  36508  knoppndvlem11  36510  knoppndvlem14  36513  knoppndvlem16  36515  knoppndvlem17  36516  bj-subcom  37296  bj-bary1lem  37298  bj-bary1lem1  37299  bj-bary1  37300  iblmulc2nc  37679  itgmulc2nc  37682  itgabsnc  37683  ftc1cnnclem  37685  ftc1anclem3  37689  dvasin  37698  areacirclem1  37702  areacirclem4  37705  areacirc  37707  cntotbnd  37790  3factsumint1  42009  3factsumint3  42011  3factsumint4  42012  lcmineqlem2  42018  lcmineqlem6  42022  lcmineqlem8  42024  lcmineqlem10  42026  lcmineqlem11  42027  lcmineqlem12  42028  lcmineqlem16  42032  lcmineqlem18  42034  lcmineqlem23  42039  3lexlogpow5ineq5  42048  aks4d1p1p1  42051  dvrelogpow2b  42056  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij  42090  primrootspoweq0  42094  2np3bcnp1  42132  2ap1caineq  42133  oddnumth  42299  nicomachus  42300  sumcubes  42301  ef11d  42327  cxp112d  42329  cxp111d  42330  readvrec2  42349  sn-addlid  42392  sn-it0e0  42404  sn-negex12  42405  sn-mul01  42414  sn-mullid  42424  sn-0tie0  42439  sn-mul02  42440  cnreeu  42478  fltnltalem  42650  fltnlta  42651  cu3addd  42669  3cubeslem2  42673  3cubeslem3l  42674  3cubeslem3r  42675  3cubeslem4  42677  pellexlem1  42817  pellexlem2  42818  pellexlem6  42822  pell1234qrne0  42841  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell1234qrdich  42849  pell14qrdich  42857  pell1qrge1  42858  pell1qrgaplem  42861  rmspecsqrtnq  42894  qirropth  42896  rmxyneg  42909  rmxyadd  42910  rmxm1  42923  rmym1  42924  rmxluc  42925  rmyluc  42926  rmxdbl  42928  rmydbl  42929  jm2.18  42977  jm2.19lem1  42978  jm2.19lem2  42979  jm2.19lem4  42981  jm2.19  42982  jm2.22  42984  jm2.23  42985  jm2.25  42988  jm2.27c  42996  jm3.1lem2  43007  flcidc  43159  areaquad  43205  sqrtcval  43630  inductionexd  44144  imo72b2lem0  44154  int-leftdistd  44168  radcnvrat  44303  expgrowth  44324  binomcxplemwb  44337  binomcxplemnn0  44338  binomcxplemfrat  44340  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  sineq0ALT  44926  mul13d  45278  fperiodmullem  45301  fperiodmul  45302  divcan8d  45310  dmmcand  45311  ltdiv23neg  45390  mulc1cncfg  45587  mccllem  45595  clim1fr1  45599  mullimc  45614  mullimcf  45621  sumnnodd  45628  reclimc  45651  sinmulcos  45863  coskpi2  45864  cosknegpi  45867  dvsinexp  45909  dvasinbx  45918  dvdivf  45920  dvdivbd  45921  dvdivcncf  45925  dvbdfbdioolem2  45927  dvxpaek  45938  dvnxpaek  45940  dvnmul  45941  dvmptfprodlem  45942  dvnprodlem2  45945  itgsinexplem1  45952  itgsinexp  45953  itgcoscmulx  45967  itgsincmulx  45972  itgiccshift  45978  itgperiod  45979  stoweidlem1  45999  stoweidlem11  46009  stoweidlem13  46011  stoweidlem14  46012  stoweidlem17  46015  stoweidlem25  46023  stoweidlem26  46024  stoweidlem42  46040  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  dirker2re  46090  dirkerdenne0  46091  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem26  46131  fourierdlem30  46135  fourierdlem39  46144  fourierdlem42  46147  fourierdlem47  46151  fourierdlem48  46152  fourierdlem56  46160  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem65  46169  fourierdlem66  46170  fourierdlem68  46172  fourierdlem72  46176  fourierdlem73  46177  fourierdlem76  46180  fourierdlem80  46184  fourierdlem83  46187  fourierdlem85  46189  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem95  46199  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  etransclem8  46240  etransclem18  46250  etransclem20  46252  etransclem21  46253  etransclem23  46255  etransclem24  46256  etransclem31  46263  etransclem33  46265  etransclem35  46267  etransclem45  46277  etransclem46  46278  etransclem47  46279  etransclem48  46280  hoicvrrex  46554  hoidmvlelem2  46594  smfmullem1  46789  sigarim  46849  sigarac  46850  sigaraf  46851  sigarmf  46852  sigarls  46855  sigardiv  46859  sigarcol  46862  cevathlem1  46865  fldivmod  47339  fmtnorec2lem  47543  fmtnorec3  47549  fmtnorec4  47550  fmtnoprmfac1  47566  fmtnoprmfac2  47568  fmtnofac2lem  47569  sfprmdvdsmersenne  47604  lighneallem3  47608  quad1  47621  requad01  47622  requad2  47624  opeoALTV  47685  perfectALTVlem2  47723  fppr2odd  47732  0nodd  48158  2nodd  48160  2zlidl  48228  2zrngnmlid  48243  altgsumbcALT  48341  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem2  48611  nn0mullong  48614  itcovalt2lem2lem2  48663  ackval2  48671  submuladdmuld  48690  affinecomb2  48692  affineid  48693  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2linest  48731  line2x  48743  line2y  48744  itschlc0yqe  48749  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  itsclc0xyqsolr  48758  2itscplem1  48767  2itscplem2  48768  2itscplem3  48769  2itscp  48770  itscnhlinecirc02plem1  48771  itscnhlinecirc02plem2  48772  inlinecirc02plem  48775  inlinecirc02p  48776  i2linesd  49768  aacllem  49790  amgmwlem  49791  amgmlemALT  49792