Theorem mulcld 10650

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  mul02lem1  10805  addid1  10809  cnegex  10810  kcnktkm1cn  11060  subaddmulsub  11092  mulsubaddmulsub  11093  receu  11274  divrec  11303  divcan3  11313  muldivdir  11322  subdivcomb1  11324  subdivcomb2  11325  divdivdiv  11330  divsubdiv  11345  lineq  11466  cru  11617  mul2lt0rlt0  12479  lincmb01cmp  12873  iccf1o  12874  flpmodeq  13237  moddiffl  13245  modvalp1  13253  modcyc  13269  modadd1  13271  modmuladdnn0  13278  modmul1  13287  modaddmulmod  13301  mulexpz  13465  expmulz  13471  binom3  13581  bernneq  13586  mulsubdivbinom2  13618  muldivbinom2  13619  remullem  14479  cjreim2  14512  absimle  14661  abstri  14682  sqreulem  14711  sqreu  14712  bhmafibid1cn  14815  bhmafibid2cn  14816  bhmafibid1  14817  bhmafibid2  14818  mulcn2  14944  reccn2  14945  o1rlimmul  14967  isummulc2  15109  fsummulc2  15131  fsumparts  15153  binomlem  15176  binom1dif  15180  incexclem  15183  incexc  15184  incexc2  15185  pwdif  15215  geomulcvg  15224  mertenslem1  15232  mertens  15234  fprodmul  15306  fprodn0f  15337  iprodmul  15349  binomfallfaclem1  15385  binomfallfaclem2  15386  binomrisefac  15388  bpolycl  15398  bpolysum  15399  bpolydiflem  15400  bpoly4  15405  efaddlem  15438  sinadd  15509  cosadd  15510  tanaddlem  15511  tanadd  15512  addsin  15515  sincossq  15521  sin2t  15522  dvds2ln  15634  oddm1even  15684  pwp1fsum  15732  flodddiv4  15754  sadadd2lem2  15789  bezoutlem2  15878  bezoutlem3  15879  bezoutlem4  15880  lcmgcdlem  15940  phiprmpw  16103  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  pcpremul  16170  pcaddlem  16214  fldivp1  16223  mul4sqlem  16279  4sqlem14  16284  vdwapun  16300  vdwlem2  16308  vdwlem6  16312  ablsimpgfindlem1  19222  zringlpirlem3  20179  znunit  20255  blcvx  23403  icopnfcnv  23547  cphipipcj  23805  cphipval2  23845  4cphipval2  23846  cphipval  23847  mbfmulc2re  24252  mbfmulc2  24267  itg1addlem4  24303  itg1addlem5  24304  itg1mulc  24308  mbfmul  24330  itgcl  24387  itgcnlem  24393  iblmulc2  24434  itgmulc2  24437  itgabs  24438  itgsplit  24439  dvmulbr  24542  dvcmul  24547  dvcmulf  24548  dvexp  24556  dvmptcmul  24567  dvmptdiv  24577  dvexp3  24581  dvsincos  24584  cmvth  24594  dvlipcn  24597  dvfsumabs  24626  dvfsumlem1  24629  ftc1lem4  24642  itgparts  24650  itgpowd  24653  plyf  24795  ply1termlem  24800  plyeq0lem  24807  plypf1  24809  plyaddlem1  24810  plymullem1  24811  coeeulem  24821  coeidlem  24834  coeid3  24837  plyco  24838  coemullem  24847  coemulhi  24851  coemulc  24852  dgrcolem2  24871  plycjlem  24873  plyrecj  24876  dvply1  24880  vieta1lem2  24907  vieta1  24908  elqaalem3  24917  aareccl  24922  aalioulem1  24928  taylfvallem1  24952  tayl0  24957  dvtaylp  24965  taylthlem2  24969  psergf  25007  radcnvlem1  25008  dvradcnv  25016  psercn2  25018  pserdvlem2  25023  pserdv2  25025  abelthlem4  25029  abelthlem5  25030  abelthlem6  25031  abelthlem7  25033  abelthlem9  25035  tanregt0  25131  efgh  25133  efabl  25142  efsubm  25143  cosargd  25199  abslogle  25209  tanarg  25210  advlogexp  25246  logtayllem  25250  logtayl  25251  cxpadd  25270  mulcxp  25276  cxpmul  25279  cxpmul2  25280  cxpmul2z  25282  abscxp  25283  abscxp2  25284  dvcxp2  25330  abscxpbnd  25342  root1eq1  25344  cxpeq  25346  angcan  25388  pythag  25403  ssscongptld  25408  affineequiv  25409  affineequiv2  25410  affineequiv3  25411  affineequiv4  25412  chordthmlem2  25419  chordthmlem3  25420  chordthmlem4  25421  chordthmlem5  25422  heron  25424  quad2  25425  quad  25426  dcubic1lem  25429  dcubic2  25430  dcubic1  25431  dcubic  25432  mcubic  25433  cubic2  25434  cubic  25435  binom4  25436  dquartlem1  25437  dquartlem2  25438  dquart  25439  quart1cl  25440  quart1lem  25441  quart1  25442  quartlem1  25443  quartlem2  25444  atantayl3  25525  leibpi  25528  birthdaylem2  25538  divsqrtsumo1  25569  cvxcl  25570  jensenlem2  25573  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamgulm2  25621  lgamcvg2  25640  gamcvg  25641  gamcvg2lem  25644  wilthlem2  25654  ftalem1  25658  ftalem2  25659  ftalem4  25661  ftalem5  25662  basellem2  25667  basellem3  25668  basellem8  25673  muinv  25778  fsumdvdsmul  25780  logfacrlim  25808  logexprlim  25809  perfectlem2  25814  bposlem9  25876  gausslemma2dlem4  25953  lgsquad2lem1  25968  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2sqlem3  26004  2sqmod  26020  rplogsumlem1  26068  dchrisumlem2  26074  dchrisumlem3  26075  dchrmusum2  26078  dchrvmasumlem1  26079  dchrvmasum2lem  26080  dchrvmasum2if  26081  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  dchrvmasumiflem2  26086  rpvmasum2  26096  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrmusumlem  26106  dchrvmasumlem  26107  rplogsum  26111  mudivsum  26114  mulogsumlem  26115  mulogsum  26116  mulog2sumlem1  26118  mulog2sumlem2  26119  mulog2sumlem3  26120  vmalogdivsum  26123  logsqvma  26126  log2sumbnd  26128  selberglem1  26129  selberglem2  26130  selberglem3  26131  selberg  26132  selberg2lem  26134  selberg2  26135  selberg3lem1  26141  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrsumo1  26149  selbergr  26152  selberg3r  26153  selberg4r  26154  selberg34r  26155  pntsval2  26160  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntlemb  26181  pntlemf  26189  pntlemo  26191  ostth2lem2  26218  ostth2lem3  26219  ttgcontlem1  26679  brbtwn2  26699  colinearalg  26704  ax5seglem2  26723  ax5seglem9  26731  axeuclidlem  26756  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  finsumvtxdg2ssteplem4  27338  ex-ind-dvds  28246  ipval2  28490  dipcl  28495  riesz3i  29845  dpfrac1  30594  wrdt2ind  30653  ccfldsrarelvec  31144  ccfldextdgrr  31145  cnre2csqima  31264  rmulccn  31281  indsum  31390  indsumin  31391  dya2icoseg  31645  oddpwdc  31722  eulerpartlems  31728  eulerpartlemsv3  31729  eulerpartlemgs2  31748  signsplypnf  31930  itgexpif  31987  breprexplemc  32013  breprexp  32014  vtscl  32019  vtsprod  32020  circlemeth  32021  logdivsqrle  32031  hgt750lemf  32034  hgt750leme  32039  subfacval2  32547  subfaclim  32548  resconn  32606  iprodgam  33087  fwddifnp1  33739  knoppndvlem2  33965  knoppndvlem7  33970  knoppndvlem9  33972  knoppndvlem11  33974  knoppndvlem14  33977  knoppndvlem16  33979  knoppndvlem17  33980  bj-subcom  34722  bj-bary1lem  34724  bj-bary1lem1  34725  bj-bary1  34726  iblmulc2nc  35122  itgmulc2nc  35125  itgabsnc  35126  ftc1cnnclem  35128  ftc1anclem3  35132  dvasin  35141  areacirclem1  35145  areacirclem4  35148  areacirc  35150  cntotbnd  35234  3factsumint1  39309  3factsumint3  39311  3factsumint4  39312  lcmineqlem2  39318  lcmineqlem6  39322  lcmineqlem8  39324  lcmineqlem10  39326  lcmineqlem11  39327  lcmineqlem12  39328  lcmineqlem16  39332  lcmineqlem18  39334  lcmineqlem23  39339  aks4d1p1p1  39345  2np3bcnp1  39348  2ap1caineq  39349  sn-addid2  39542  sn-it0e0  39552  sn-negex12  39553  sn-mul01  39562  sn-mulid2  39572  sn-0tie0  39576  sn-mul02  39577  cnreeu  39593  fltnltalem  39618  fltnlta  39619  cu3addd  39621  3cubeslem2  39626  3cubeslem3l  39627  3cubeslem3r  39628  3cubeslem4  39630  pellexlem1  39770  pellexlem2  39771  pellexlem6  39775  pell1234qrne0  39794  pell1234qrreccl  39795  pell1234qrmulcl  39796  pell1234qrdich  39802  pell14qrdich  39810  pell1qrge1  39811  pell1qrgaplem  39814  rmspecsqrtnq  39847  qirropth  39849  rmxyneg  39861  rmxyadd  39862  rmxm1  39875  rmym1  39876  rmxluc  39877  rmyluc  39878  rmxdbl  39880  rmydbl  39881  jm2.18  39929  jm2.19lem1  39930  jm2.19lem2  39931  jm2.19lem4  39933  jm2.19  39934  jm2.22  39936  jm2.23  39937  jm2.25  39940  jm2.27c  39948  jm3.1lem2  39959  flcidc  40118  areaquad  40166  sqrtcval  40341  inductionexd  40858  imo72b2lem0  40869  int-leftdistd  40885  radcnvrat  41018  expgrowth  41039  binomcxplemwb  41052  binomcxplemnn0  41053  binomcxplemfrat  41055  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  sineq0ALT  41643  mul13d  41910  fperiodmullem  41935  fperiodmul  41936  divcan8d  41944  dmmcand  41945  ltdiv23neg  42030  mulc1cncfg  42231  mccllem  42239  clim1fr1  42243  mullimc  42258  mullimcf  42265  sumnnodd  42272  reclimc  42295  sinmulcos  42507  coskpi2  42508  cosknegpi  42511  dvsinexp  42553  dvasinbx  42562  dvdivf  42564  dvdivbd  42565  dvdivcncf  42569  dvbdfbdioolem2  42571  dvxpaek  42582  dvnxpaek  42584  dvnmul  42585  dvmptfprodlem  42586  dvnprodlem2  42589  itgsinexplem1  42596  itgsinexp  42597  itgcoscmulx  42611  itgsincmulx  42616  itgiccshift  42622  itgperiod  42623  stoweidlem1  42643  stoweidlem11  42653  stoweidlem13  42655  stoweidlem14  42656  stoweidlem17  42659  stoweidlem25  42667  stoweidlem26  42668  stoweidlem42  42684  wallispilem4  42710  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  wallispi2  42715  stirlinglem1  42716  stirlinglem3  42718  stirlinglem4  42719  stirlinglem5  42720  stirlinglem6  42721  stirlinglem7  42722  stirlinglem8  42723  stirlinglem10  42725  stirlinglem11  42726  stirlinglem12  42727  stirlinglem13  42728  stirlinglem14  42729  stirlinglem15  42730  dirker2re  42734  dirkerdenne0  42735  dirkerper  42738  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkeritg  42744  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem26  42775  fourierdlem30  42779  fourierdlem39  42788  fourierdlem42  42791  fourierdlem47  42795  fourierdlem48  42796  fourierdlem56  42804  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem65  42813  fourierdlem66  42814  fourierdlem68  42816  fourierdlem72  42820  fourierdlem73  42821  fourierdlem76  42824  fourierdlem80  42828  fourierdlem83  42831  fourierdlem85  42833  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem95  42843  fourierdlem97  42845  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  elaa2lem  42875  etransclem8  42884  etransclem18  42894  etransclem20  42896  etransclem21  42897  etransclem23  42899  etransclem24  42900  etransclem31  42907  etransclem33  42909  etransclem35  42911  etransclem45  42921  etransclem46  42922  etransclem47  42923  etransclem48  42924  hoicvrrex  43195  hoidmvlelem2  43235  smfmullem1  43423  sigarim  43465  sigarac  43466  sigaraf  43467  sigarmf  43468  sigarls  43471  sigardiv  43475  sigarcol  43478  cevathlem1  43481  fmtnorec2lem  44059  fmtnorec3  44065  fmtnorec4  44066  fmtnoprmfac1  44082  fmtnoprmfac2  44084  fmtnofac2lem  44085  sfprmdvdsmersenne  44121  lighneallem3  44125  quad1  44138  requad01  44139  requad2  44141  opeoALTV  44202  perfectALTVlem2  44240  fppr2odd  44249  0nodd  44430  2nodd  44432  2zlidl  44558  2zrngnmlid  44573  altgsumbcALT  44755  fldivmod  44932  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  nn0sumshdiglem2  45036  nn0mullong  45039  itcovalt2lem2lem2  45088  ackval2  45096  submuladdmuld  45115  affinecomb2  45117  affineid  45118  1subrec1sub  45119  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  rrx2linest  45156  line2x  45168  line2y  45169  itschlc0yqe  45174  itsclc0yqsollem1  45176  itsclc0yqsol  45178  itscnhlc0xyqsol  45179  itschlc0xyqsol1  45180  itschlc0xyqsol  45181  itsclc0xyqsolr  45183  2itscplem1  45192  2itscplem2  45193  2itscplem3  45194  2itscp  45195  itscnhlinecirc02plem1  45196  itscnhlinecirc02plem2  45197  inlinecirc02plem  45200  inlinecirc02p  45201  i2linesd  45307  aacllem  45329  amgmwlem  45330  amgmlemALT  45331