Theorem mulcld 10661

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mul02lem1  10816  addid1  10820  cnegex  10821  kcnktkm1cn  11071  subaddmulsub  11103  mulsubaddmulsub  11104  receu  11285  divrec  11314  divcan3  11324  muldivdir  11333  subdivcomb1  11335  subdivcomb2  11336  divdivdiv  11341  divsubdiv  11356  lineq  11477  cru  11630  mul2lt0rlt0  12492  lincmb01cmp  12882  iccf1o  12883  flpmodeq  13243  moddiffl  13251  modvalp1  13259  modcyc  13275  modadd1  13277  modmuladdnn0  13284  modmul1  13293  modaddmulmod  13307  mulexpz  13470  expmulz  13476  binom3  13586  bernneq  13591  mulsubdivbinom2  13623  muldivbinom2  13624  remullem  14487  cjreim2  14520  absimle  14669  abstri  14690  sqreulem  14719  sqreu  14720  bhmafibid1cn  14823  bhmafibid2cn  14824  bhmafibid1  14825  bhmafibid2  14826  mulcn2  14952  reccn2  14953  o1rlimmul  14975  isummulc2  15117  fsummulc2  15139  fsumparts  15161  binomlem  15184  binom1dif  15188  incexclem  15191  incexc  15192  incexc2  15193  pwdif  15223  geomulcvg  15232  mertenslem1  15240  mertens  15242  fprodmul  15314  fprodn0f  15345  iprodmul  15357  binomfallfaclem1  15393  binomfallfaclem2  15394  binomrisefac  15396  bpolycl  15406  bpolysum  15407  bpolydiflem  15408  bpoly4  15413  efaddlem  15446  sinadd  15517  cosadd  15518  tanaddlem  15519  tanadd  15520  addsin  15523  sincossq  15529  sin2t  15530  dvds2ln  15642  oddm1even  15692  pwp1fsum  15742  flodddiv4  15764  sadadd2lem2  15799  bezoutlem2  15888  bezoutlem3  15889  bezoutlem4  15890  lcmgcdlem  15950  phiprmpw  16113  pythagtriplem12  16163  pythagtriplem14  16165  pythagtriplem16  16167  pcpremul  16180  pcaddlem  16224  fldivp1  16233  mul4sqlem  16289  4sqlem14  16294  vdwapun  16310  vdwlem2  16318  vdwlem6  16322  ablsimpgfindlem1  19229  zringlpirlem3  20633  znunit  20710  blcvx  23406  icopnfcnv  23546  cphipipcj  23804  cphipval2  23844  4cphipval2  23845  cphipval  23846  mbfmulc2re  24249  mbfmulc2  24264  itg1addlem4  24300  itg1addlem5  24301  itg1mulc  24305  mbfmul  24327  itgcl  24384  itgcnlem  24390  iblmulc2  24431  itgmulc2  24434  itgabs  24435  itgsplit  24436  dvmulbr  24536  dvcmul  24541  dvcmulf  24542  dvexp  24550  dvmptcmul  24561  dvmptdiv  24571  dvexp3  24575  dvsincos  24578  cmvth  24588  dvlipcn  24591  dvfsumabs  24620  dvfsumlem1  24623  ftc1lem4  24636  itgparts  24644  plyf  24788  ply1termlem  24793  plyeq0lem  24800  plypf1  24802  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeidlem  24827  coeid3  24830  plyco  24831  coemullem  24840  coemulhi  24844  coemulc  24845  dgrcolem2  24864  plycjlem  24866  plyrecj  24869  dvply1  24873  vieta1lem2  24900  vieta1  24901  elqaalem3  24910  aareccl  24915  aalioulem1  24921  taylfvallem1  24945  tayl0  24950  dvtaylp  24958  taylthlem2  24962  psergf  25000  radcnvlem1  25001  dvradcnv  25009  psercn2  25011  pserdvlem2  25016  pserdv2  25018  abelthlem4  25022  abelthlem5  25023  abelthlem6  25024  abelthlem7  25026  abelthlem9  25028  tanregt0  25123  efgh  25125  efabl  25134  efsubm  25135  cosargd  25191  abslogle  25201  tanarg  25202  advlogexp  25238  logtayllem  25242  logtayl  25243  cxpadd  25262  mulcxp  25268  cxpmul  25271  cxpmul2  25272  cxpmul2z  25274  abscxp  25275  abscxp2  25276  dvcxp2  25322  abscxpbnd  25334  root1eq1  25336  cxpeq  25338  angcan  25380  pythag  25395  ssscongptld  25400  affineequiv  25401  affineequiv2  25402  affineequiv3  25403  affineequiv4  25404  chordthmlem2  25411  chordthmlem3  25412  chordthmlem4  25413  chordthmlem5  25414  heron  25416  quad2  25417  quad  25418  dcubic1lem  25421  dcubic2  25422  dcubic1  25423  dcubic  25424  mcubic  25425  cubic2  25426  cubic  25427  binom4  25428  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1cl  25432  quart1lem  25433  quart1  25434  quartlem1  25435  quartlem2  25436  atantayl3  25517  leibpi  25520  birthdaylem2  25530  divsqrtsumo1  25561  cvxcl  25562  jensenlem2  25565  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamgulm2  25613  lgamcvg2  25632  gamcvg  25633  gamcvg2lem  25636  wilthlem2  25646  ftalem1  25650  ftalem2  25651  ftalem4  25653  ftalem5  25654  basellem2  25659  basellem3  25660  basellem8  25665  muinv  25770  fsumdvdsmul  25772  logfacrlim  25800  logexprlim  25801  perfectlem2  25806  bposlem9  25868  gausslemma2dlem4  25945  lgsquad2lem1  25960  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2sqlem3  25996  2sqmod  26012  rplogsumlem1  26060  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasum2if  26073  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrvmasumiflem2  26078  rpvmasum2  26088  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrmusumlem  26098  dchrvmasumlem  26099  rplogsum  26103  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  mulog2sumlem1  26110  mulog2sumlem2  26111  mulog2sumlem3  26112  vmalogdivsum  26115  logsqvma  26118  log2sumbnd  26120  selberglem1  26121  selberglem2  26122  selberglem3  26123  selberg  26124  selberg2lem  26126  selberg2  26127  selberg3lem1  26133  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  selbergr  26144  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntsval2  26152  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntlemb  26173  pntlemf  26181  pntlemo  26183  ostth2lem2  26210  ostth2lem3  26211  ttgcontlem1  26671  brbtwn2  26691  colinearalg  26696  ax5seglem2  26715  ax5seglem9  26723  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  finsumvtxdg2ssteplem4  27330  ex-ind-dvds  28240  ipval2  28484  dipcl  28489  riesz3i  29839  dpfrac1  30568  wrdt2ind  30627  ccfldsrarelvec  31056  ccfldextdgrr  31057  cnre2csqima  31154  rmulccn  31171  indsum  31280  indsumin  31281  dya2icoseg  31535  oddpwdc  31612  eulerpartlems  31618  eulerpartlemsv3  31619  eulerpartlemgs2  31638  signsplypnf  31820  itgexpif  31877  breprexplemc  31903  breprexp  31904  vtscl  31909  vtsprod  31910  circlemeth  31911  logdivsqrle  31921  hgt750lemf  31924  hgt750leme  31929  subfacval2  32434  subfaclim  32435  resconn  32493  iprodgam  32974  fwddifnp1  33626  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem9  33859  knoppndvlem11  33861  knoppndvlem14  33864  knoppndvlem16  33866  knoppndvlem17  33867  bj-subcom  34592  bj-bary1lem  34594  bj-bary1lem1  34595  bj-bary1  34596  iblmulc2nc  34972  itgmulc2nc  34975  itgabsnc  34976  ftc1cnnclem  34980  ftc1anclem3  34984  dvasin  34993  areacirclem1  34997  areacirclem4  35000  areacirc  35002  cntotbnd  35089  sn-addid2  39283  fltnltalem  39323  fltnlta  39324  cu3addd  39326  3cubeslem2  39331  3cubeslem3l  39332  3cubeslem3r  39333  3cubeslem4  39335  pellexlem1  39475  pellexlem2  39476  pellexlem6  39480  pell1234qrne0  39499  pell1234qrreccl  39500  pell1234qrmulcl  39501  pell1234qrdich  39507  pell14qrdich  39515  pell1qrge1  39516  pell1qrgaplem  39519  rmspecsqrtnq  39552  qirropth  39554  rmxyneg  39566  rmxyadd  39567  rmxm1  39580  rmym1  39581  rmxluc  39582  rmyluc  39583  rmxdbl  39585  rmydbl  39586  jm2.18  39634  jm2.19lem1  39635  jm2.19lem2  39636  jm2.19lem4  39638  jm2.19  39639  jm2.22  39641  jm2.23  39642  jm2.25  39645  jm2.27c  39653  jm3.1lem2  39664  flcidc  39823  itgpowd  39870  areaquad  39872  inductionexd  40554  imo72b2lem0  40565  int-leftdistd  40581  radcnvrat  40695  expgrowth  40716  binomcxplemwb  40729  binomcxplemnn0  40730  binomcxplemfrat  40732  binomcxplemdvbinom  40734  binomcxplemnotnn0  40737  sineq0ALT  41320  mul13d  41594  fperiodmullem  41619  fperiodmul  41620  divcan8d  41628  dmmcand  41629  ltdiv23neg  41715  mulc1cncfg  41919  mccllem  41927  clim1fr1  41931  mullimc  41946  mullimcf  41953  sumnnodd  41960  reclimc  41983  sinmulcos  42195  coskpi2  42196  cosknegpi  42199  dvsinexp  42244  dvasinbx  42254  dvdivf  42256  dvdivbd  42257  dvdivcncf  42261  dvbdfbdioolem2  42263  dvxpaek  42274  dvnxpaek  42276  dvnmul  42277  dvmptfprodlem  42278  dvnprodlem2  42281  itgsinexplem1  42288  itgsinexp  42289  itgcoscmulx  42303  itgsincmulx  42308  itgiccshift  42314  itgperiod  42315  stoweidlem1  42335  stoweidlem11  42345  stoweidlem13  42347  stoweidlem14  42348  stoweidlem17  42351  stoweidlem25  42359  stoweidlem26  42360  stoweidlem42  42376  wallispilem4  42402  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  wallispi2  42407  stirlinglem1  42408  stirlinglem3  42410  stirlinglem4  42411  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem8  42415  stirlinglem10  42417  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  stirlinglem14  42421  stirlinglem15  42422  dirker2re  42426  dirkerdenne0  42427  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkeritg  42436  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem26  42467  fourierdlem30  42471  fourierdlem39  42480  fourierdlem42  42483  fourierdlem47  42487  fourierdlem48  42488  fourierdlem56  42496  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem65  42505  fourierdlem66  42506  fourierdlem68  42508  fourierdlem72  42512  fourierdlem73  42513  fourierdlem76  42516  fourierdlem80  42520  fourierdlem83  42523  fourierdlem85  42525  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem95  42535  fourierdlem97  42537  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  elaa2lem  42567  etransclem8  42576  etransclem18  42586  etransclem20  42588  etransclem21  42589  etransclem23  42591  etransclem24  42592  etransclem31  42599  etransclem33  42601  etransclem35  42603  etransclem45  42613  etransclem46  42614  etransclem47  42615  etransclem48  42616  hoicvrrex  42887  hoidmvlelem2  42927  smfmullem1  43115  sigarim  43157  sigarac  43158  sigaraf  43159  sigarmf  43160  sigarls  43163  sigardiv  43167  sigarcol  43170  cevathlem1  43173  fmtnorec2lem  43753  fmtnorec3  43759  fmtnorec4  43760  fmtnoprmfac1  43776  fmtnoprmfac2  43778  fmtnofac2lem  43779  sfprmdvdsmersenne  43817  lighneallem3  43821  quad1  43834  requad01  43835  requad2  43837  opeoALTV  43898  perfectALTVlem2  43936  fppr2odd  43945  0nodd  44126  2nodd  44128  2zlidl  44254  2zrngnmlid  44269  altgsumbcALT  44450  fldivmod  44627  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  nn0sumshdiglem2  44731  nn0mullong  44734  submuladdmuld  44737  affinecomb2  44739  affineid  44740  1subrec1sub  44741  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrx2linest  44778  line2x  44790  line2y  44791  itschlc0yqe  44796  itsclc0yqsollem1  44798  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itschlc0xyqsol1  44802  itschlc0xyqsol  44803  itsclc0xyqsolr  44805  2itscplem1  44814  2itscplem2  44815  2itscplem3  44816  2itscp  44817  itscnhlinecirc02plem1  44818  itscnhlinecirc02plem2  44819  inlinecirc02plem  44822  inlinecirc02p  44823  i2linesd  44929  aacllem  44951  amgmwlem  44952  amgmlemALT  44953