Theorem mulcld 10460

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

Syntax hints:   → wi 4   ∈ wcel 2050  (class class class)co 6976  ℂcc 10333   · cmul 10340

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

This theorem depends on definitions:  df-bi 199  df-an 388

This theorem is referenced by:  mul02lem1  10616  addid1  10620  cnegex  10621  kcnktkm1cn  10872  subaddmulsub  10904  mulsubaddmulsub  10905  receu  11086  divrec  11115  divcan3  11125  muldivdir  11134  subdivcomb1  11136  subdivcomb2  11137  divdivdiv  11142  divsubdiv  11157  lineq  11278  cru  11431  mul2lt0rlt0  12308  lincmb01cmp  12697  iccf1o  12698  flpmodeq  13057  moddiffl  13065  modvalp1  13073  modcyc  13089  modadd1  13091  modmuladdnn0  13098  modmul1  13107  modaddmulmod  13121  mulexpz  13284  expmulz  13290  binom3  13400  bernneq  13405  mulsubdivbinom2  13437  muldivbinom2  13438  remullem  14348  cjreim2  14381  absimle  14530  abstri  14551  sqreulem  14580  sqreu  14581  bhmafibid1cn  14684  bhmafibid2cn  14685  bhmafibid1  14686  bhmafibid2  14687  mulcn2  14813  reccn2  14814  o1rlimmul  14836  isummulc2  14977  fsummulc2  14999  fsumparts  15021  binomlem  15044  binom1dif  15048  incexclem  15051  incexc  15052  incexc2  15053  pwdif  15083  geomulcvg  15092  mertenslem1  15100  mertens  15102  fprodmul  15174  fprodn0f  15205  iprodmul  15217  binomfallfaclem1  15253  binomfallfaclem2  15254  binomrisefac  15256  bpolycl  15266  bpolysum  15267  bpolydiflem  15268  bpoly4  15273  efaddlem  15306  sinadd  15377  cosadd  15378  tanaddlem  15379  tanadd  15380  addsin  15383  sincossq  15389  sin2t  15390  dvds2ln  15502  oddm1even  15552  pwp1fsum  15602  flodddiv4  15624  sadadd2lem2  15659  bezoutlem2  15744  bezoutlem3  15745  bezoutlem4  15746  lcmgcdlem  15806  phiprmpw  15969  pythagtriplem12  16019  pythagtriplem14  16021  pythagtriplem16  16023  pcpremul  16036  pcaddlem  16080  fldivp1  16089  mul4sqlem  16145  4sqlem14  16150  vdwapun  16166  vdwlem2  16174  vdwlem6  16178  zringlpirlem3  20335  znunit  20412  blcvx  23109  icopnfcnv  23249  cphipipcj  23507  cphipval2  23547  4cphipval2  23548  cphipval  23549  mbfmulc2re  23952  mbfmulc2  23967  itg1addlem4  24003  itg1addlem5  24004  itg1mulc  24008  mbfmul  24030  itgcl  24087  itgcnlem  24093  iblmulc2  24134  itgmulc2  24137  itgabs  24138  itgsplit  24139  dvmulbr  24239  dvcmul  24244  dvcmulf  24245  dvexp  24253  dvmptcmul  24264  dvmptdiv  24274  dvexp3  24278  dvsincos  24281  cmvth  24291  dvlipcn  24294  dvfsumabs  24323  dvfsumlem1  24326  ftc1lem4  24339  itgparts  24347  plyf  24491  ply1termlem  24496  plyeq0lem  24503  plypf1  24505  plyaddlem1  24506  plymullem1  24507  coeeulem  24517  coeidlem  24530  coeid3  24533  plyco  24534  coemullem  24543  coemulhi  24547  coemulc  24548  dgrcolem2  24567  plycjlem  24569  plyrecj  24572  dvply1  24576  vieta1lem2  24603  vieta1  24604  elqaalem3  24613  aareccl  24618  aalioulem1  24624  taylfvallem1  24648  tayl0  24653  dvtaylp  24661  taylthlem2  24665  psergf  24703  radcnvlem1  24704  dvradcnv  24712  psercn2  24714  pserdvlem2  24719  pserdv2  24721  abelthlem4  24725  abelthlem5  24726  abelthlem6  24727  abelthlem7  24729  abelthlem9  24731  tanregt0  24824  efgh  24826  efabl  24835  efsubm  24836  cosargd  24892  abslogle  24902  tanarg  24903  advlogexp  24939  logtayllem  24943  logtayl  24944  cxpadd  24963  mulcxp  24969  cxpmul  24972  cxpmul2  24973  cxpmul2z  24975  abscxp  24976  abscxp2  24977  dvcxp2  25023  abscxpbnd  25035  root1eq1  25037  cxpeq  25039  angcan  25081  pythag  25096  ssscongptld  25101  affineequiv  25102  affineequiv2  25103  affineequiv3  25104  affineequiv4  25105  chordthmlem2  25112  chordthmlem3  25113  chordthmlem4  25114  chordthmlem5  25115  heron  25117  quad2  25118  quad  25119  dcubic1lem  25122  dcubic2  25123  dcubic1  25124  dcubic  25125  mcubic  25126  cubic2  25127  cubic  25128  binom4  25129  dquartlem1  25130  dquartlem2  25131  dquart  25132  quart1cl  25133  quart1lem  25134  quart1  25135  quartlem1  25136  quartlem2  25137  atantayl3  25218  leibpi  25222  birthdaylem2  25232  divsqrtsumo1  25263  cvxcl  25264  jensenlem2  25267  lgamgulmlem2  25309  lgamgulmlem3  25310  lgamgulmlem4  25311  lgamgulmlem5  25312  lgamgulmlem6  25313  lgamgulm2  25315  lgamcvg2  25334  gamcvg  25335  gamcvg2lem  25338  wilthlem2  25348  ftalem1  25352  ftalem2  25353  ftalem4  25355  ftalem5  25356  basellem2  25361  basellem3  25362  basellem8  25367  muinv  25472  fsumdvdsmul  25474  logfacrlim  25502  logexprlim  25503  perfectlem2  25508  bposlem9  25570  gausslemma2dlem4  25647  lgsquad2lem1  25662  2lgslem3b  25675  2lgslem3c  25676  2lgslem3d  25677  2sqlem3  25698  2sqmod  25714  rplogsumlem1  25762  dchrisumlem2  25768  dchrisumlem3  25769  dchrmusum2  25772  dchrvmasumlem1  25773  dchrvmasum2lem  25774  dchrvmasum2if  25775  dchrvmasumlem3  25777  dchrvmasumiflem1  25779  dchrvmasumiflem2  25780  rpvmasum2  25790  dchrisum0lem1  25794  dchrisum0lem2a  25795  dchrisum0lem2  25796  dchrmusumlem  25800  dchrvmasumlem  25801  rplogsum  25805  mudivsum  25808  mulogsumlem  25809  mulogsum  25810  mulog2sumlem1  25812  mulog2sumlem2  25813  mulog2sumlem3  25814  vmalogdivsum  25817  logsqvma  25820  log2sumbnd  25822  selberglem1  25823  selberglem2  25824  selberglem3  25825  selberg  25826  selberg2lem  25828  selberg2  25829  selberg3lem1  25835  selberg3  25837  selberg4lem1  25838  selberg4  25839  pntrsumo1  25843  selbergr  25846  selberg3r  25847  selberg4r  25848  selberg34r  25849  pntsval2  25854  pntrlog2bndlem1  25855  pntrlog2bndlem2  25856  pntrlog2bndlem3  25857  pntrlog2bndlem4  25858  pntrlog2bndlem5  25859  pntrlog2bndlem6  25861  pntrlog2bnd  25862  pntlemb  25875  pntlemf  25883  pntlemo  25885  ostth2lem2  25912  ostth2lem3  25913  ttgcontlem1  26374  brbtwn2  26394  colinearalg  26399  ax5seglem2  26418  ax5seglem9  26426  axeuclidlem  26451  axcontlem2  26454  axcontlem4  26456  axcontlem7  26459  axcontlem8  26460  finsumvtxdg2ssteplem4  27033  ex-ind-dvds  28018  ipval2  28261  dipcl  28266  riesz3i  29620  dpfrac1  30314  ccfldsrarelvec  30682  ccfldextdgrr  30683  cnre2csqima  30795  rmulccn  30812  indsum  30921  indsumin  30922  dya2icoseg  31177  oddpwdc  31254  eulerpartlems  31260  eulerpartlemsv3  31261  eulerpartlemgs2  31280  signsplypnf  31463  itgexpif  31522  breprexplemc  31548  breprexp  31549  vtscl  31554  vtsprod  31555  circlemeth  31556  logdivsqrle  31566  hgt750lemf  31569  hgt750leme  31574  subfacval2  32016  subfaclim  32017  resconn  32075  iprodgam  32491  fwddifnp1  33144  knoppndvlem2  33369  knoppndvlem7  33374  knoppndvlem9  33376  knoppndvlem11  33378  knoppndvlem14  33381  knoppndvlem16  33383  knoppndvlem17  33384  bj-subcom  34034  bj-bary1lem  34036  bj-bary1lem1  34037  bj-bary1  34038  iblmulc2nc  34395  itgmulc2nc  34398  itgabsnc  34399  ftc1cnnclem  34403  ftc1anclem3  34407  dvasin  34416  areacirclem1  34420  areacirclem4  34423  areacirc  34425  cntotbnd  34513  fltnltalem  38678  fltnlta  38679  pellexlem1  38819  pellexlem2  38820  pellexlem6  38824  pell1234qrne0  38843  pell1234qrreccl  38844  pell1234qrmulcl  38845  pell1234qrdich  38851  pell14qrdich  38859  pell1qrge1  38860  pell1qrgaplem  38863  rmspecsqrtnq  38896  qirropth  38898  rmxyneg  38910  rmxyadd  38911  rmxm1  38924  rmym1  38925  rmxluc  38926  rmyluc  38927  rmxdbl  38929  rmydbl  38930  jm2.18  38978  jm2.19lem1  38979  jm2.19lem2  38980  jm2.19lem4  38982  jm2.19  38983  jm2.22  38985  jm2.23  38986  jm2.25  38989  jm2.27c  38997  jm3.1lem2  39008  flcidc  39167  itgpowd  39214  areaquad  39216  inductionexd  39865  imo72b2lem0  39877  int-leftdistd  39894  ablsimpgfindlem1  40040  radcnvrat  40059  expgrowth  40080  binomcxplemwb  40093  binomcxplemnn0  40094  binomcxplemfrat  40096  binomcxplemdvbinom  40098  binomcxplemnotnn0  40101  sineq0ALT  40687  mul13d  40972  fperiodmullem  40997  fperiodmul  40998  divcan8d  41006  dmmcand  41007  ltdiv23neg  41094  mulc1cncfg  41299  mccllem  41307  clim1fr1  41311  mullimc  41326  mullimcf  41333  sumnnodd  41340  reclimc  41363  sinmulcos  41574  coskpi2  41575  cosknegpi  41578  dvsinexp  41623  dvasinbx  41633  dvdivf  41635  dvdivbd  41636  dvdivcncf  41640  dvbdfbdioolem2  41642  dvxpaek  41653  dvnxpaek  41655  dvnmul  41656  dvmptfprodlem  41657  dvnprodlem2  41660  itgsinexplem1  41667  itgsinexp  41668  itgcoscmulx  41682  itgsincmulx  41687  itgiccshift  41693  itgperiod  41694  stoweidlem1  41715  stoweidlem11  41725  stoweidlem13  41727  stoweidlem14  41728  stoweidlem17  41731  stoweidlem25  41739  stoweidlem26  41740  stoweidlem42  41756  wallispilem4  41782  wallispilem5  41783  wallispi  41784  wallispi2lem1  41785  wallispi2lem2  41786  wallispi2  41787  stirlinglem1  41788  stirlinglem3  41790  stirlinglem4  41791  stirlinglem5  41792  stirlinglem6  41793  stirlinglem7  41794  stirlinglem8  41795  stirlinglem10  41797  stirlinglem11  41798  stirlinglem12  41799  stirlinglem13  41800  stirlinglem14  41801  stirlinglem15  41802  dirker2re  41806  dirkerdenne0  41807  dirkerper  41810  dirkertrigeqlem1  41812  dirkertrigeqlem2  41813  dirkertrigeqlem3  41814  dirkertrigeq  41815  dirkeritg  41816  dirkercncflem2  41818  dirkercncflem4  41820  fourierdlem26  41847  fourierdlem30  41851  fourierdlem39  41860  fourierdlem42  41863  fourierdlem47  41867  fourierdlem48  41868  fourierdlem56  41876  fourierdlem57  41877  fourierdlem58  41878  fourierdlem62  41882  fourierdlem65  41885  fourierdlem66  41886  fourierdlem68  41888  fourierdlem72  41892  fourierdlem73  41893  fourierdlem76  41896  fourierdlem80  41900  fourierdlem83  41903  fourierdlem85  41905  fourierdlem89  41909  fourierdlem90  41910  fourierdlem91  41911  fourierdlem95  41915  fourierdlem97  41917  fourierdlem101  41921  fourierdlem103  41923  fourierdlem104  41924  fourierdlem111  41931  sqwvfoura  41942  sqwvfourb  41943  fourierswlem  41944  fouriersw  41945  elaa2lem  41947  etransclem8  41956  etransclem18  41966  etransclem20  41968  etransclem21  41969  etransclem23  41971  etransclem24  41972  etransclem31  41979  etransclem33  41981  etransclem35  41983  etransclem45  41993  etransclem46  41994  etransclem47  41995  etransclem48  41996  hoicvrrex  42267  hoidmvlelem2  42307  smfmullem1  42495  sigarim  42537  sigarac  42538  sigaraf  42539  sigarmf  42540  sigarls  42543  sigardiv  42547  sigarcol  42550  cevathlem1  42553  fmtnorec2lem  43070  fmtnorec3  43076  fmtnorec4  43077  fmtnoprmfac1  43093  fmtnoprmfac2  43095  fmtnofac2lem  43096  sfprmdvdsmersenne  43134  lighneallem3  43138  quad1  43151  requad01  43152  requad2  43154  opeoALTV  43215  perfectALTVlem2  43253  fppr2odd  43262  0nodd  43443  2nodd  43445  2zlidl  43567  2zrngnmlid  43582  altgsumbcALT  43763  fldivmod  43944  nn0sumshdiglemA  44045  nn0sumshdiglemB  44046  nn0sumshdiglem2  44048  nn0mullong  44051  submuladdmuld  44054  affinecomb2  44056  affineid  44057  1subrec1sub  44058  eenglngeehlnmlem1  44090  eenglngeehlnmlem2  44091  rrx2linest  44095  line2x  44107  line2y  44108  itschlc0yqe  44113  itsclc0yqsollem1  44115  itsclc0yqsol  44117  itscnhlc0xyqsol  44118  itschlc0xyqsol1  44119  itschlc0xyqsol  44120  itsclc0xyqsolr  44122  2itscplem1  44131  2itscplem2  44132  2itscplem3  44133  2itscp  44134  itscnhlinecirc02plem1  44135  itscnhlinecirc02plem2  44136  inlinecirc02plem  44139  inlinecirc02p  44140  i2linesd  44245  aacllem  44267  amgmwlem  44268  amgmlemALT  44269