Theorem mulcld 10926

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

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

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

This theorem is referenced by:  mul02lem1  11081  addid1  11085  cnegex  11086  kcnktkm1cn  11336  subaddmulsub  11368  mulsubaddmulsub  11369  receu  11550  divrec  11579  divcan3  11589  muldivdir  11598  subdivcomb1  11600  subdivcomb2  11601  divdivdiv  11606  divsubdiv  11621  lineq  11742  cru  11895  mul2lt0rlt0  12761  lincmb01cmp  13156  iccf1o  13157  flpmodeq  13522  moddiffl  13530  modvalp1  13538  modcyc  13554  modadd1  13556  modmuladdnn0  13563  modmul1  13572  modaddmulmod  13586  mulexpz  13751  expmulz  13757  binom3  13867  bernneq  13872  mulsubdivbinom2  13904  muldivbinom2  13905  remullem  14767  cjreim2  14800  absimle  14949  abstri  14970  sqreulem  14999  sqreu  15000  bhmafibid1cn  15103  bhmafibid2cn  15104  bhmafibid1  15105  bhmafibid2  15106  mulcn2  15233  reccn2  15234  o1rlimmul  15256  rlimmul  15283  isummulc2  15402  fsummulc2  15424  fsumparts  15446  binomlem  15469  binom1dif  15473  incexclem  15476  incexc  15477  incexc2  15478  pwdif  15508  geomulcvg  15516  mertenslem1  15524  mertens  15526  fprodmul  15598  fprodn0f  15629  iprodmul  15641  binomfallfaclem1  15677  binomfallfaclem2  15678  binomrisefac  15680  bpolycl  15690  bpolysum  15691  bpolydiflem  15692  bpoly4  15697  efaddlem  15730  sinadd  15801  cosadd  15802  tanaddlem  15803  tanadd  15804  addsin  15807  sincossq  15813  sin2t  15814  dvds2ln  15926  oddm1even  15980  pwp1fsum  16028  flodddiv4  16050  sadadd2lem2  16085  bezoutlem2  16176  bezoutlem3  16177  bezoutlem4  16178  lcmgcdlem  16239  phiprmpw  16405  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem16  16459  pcpremul  16472  pcaddlem  16517  fldivp1  16526  mul4sqlem  16582  4sqlem14  16587  vdwapun  16603  vdwlem2  16611  vdwlem6  16615  ablsimpgfindlem1  19625  zringlpirlem3  20598  znunit  20683  blcvx  23867  icopnfcnv  24011  cphipipcj  24269  cphipval2  24310  4cphipval2  24311  cphipval  24312  mbfmulc2re  24717  mbfmulc2  24732  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  itg1mulc  24774  mbfmul  24796  itgcl  24853  itgcnlem  24859  iblmulc2  24900  itgmulc2  24903  itgabs  24904  itgsplit  24905  dvmulbr  25008  dvcmul  25013  dvcmulf  25014  dvexp  25022  dvmptcmul  25033  dvmptdiv  25043  dvexp3  25047  dvsincos  25050  cmvth  25060  dvlipcn  25063  dvfsumabs  25092  dvfsumlem1  25095  ftc1lem4  25108  itgparts  25116  itgpowd  25119  plyf  25264  ply1termlem  25269  plyeq0lem  25276  plypf1  25278  plyaddlem1  25279  plymullem1  25280  coeeulem  25290  coeidlem  25303  coeid3  25306  plyco  25307  coemullem  25316  coemulhi  25320  coemulc  25321  dgrcolem2  25340  plycjlem  25342  plyrecj  25345  dvply1  25349  vieta1lem2  25376  vieta1  25377  elqaalem3  25386  aareccl  25391  aalioulem1  25397  taylfvallem1  25421  tayl0  25426  dvtaylp  25434  taylthlem2  25438  psergf  25476  radcnvlem1  25477  dvradcnv  25485  psercn2  25487  pserdvlem2  25492  pserdv2  25494  abelthlem4  25498  abelthlem5  25499  abelthlem6  25500  abelthlem7  25502  abelthlem9  25504  tanregt0  25600  efgh  25602  efabl  25611  efsubm  25612  cosargd  25668  abslogle  25678  tanarg  25679  advlogexp  25715  logtayllem  25719  logtayl  25720  cxpadd  25739  mulcxp  25745  cxpmul  25748  cxpmul2  25749  cxpmul2z  25751  abscxp  25752  abscxp2  25753  dvcxp2  25799  abscxpbnd  25811  root1eq1  25813  cxpeq  25815  angcan  25857  pythag  25872  ssscongptld  25877  affineequiv  25878  affineequiv2  25879  affineequiv3  25880  affineequiv4  25881  chordthmlem2  25888  chordthmlem3  25889  chordthmlem4  25890  chordthmlem5  25891  heron  25893  quad2  25894  quad  25895  dcubic1lem  25898  dcubic2  25899  dcubic1  25900  dcubic  25901  mcubic  25902  cubic2  25903  cubic  25904  binom4  25905  dquartlem1  25906  dquartlem2  25907  dquart  25908  quart1cl  25909  quart1lem  25910  quart1  25911  quartlem1  25912  quartlem2  25913  atantayl3  25994  leibpi  25997  birthdaylem2  26007  divsqrtsumo1  26038  cvxcl  26039  jensenlem2  26042  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  wilthlem2  26123  ftalem1  26127  ftalem2  26128  ftalem4  26130  ftalem5  26131  basellem2  26136  basellem3  26137  basellem8  26142  muinv  26247  fsumdvdsmul  26249  logfacrlim  26277  logexprlim  26278  perfectlem2  26283  bposlem9  26345  gausslemma2dlem4  26422  lgsquad2lem1  26437  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2sqlem3  26473  2sqmod  26489  rplogsumlem1  26537  dchrisumlem2  26543  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasum2if  26550  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  dchrvmasumiflem2  26555  rpvmasum2  26565  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrmusumlem  26575  dchrvmasumlem  26576  rplogsum  26580  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem1  26587  mulog2sumlem2  26588  mulog2sumlem3  26589  vmalogdivsum  26592  logsqvma  26595  log2sumbnd  26597  selberglem1  26598  selberglem2  26599  selberglem3  26600  selberg  26601  selberg2lem  26603  selberg2  26604  selberg3lem1  26610  selberg3  26612  selberg4lem1  26613  selberg4  26614  pntrsumo1  26618  selbergr  26621  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntsval2  26629  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntlemb  26650  pntlemf  26658  pntlemo  26660  ostth2lem2  26687  ostth2lem3  26688  ttgcontlem1  27155  brbtwn2  27176  colinearalg  27181  ax5seglem2  27200  ax5seglem9  27208  axeuclidlem  27233  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  finsumvtxdg2ssteplem4  27818  ex-ind-dvds  28726  ipval2  28970  dipcl  28975  riesz3i  30325  dpfrac1  31068  wrdt2ind  31127  ccfldsrarelvec  31643  ccfldextdgrr  31644  cnre2csqima  31763  rmulccn  31780  indsum  31889  indsumin  31890  dya2icoseg  32144  oddpwdc  32221  eulerpartlems  32227  eulerpartlemsv3  32228  eulerpartlemgs2  32247  signsplypnf  32429  itgexpif  32486  breprexplemc  32512  breprexp  32513  vtscl  32518  vtsprod  32519  circlemeth  32520  logdivsqrle  32530  hgt750lemf  32533  hgt750leme  32538  subfacval2  33049  subfaclim  33050  resconn  33108  iprodgam  33614  fwddifnp1  34394  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem9  34627  knoppndvlem11  34629  knoppndvlem14  34632  knoppndvlem16  34634  knoppndvlem17  34635  bj-subcom  35406  bj-bary1lem  35408  bj-bary1lem1  35409  bj-bary1  35410  iblmulc2nc  35769  itgmulc2nc  35772  itgabsnc  35773  ftc1cnnclem  35775  ftc1anclem3  35779  dvasin  35788  areacirclem1  35792  areacirclem4  35795  areacirc  35797  cntotbnd  35881  3factsumint1  39957  3factsumint3  39959  3factsumint4  39960  lcmineqlem2  39966  lcmineqlem6  39970  lcmineqlem8  39972  lcmineqlem10  39974  lcmineqlem11  39975  lcmineqlem12  39976  lcmineqlem16  39980  lcmineqlem18  39982  lcmineqlem23  39987  3lexlogpow5ineq5  39996  aks4d1p1p1  39999  dvrelogpow2b  40004  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  2np3bcnp1  40028  2ap1caineq  40029  sn-addid2  40308  sn-it0e0  40318  sn-negex12  40319  sn-mul01  40328  sn-mulid2  40338  sn-0tie0  40342  sn-mul02  40343  cnreeu  40359  fltnltalem  40415  fltnlta  40416  cu3addd  40418  3cubeslem2  40423  3cubeslem3l  40424  3cubeslem3r  40425  3cubeslem4  40427  pellexlem1  40567  pellexlem2  40568  pellexlem6  40572  pell1234qrne0  40591  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell1234qrdich  40599  pell14qrdich  40607  pell1qrge1  40608  pell1qrgaplem  40611  rmspecsqrtnq  40644  qirropth  40646  rmxyneg  40658  rmxyadd  40659  rmxm1  40672  rmym1  40673  rmxluc  40674  rmyluc  40675  rmxdbl  40677  rmydbl  40678  jm2.18  40726  jm2.19lem1  40727  jm2.19lem2  40728  jm2.19lem4  40730  jm2.19  40731  jm2.22  40733  jm2.23  40734  jm2.25  40737  jm2.27c  40745  jm3.1lem2  40756  flcidc  40915  areaquad  40963  sqrtcval  41138  inductionexd  41654  imo72b2lem0  41665  int-leftdistd  41679  radcnvrat  41821  expgrowth  41842  binomcxplemwb  41855  binomcxplemnn0  41856  binomcxplemfrat  41858  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  sineq0ALT  42446  mul13d  42707  fperiodmullem  42732  fperiodmul  42733  divcan8d  42741  dmmcand  42742  ltdiv23neg  42824  mulc1cncfg  43020  mccllem  43028  clim1fr1  43032  mullimc  43047  mullimcf  43054  sumnnodd  43061  reclimc  43084  sinmulcos  43296  coskpi2  43297  cosknegpi  43300  dvsinexp  43342  dvasinbx  43351  dvdivf  43353  dvdivbd  43354  dvdivcncf  43358  dvbdfbdioolem2  43360  dvxpaek  43371  dvnxpaek  43373  dvnmul  43374  dvmptfprodlem  43375  dvnprodlem2  43378  itgsinexplem1  43385  itgsinexp  43386  itgcoscmulx  43400  itgsincmulx  43405  itgiccshift  43411  itgperiod  43412  stoweidlem1  43432  stoweidlem11  43442  stoweidlem13  43444  stoweidlem14  43445  stoweidlem17  43448  stoweidlem25  43456  stoweidlem26  43457  stoweidlem42  43473  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  dirker2re  43523  dirkerdenne0  43524  dirkerper  43527  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkeritg  43533  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem26  43564  fourierdlem30  43568  fourierdlem39  43577  fourierdlem42  43580  fourierdlem47  43584  fourierdlem48  43585  fourierdlem56  43593  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  fourierdlem65  43602  fourierdlem66  43603  fourierdlem68  43605  fourierdlem72  43609  fourierdlem73  43610  fourierdlem76  43613  fourierdlem80  43617  fourierdlem83  43620  fourierdlem85  43622  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem95  43632  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  elaa2lem  43664  etransclem8  43673  etransclem18  43683  etransclem20  43685  etransclem21  43686  etransclem23  43688  etransclem24  43689  etransclem31  43696  etransclem33  43698  etransclem35  43700  etransclem45  43710  etransclem46  43711  etransclem47  43712  etransclem48  43713  hoicvrrex  43984  hoidmvlelem2  44024  smfmullem1  44212  sigarim  44254  sigarac  44255  sigaraf  44256  sigarmf  44257  sigarls  44260  sigardiv  44264  sigarcol  44267  cevathlem1  44270  fmtnorec2lem  44882  fmtnorec3  44888  fmtnorec4  44889  fmtnoprmfac1  44905  fmtnoprmfac2  44907  fmtnofac2lem  44908  sfprmdvdsmersenne  44943  lighneallem3  44947  quad1  44960  requad01  44961  requad2  44963  opeoALTV  45024  perfectALTVlem2  45062  fppr2odd  45071  0nodd  45252  2nodd  45254  2zlidl  45380  2zrngnmlid  45395  altgsumbcALT  45577  fldivmod  45752  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  nn0sumshdiglem2  45856  nn0mullong  45859  itcovalt2lem2lem2  45908  ackval2  45916  submuladdmuld  45935  affinecomb2  45937  affineid  45938  1subrec1sub  45939  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2linest  45976  line2x  45988  line2y  45989  itschlc0yqe  45994  itsclc0yqsollem1  45996  itsclc0yqsol  45998  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  itsclc0xyqsolr  46003  2itscplem1  46012  2itscplem2  46013  2itscplem3  46014  2itscp  46015  itscnhlinecirc02plem1  46016  itscnhlinecirc02plem2  46017  inlinecirc02plem  46020  inlinecirc02p  46021  i2linesd  46369  aacllem  46391  amgmwlem  46392  amgmlemALT  46393