Theorem mulcld 11339

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208   · cmul 11215

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 11272

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul02lem1  11496  addrid  11500  cnegex  11501  kcnktkm1cn  11757  subaddmulsub  11789  mulsubaddmulsub  11790  receu  11971  divrec  12000  divcan3  12010  muldivdir  12019  subdivcomb1  12022  subdivcomb2  12023  divdivdiv  12028  divsubdiv  12043  lineq  12164  cru  12322  mul2lt0rlt0  13234  lincmb01cmp  13636  iccf1o  13637  flpmodeq  14024  moddiffl  14032  modvalp1  14040  modcyc  14056  modadd1  14058  modmuladdnn0  14068  modmul1  14077  modaddmulmod  14091  mulexpz  14255  expmulz  14261  binom3  14378  bernneq  14383  mulsubdivbinom2  14416  muldivbinom2  14417  remullem  15307  cjreim2  15340  absimle  15488  abstri  15510  sqreulem  15539  sqreu  15540  bhmafibid1cn  15645  bhmafibid2cn  15646  bhmafibid1  15647  bhmafibid2  15648  mulcn2  15775  reccn2  15776  o1rlimmul  15798  rlimmul  15824  isummulc2  15940  fsummulc2  15962  fsumparts  15985  indsum  16007  binomlem  16010  binom1dif  16014  incexclem  16017  incexc  16018  incexc2  16019  pwdif  16049  geomulcvg  16057  mertenslem1  16065  mertens  16067  fprodmul  16139  fprodn0f  16170  iprodmul  16182  binomfallfaclem1  16217  binomfallfaclem2  16218  binomrisefac  16220  bpolycl  16230  bpolysum  16231  bpolydiflem  16232  bpoly4  16237  efaddlem  16271  sinadd  16344  cosadd  16345  tanaddlem  16346  tanadd  16347  addsin  16350  sincossq  16356  sin2t  16357  dvds2ln  16471  oddm1even  16525  pwp1fsum  16573  flodddiv4  16597  sadadd2lem2  16632  bezoutlem2  16725  bezoutlem3  16726  bezoutlem4  16727  lcmgcdlem  16793  phiprmpw  16965  pythagtriplem12  17016  pythagtriplem14  17018  pythagtriplem16  17020  pcpremul  17033  pcaddlem  17078  fldivp1  17087  mul4sqlem  17143  4sqlem14  17148  vdwapun  17164  vdwlem2  17172  vdwlem6  17176  ablsimpgfindlem1  20335  zringlpirlem3  21782  znunit  21881  blcvx  25129  icopnfcnv  25275  cphipipcj  25533  cphipval2  25574  4cphipval2  25575  cphipval  25576  mbfmulc2re  25981  mbfmulc2  25996  itg1addlem4  26032  itg1addlem5  26033  itg1mulc  26037  mbfmul  26059  itgcl  26116  itgcnlem  26122  iblmulc2  26163  itgmulc2  26166  itgabs  26167  itgsplit  26168  dvmulbr  26271  dvcmul  26276  dvcmulf  26277  dvexp  26285  dvmptcmul  26296  dvmptdiv  26306  dvexp3  26310  dvsincos  26313  cmvth  26323  dvlipcn  26326  dvfsumabs  26355  dvfsumlem1  26358  ftc1lem4  26371  itgparts  26379  itgpowd  26382  plyf  26528  ply1termlem  26533  plyeq0lem  26541  plypf1  26543  plyaddlem1  26544  plymullem1  26545  coeeulem  26555  coeidlem  26568  coeid3  26571  plyco  26572  coemullem  26581  coemulhi  26585  coemulc  26586  dgrcolem2  26605  plycjlem  26607  plyrecj  26610  dvply1  26617  vieta1lem2  26646  vieta1  26647  elqaalem3  26656  aareccl  26665  aalioulem1  26671  taylfvallem1  26696  tayl0  26701  dvtaylp  26709  taylthlem2  26713  psergf  26751  radcnvlem1  26752  dvradcnv  26760  psercn2  26762  pserdvlem2  26767  pserdv2  26769  abelthlem4  26773  abelthlem5  26774  abelthlem6  26775  abelthlem7  26777  abelthlem9  26779  tanregt0  26879  efgh  26881  efabl  26890  efsubm  26891  cosargd  26948  abslogle  26958  tanarg  26959  advlogexp  26995  logtayllem  26999  logtayl  27000  cxpadd  27019  mulcxp  27025  cxpmul  27028  cxpmul2  27029  cxpmul2z  27031  abscxp  27032  abscxp2  27033  dvcxp2  27081  abscxpbnd  27093  root1eq1  27095  cxpeq  27097  angcan  27142  pythag  27157  ssscongptld  27162  affineequiv  27163  affineequiv2  27164  affineequiv3  27165  affineequiv4  27166  chordthmlem2  27173  chordthmlem3  27174  chordthmlem4  27175  chordthmlem5  27176  heron  27178  quad2  27179  quad  27180  dcubic1lem  27183  dcubic2  27184  dcubic1  27185  dcubic  27186  mcubic  27187  cubic2  27188  cubic  27189  binom4  27190  dquartlem1  27191  dquartlem2  27192  dquart  27193  quart1cl  27194  quart1lem  27195  quart1  27196  quartlem1  27197  quartlem2  27198  atantayl3  27279  leibpi  27282  birthdaylem2  27292  divsqrtsumo1  27323  cvxcl  27324  jensenlem2  27327  lgamgulmlem2  27369  lgamgulmlem3  27370  lgamgulmlem4  27371  lgamgulmlem5  27372  lgamgulmlem6  27373  lgamgulm2  27375  lgamcvg2  27394  gamcvg  27395  gamcvg2lem  27398  wilthlem2  27408  ftalem1  27412  ftalem2  27413  ftalem4  27415  ftalem5  27416  basellem2  27421  basellem3  27422  basellem8  27427  muinv  27532  fsumdvdsmul  27534  logfacrlim  27563  logexprlim  27564  perfectlem2  27569  bposlem9  27631  gausslemma2dlem4  27708  lgsquad2lem1  27723  2lgslem3b  27736  2lgslem3c  27737  2lgslem3d  27738  2sqlem3  27759  2sqmod  27775  rplogsumlem1  27823  dchrisumlem2  27829  dchrisumlem3  27830  dchrmusum2  27833  dchrvmasumlem1  27834  dchrvmasum2lem  27835  dchrvmasum2if  27836  dchrvmasumlem3  27838  dchrvmasumiflem1  27840  dchrvmasumiflem2  27841  rpvmasum2  27851  dchrisum0lem1  27855  dchrisum0lem2a  27856  dchrisum0lem2  27857  dchrmusumlem  27861  dchrvmasumlem  27862  rplogsum  27866  mudivsum  27869  mulogsumlem  27870  mulogsum  27871  mulog2sumlem1  27873  mulog2sumlem2  27874  mulog2sumlem3  27875  vmalogdivsum  27878  logsqvma  27881  log2sumbnd  27883  selberglem1  27884  selberglem2  27885  selberglem3  27886  selberg  27887  selberg2lem  27889  selberg2  27890  selberg3lem1  27896  selberg3  27898  selberg4lem1  27899  selberg4  27900  pntrsumo1  27904  selbergr  27907  selberg3r  27908  selberg4r  27909  selberg34r  27910  pntsval2  27915  pntrlog2bndlem1  27916  pntrlog2bndlem2  27917  pntrlog2bndlem3  27918  pntrlog2bndlem4  27919  pntrlog2bndlem5  27920  pntrlog2bndlem6  27922  pntrlog2bnd  27923  pntlemb  27936  pntlemf  27944  pntlemo  27946  ostth2lem2  27973  ostth2lem3  27974  ttgcontlem1  29474  brbtwn2  29495  colinearalg  29500  ax5seglem2  29519  ax5seglem9  29527  axeuclidlem  29552  axcontlem2  29555  axcontlem4  29557  axcontlem7  29560  axcontlem8  29561  finsumvtxdg2ssteplem4  30141  ex-ind-dvds  31074  nrt2irr  31086  ipval2  31321  dipcl  31326  riesz3i  32676  re0cj  33388  pythagreim  33390  quad3d  33394  indsumin  33481  dpfrac1  33511  wrdt2ind  33569  zringfrac  34139  ccfldsrarelvec  34356  ccfldextdgrr  34357  constrrtll  34416  constrrtlc1  34417  constrrtcclem  34419  constrrtcc  34420  constrconj  34430  constrfin  34431  constrelextdg2  34432  nn0constr  34446  constraddcl  34447  constrnegcl  34448  constrdircl  34450  iconstr  34451  constrremulcl  34452  constrrecl  34454  constrimcl  34455  constrmulcl  34456  constrreinvcl  34457  constrinvcl  34458  constrresqrtcl  34462  constrabscl  34463  constrsqrtcl  34464  cos9thpiminplylem1  34467  cos9thpiminplylem2  34468  cos9thpiminplylem3  34469  cos9thpiminply  34473  cos9thpinconstrlem1  34474  cos9thpinconstrlem2  34475  cos9thpinconstr  34476  cnre2csqima  34596  rmulccn  34613  dya2icoseg  34962  oddpwdc  35039  eulerpartlems  35045  eulerpartlemsv3  35046  eulerpartlemgs2  35065  signsplypnf  35232  itgexpif  35288  breprexplemc  35314  breprexp  35315  vtscl  35320  vtsprod  35321  circlemeth  35322  logdivsqrle  35332  hgt750lemf  35335  hgt750leme  35340  subfacval2  36073  subfaclim  36074  resconn  36132  iprodgam  36634  fwddifnp1  37057  knoppcnlem10  37495  knoppndvlem2  37506  knoppndvlem7  37511  knoppndvlem9  37513  knoppndvlem11  37515  knoppndvlem14  37518  knoppndvlem16  37520  knoppndvlem17  37521  bj-subcom  38369  bj-bary1lem  38371  bj-bary1lem1  38372  bj-bary1  38373  qdiff  38388  iblmulc2nc  38743  itgmulc2nc  38746  itgabsnc  38747  ftc1cnnclem  38749  ftc1anclem3  38753  dvasin  38762  areacirclem1  38766  areacirclem4  38769  areacirc  38771  cntotbnd  38870  3factsumint1  43211  3factsumint3  43213  3factsumint4  43214  lcmineqlem2  43220  lcmineqlem6  43224  lcmineqlem8  43226  lcmineqlem10  43228  lcmineqlem11  43229  lcmineqlem12  43230  lcmineqlem16  43234  lcmineqlem18  43236  lcmineqlem23  43241  3lexlogpow5ineq5  43250  aks4d1p1p1  43253  dvrelogpow2b  43258  aks4d1p1p6  43263  aks4d1p1p7  43264  aks4d1p1p5  43265  primrootscoprmpow  43289  posbezout  43290  primrootscoprbij  43292  primrootspoweq0  43296  2np3bcnp1  43334  2ap1caineq  43335  quadfac  43395  oddnumth  43508  nicomachus  43509  sumcubes  43510  ef11d  43530  cxp112d  43532  cxp111d  43533  readvrec2  43552  sn-addlid  43595  sn-it0e0  43607  sn-negex12  43608  sn-mul01  43617  sn-mullid  43627  sn-0tie0  43655  sn-mul02  43656  cnreeu  43694  fltnltalem  43813  fltnlta  43814  cu3addd  43831  3cubeslem2  43835  3cubeslem3l  43836  3cubeslem3r  43837  3cubeslem4  43839  pellexlem1  43976  pellexlem2  43977  pellexlem6  43981  pell1234qrne0  44000  pell1234qrreccl  44001  pell1234qrmulcl  44002  pell1234qrdich  44008  pell14qrdich  44016  pell1qrge1  44017  pell1qrgaplem  44020  rmspecsqrtnq  44053  qirropth  44055  rmxyneg  44067  rmxyadd  44068  rmxm1  44081  rmym1  44082  rmxluc  44083  rmyluc  44084  rmxdbl  44086  rmydbl  44087  jm2.18  44135  jm2.19lem1  44136  jm2.19lem2  44137  jm2.19lem4  44139  jm2.19  44140  jm2.22  44142  jm2.23  44143  jm2.25  44146  jm2.27c  44154  jm3.1lem2  44165  flcidc  44312  areaquad  44358  sqrtcval  44781  inductionexd  45295  imo72b2lem0  45305  int-leftdistd  45319  radcnvrat  45438  expgrowth  45459  binomcxplemwb  45472  binomcxplemnn0  45473  binomcxplemfrat  45475  binomcxplemdvbinom  45477  binomcxplemnotnn0  45480  sineq0ALT  46058  mul13d  46435  fperiodmullem  46458  fperiodmul  46459  divcan8d  46467  dmmcand  46468  ltdiv23neg  46544  mulc1cncfg  46740  mccllem  46748  clim1fr1  46752  mullimc  46767  mullimcf  46774  sumnnodd  46781  reclimc  46802  sinmulcos  47014  coskpi2  47015  cosknegpi  47018  dvsinexp  47060  dvasinbx  47069  dvdivf  47071  dvdivbd  47072  dvdivcncf  47076  dvbdfbdioolem2  47078  dvxpaek  47089  dvnxpaek  47091  dvnmul  47092  dvmptfprodlem  47093  dvnprodlem2  47096  itgsinexplem1  47103  itgsinexp  47104  itgcoscmulx  47118  itgsincmulx  47123  itgiccshift  47129  itgperiod  47130  stoweidlem1  47150  stoweidlem11  47160  stoweidlem13  47162  stoweidlem14  47163  stoweidlem17  47166  stoweidlem25  47174  stoweidlem26  47175  stoweidlem42  47191  wallispilem4  47217  wallispilem5  47218  wallispi  47219  wallispi2lem1  47220  wallispi2lem2  47221  wallispi2  47222  stirlinglem1  47223  stirlinglem3  47225  stirlinglem4  47226  stirlinglem5  47227  stirlinglem6  47228  stirlinglem7  47229  stirlinglem8  47230  stirlinglem10  47232  stirlinglem11  47233  stirlinglem12  47234  stirlinglem13  47235  stirlinglem14  47236  stirlinglem15  47237  dirker2re  47241  dirkerdenne0  47242  dirkerper  47245  dirkertrigeqlem1  47247  dirkertrigeqlem2  47248  dirkertrigeqlem3  47249  dirkertrigeq  47250  dirkeritg  47251  dirkercncflem2  47253  dirkercncflem4  47255  fourierdlem26  47282  fourierdlem30  47286  fourierdlem39  47295  fourierdlem42  47298  fourierdlem47  47302  fourierdlem48  47303  fourierdlem56  47311  fourierdlem57  47312  fourierdlem58  47313  fourierdlem62  47317  fourierdlem65  47320  fourierdlem66  47321  fourierdlem68  47323  fourierdlem72  47327  fourierdlem73  47328  fourierdlem76  47331  fourierdlem80  47335  fourierdlem83  47338  fourierdlem85  47340  fourierdlem89  47344  fourierdlem90  47345  fourierdlem91  47346  fourierdlem95  47350  fourierdlem97  47352  fourierdlem101  47356  fourierdlem103  47358  fourierdlem104  47359  fourierdlem111  47366  sqwvfoura  47377  sqwvfourb  47378  fourierswlem  47379  fouriersw  47380  elaa2lem  47382  etransclem8  47391  etransclem18  47401  etransclem20  47403  etransclem21  47404  etransclem23  47406  etransclem24  47407  etransclem31  47414  etransclem33  47416  etransclem35  47418  etransclem45  47428  etransclem46  47429  etransclem47  47430  etransclem48  47431  hoicvrrex  47705  hoidmvlelem2  47745  smfmullem1  47940  sigarim  48000  sigarac  48001  sigaraf  48002  sigarmf  48003  sigarls  48006  sigardiv  48010  sigarcol  48013  cevathlem1  48016  sin3t  48056  cos3t  48057  sin5tlem1  48058  sin5tlem2  48059  sin5tlem3  48060  sin5tlem4  48061  sin5tlem5  48062  sin5t  48063  cos5t  48064  fldivmod  48553  fmtnorec2lem  48766  fmtnorec3  48772  fmtnorec4  48773  fmtnoprmfac1  48789  fmtnoprmfac2  48791  fmtnofac2lem  48792  sfprmdvdsmersenne  48827  lighneallem3  48831  quad1  48857  requad01  48858  requad2  48860  opeoALTV  48921  perfectALTVlem2  48959  fppr2odd  48968  0nodd  49406  2nodd  49408  2zlidl  49476  2zrngnmlid  49491  altgsumbcALT  49604  nn0sumshdiglemA  49870  nn0sumshdiglemB  49871  nn0sumshdiglem2  49873  nn0mullong  49876  itcovalt2lem2lem2  49925  ackval2  49933  submuladdmuld  49952  affinecomb2  49954  affineid  49955  1subrec1sub  49956  eenglngeehlnmlem1  49989  eenglngeehlnmlem2  49990  rrx2linest  49993  line2x  50005  line2y  50006  itschlc0yqe  50011  itsclc0yqsollem1  50013  itsclc0yqsol  50015  itscnhlc0xyqsol  50016  itschlc0xyqsol1  50017  itschlc0xyqsol  50018  itsclc0xyqsolr  50020  2itscplem1  50029  2itscplem2  50030  2itscplem3  50031  2itscp  50032  itscnhlinecirc02plem1  50033  itscnhlinecirc02plem2  50034  inlinecirc02plem  50037  inlinecirc02p  50038  dvsec  51070  i2linesd  51089  aacllem  51153  crossp3d  51181  amgmwlem  51201  amgmlemALT  51202