Theorem mulcld 11246

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115   · cmul 11122

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

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

This theorem is used by:  mul02lem1  11403  addrid  11407  cnegex  11408  kcnktkm1cn  11662  subaddmulsub  11694  mulsubaddmulsub  11695  receu  11876  divrec  11905  divcan3  11915  muldivdir  11924  subdivcomb1  11927  subdivcomb2  11928  divdivdiv  11933  divsubdiv  11948  lineq  12069  cru  12227  mul2lt0rlt0  13138  lincmb01cmp  13540  iccf1o  13541  flpmodeq  13927  moddiffl  13935  modvalp1  13943  modcyc  13959  modadd1  13961  modmuladdnn0  13971  modmul1  13980  modaddmulmod  13994  mulexpz  14158  expmulz  14164  binom3  14280  bernneq  14285  mulsubdivbinom2  14318  muldivbinom2  14319  remullem  15205  cjreim2  15238  absimle  15386  abstri  15408  sqreulem  15437  sqreu  15438  bhmafibid1cn  15543  bhmafibid2cn  15544  bhmafibid1  15545  bhmafibid2  15546  mulcn2  15673  reccn2  15674  o1rlimmul  15696  rlimmul  15722  isummulc2  15838  fsummulc2  15860  fsumparts  15883  indsum  15905  binomlem  15908  binom1dif  15912  incexclem  15915  incexc  15916  incexc2  15917  pwdif  15947  geomulcvg  15955  mertenslem1  15963  mertens  15965  fprodmul  16039  fprodn0f  16070  iprodmul  16082  binomfallfaclem1  16117  binomfallfaclem2  16118  binomrisefac  16120  bpolycl  16130  bpolysum  16131  bpolydiflem  16132  bpoly4  16137  efaddlem  16171  sinadd  16244  cosadd  16245  tanaddlem  16246  tanadd  16247  addsin  16250  sincossq  16256  sin2t  16257  dvds2ln  16371  oddm1even  16425  pwp1fsum  16473  flodddiv4  16497  sadadd2lem2  16532  bezoutlem2  16622  bezoutlem3  16623  bezoutlem4  16624  lcmgcdlem  16688  phiprmpw  16859  pythagtriplem12  16910  pythagtriplem14  16912  pythagtriplem16  16914  pcpremul  16927  pcaddlem  16972  fldivp1  16981  mul4sqlem  17037  4sqlem14  17042  vdwapun  17058  vdwlem2  17066  vdwlem6  17070  ablsimpgfindlem1  20225  zringlpirlem3  21666  znunit  21765  blcvx  25008  icopnfcnv  25154  cphipipcj  25412  cphipval2  25453  4cphipval2  25454  cphipval  25455  mbfmulc2re  25860  mbfmulc2  25875  itg1addlem4  25911  itg1addlem5  25912  itg1mulc  25916  mbfmul  25938  itgcl  25996  itgcnlem  26002  iblmulc2  26043  itgmulc2  26046  itgabs  26047  itgsplit  26048  dvmulbr  26151  dvcmul  26156  dvcmulf  26157  dvexp  26165  dvmptcmul  26176  dvmptdiv  26186  dvexp3  26190  dvsincos  26193  cmvth  26203  dvlipcn  26206  dvfsumabs  26235  dvfsumlem1  26238  ftc1lem4  26251  itgparts  26259  itgpowd  26262  plyf  26408  ply1termlem  26413  plyeq0lem  26420  plypf1  26422  plyaddlem1  26423  plymullem1  26424  coeeulem  26434  coeidlem  26447  coeid3  26450  plyco  26451  coemullem  26460  coemulhi  26464  coemulc  26465  dgrcolem2  26484  plycjlem  26486  plyrecj  26491  dvply1  26498  vieta1lem2  26525  vieta1  26526  elqaalem3  26535  aareccl  26542  aalioulem1  26548  taylfvallem1  26573  tayl0  26578  dvtaylp  26586  taylthlem2  26590  psergf  26628  radcnvlem1  26629  dvradcnv  26637  psercn2  26639  pserdvlem2  26644  pserdv2  26646  abelthlem4  26650  abelthlem5  26651  abelthlem6  26652  abelthlem7  26654  abelthlem9  26656  tanregt0  26757  efgh  26759  efabl  26768  efsubm  26769  cosargd  26826  abslogle  26836  tanarg  26837  advlogexp  26873  logtayllem  26877  logtayl  26878  cxpadd  26897  mulcxp  26903  cxpmul  26906  cxpmul2  26907  cxpmul2z  26909  abscxp  26910  abscxp2  26911  dvcxp2  26959  abscxpbnd  26971  root1eq1  26973  cxpeq  26975  angcan  27020  pythag  27035  ssscongptld  27040  affineequiv  27041  affineequiv2  27042  affineequiv3  27043  affineequiv4  27044  chordthmlem2  27051  chordthmlem3  27052  chordthmlem4  27053  chordthmlem5  27054  heron  27056  quad2  27057  quad  27058  dcubic1lem  27061  dcubic2  27062  dcubic1  27063  dcubic  27064  mcubic  27065  cubic2  27066  cubic  27067  binom4  27068  dquartlem1  27069  dquartlem2  27070  dquart  27071  quart1cl  27072  quart1lem  27073  quart1  27074  quartlem1  27075  quartlem2  27076  atantayl3  27157  leibpi  27160  birthdaylem2  27170  divsqrtsumo1  27201  cvxcl  27202  jensenlem2  27205  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamgulmlem4  27249  lgamgulmlem5  27250  lgamgulmlem6  27251  lgamgulm2  27253  lgamcvg2  27272  gamcvg  27273  gamcvg2lem  27276  wilthlem2  27286  ftalem1  27290  ftalem2  27291  ftalem4  27293  ftalem5  27294  basellem2  27299  basellem3  27300  basellem8  27305  muinv  27410  fsumdvdsmul  27412  logfacrlim  27441  logexprlim  27442  perfectlem2  27447  bposlem9  27509  gausslemma2dlem4  27586  lgsquad2lem1  27601  2lgslem3b  27614  2lgslem3c  27615  2lgslem3d  27616  2sqlem3  27637  2sqmod  27653  rplogsumlem1  27701  dchrisumlem2  27707  dchrisumlem3  27708  dchrmusum2  27711  dchrvmasumlem1  27712  dchrvmasum2lem  27713  dchrvmasum2if  27714  dchrvmasumlem3  27716  dchrvmasumiflem1  27718  dchrvmasumiflem2  27719  rpvmasum2  27729  dchrisum0lem1  27733  dchrisum0lem2a  27734  dchrisum0lem2  27735  dchrmusumlem  27739  dchrvmasumlem  27740  rplogsum  27744  mudivsum  27747  mulogsumlem  27748  mulogsum  27749  mulog2sumlem1  27751  mulog2sumlem2  27752  mulog2sumlem3  27753  vmalogdivsum  27756  logsqvma  27759  log2sumbnd  27761  selberglem1  27762  selberglem2  27763  selberglem3  27764  selberg  27765  selberg2lem  27767  selberg2  27768  selberg3lem1  27774  selberg3  27776  selberg4lem1  27777  selberg4  27778  pntrsumo1  27782  selbergr  27785  selberg3r  27786  selberg4r  27787  selberg34r  27788  pntsval2  27793  pntrlog2bndlem1  27794  pntrlog2bndlem2  27795  pntrlog2bndlem3  27796  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntrlog2bndlem6  27800  pntrlog2bnd  27801  pntlemb  27814  pntlemf  27822  pntlemo  27824  ostth2lem2  27851  ostth2lem3  27852  ttgcontlem1  29291  brbtwn2  29312  colinearalg  29317  ax5seglem2  29336  ax5seglem9  29344  axeuclidlem  29369  axcontlem2  29372  axcontlem4  29374  axcontlem7  29377  axcontlem8  29378  finsumvtxdg2ssteplem4  29958  ex-ind-dvds  30885  nrt2irr  30897  ipval2  31132  dipcl  31137  riesz3i  32487  re0cj  33160  pythagreim  33162  quad3d  33166  indsumin  33253  dpfrac1  33283  wrdt2ind  33341  zringfrac  33910  ccfldsrarelvec  34127  ccfldextdgrr  34128  constrrtll  34187  constrrtlc1  34188  constrrtcclem  34190  constrrtcc  34191  constrconj  34201  constrfin  34202  constrelextdg2  34203  nn0constr  34217  constraddcl  34218  constrnegcl  34219  constrdircl  34221  iconstr  34222  constrremulcl  34223  constrrecl  34225  constrimcl  34226  constrmulcl  34227  constrreinvcl  34228  constrinvcl  34229  constrresqrtcl  34233  constrabscl  34234  constrsqrtcl  34235  cos9thpiminplylem1  34238  cos9thpiminplylem2  34239  cos9thpiminplylem3  34240  cos9thpiminply  34244  cos9thpinconstrlem1  34245  cos9thpinconstrlem2  34246  cos9thpinconstr  34247  cnre2csqima  34367  rmulccn  34384  dya2icoseg  34734  oddpwdc  34811  eulerpartlems  34817  eulerpartlemsv3  34818  eulerpartlemgs2  34837  signsplypnf  35004  itgexpif  35060  breprexplemc  35086  breprexp  35087  vtscl  35092  vtsprod  35093  circlemeth  35094  logdivsqrle  35104  hgt750lemf  35107  hgt750leme  35112  subfacval2  35718  subfaclim  35719  resconn  35777  iprodgam  36273  fwddifnp1  36696  knoppcnlem10  37150  knoppndvlem2  37161  knoppndvlem7  37166  knoppndvlem9  37168  knoppndvlem11  37170  knoppndvlem14  37173  knoppndvlem16  37175  knoppndvlem17  37176  bj-subcom  38011  bj-bary1lem  38013  bj-bary1lem1  38014  bj-bary1  38015  qdiff  38030  iblmulc2nc  38395  itgmulc2nc  38398  itgabsnc  38399  ftc1cnnclem  38401  ftc1anclem3  38405  dvasin  38414  areacirclem1  38418  areacirclem4  38421  areacirc  38423  cntotbnd  38507  3factsumint1  42848  3factsumint3  42850  3factsumint4  42851  lcmineqlem2  42857  lcmineqlem6  42861  lcmineqlem8  42863  lcmineqlem10  42865  lcmineqlem11  42866  lcmineqlem12  42867  lcmineqlem16  42871  lcmineqlem18  42873  lcmineqlem23  42878  3lexlogpow5ineq5  42887  aks4d1p1p1  42890  dvrelogpow2b  42895  aks4d1p1p6  42900  aks4d1p1p7  42901  aks4d1p1p5  42902  primrootscoprmpow  42926  posbezout  42927  primrootscoprbij  42929  primrootspoweq0  42933  2np3bcnp1  42971  2ap1caineq  42972  quadfac  43032  oddnumth  43132  nicomachus  43133  sumcubes  43134  ef11d  43160  cxp112d  43162  cxp111d  43163  readvrec2  43182  sn-addlid  43225  sn-it0e0  43237  sn-negex12  43238  sn-mul01  43247  sn-mullid  43257  sn-0tie0  43285  sn-mul02  43286  cnreeu  43324  fltnltalem  43454  fltnlta  43455  cu3addd  43472  3cubeslem2  43476  3cubeslem3l  43477  3cubeslem3r  43478  3cubeslem4  43480  pellexlem1  43616  pellexlem2  43617  pellexlem6  43621  pell1234qrne0  43640  pell1234qrreccl  43641  pell1234qrmulcl  43642  pell1234qrdich  43648  pell14qrdich  43656  pell1qrge1  43657  pell1qrgaplem  43660  rmspecsqrtnq  43693  qirropth  43695  rmxyneg  43707  rmxyadd  43708  rmxm1  43721  rmym1  43722  rmxluc  43723  rmyluc  43724  rmxdbl  43726  rmydbl  43727  jm2.18  43775  jm2.19lem1  43776  jm2.19lem2  43777  jm2.19lem4  43779  jm2.19  43780  jm2.22  43782  jm2.23  43783  jm2.25  43786  jm2.27c  43794  jm3.1lem2  43805  flcidc  43957  areaquad  44003  sqrtcval  44427  inductionexd  44941  imo72b2lem0  44951  int-leftdistd  44965  radcnvrat  45084  expgrowth  45105  binomcxplemwb  45118  binomcxplemnn0  45119  binomcxplemfrat  45121  binomcxplemdvbinom  45123  binomcxplemnotnn0  45126  sineq0ALT  45705  mul13d  46059  fperiodmullem  46082  fperiodmul  46083  divcan8d  46091  dmmcand  46092  ltdiv23neg  46169  mulc1cncfg  46365  mccllem  46373  clim1fr1  46377  mullimc  46392  mullimcf  46399  sumnnodd  46406  reclimc  46427  sinmulcos  46639  coskpi2  46640  cosknegpi  46643  dvsinexp  46685  dvasinbx  46694  dvdivf  46696  dvdivbd  46697  dvdivcncf  46701  dvbdfbdioolem2  46703  dvxpaek  46714  dvnxpaek  46716  dvnmul  46717  dvmptfprodlem  46718  dvnprodlem2  46721  itgsinexplem1  46728  itgsinexp  46729  itgcoscmulx  46743  itgsincmulx  46748  itgiccshift  46754  itgperiod  46755  stoweidlem1  46775  stoweidlem11  46785  stoweidlem13  46787  stoweidlem14  46788  stoweidlem17  46791  stoweidlem25  46799  stoweidlem26  46800  stoweidlem42  46816  wallispilem4  46842  wallispilem5  46843  wallispi  46844  wallispi2lem1  46845  wallispi2lem2  46846  wallispi2  46847  stirlinglem1  46848  stirlinglem3  46850  stirlinglem4  46851  stirlinglem5  46852  stirlinglem6  46853  stirlinglem7  46854  stirlinglem8  46855  stirlinglem10  46857  stirlinglem11  46858  stirlinglem12  46859  stirlinglem13  46860  stirlinglem14  46861  stirlinglem15  46862  dirker2re  46866  dirkerdenne0  46867  dirkerper  46870  dirkertrigeqlem1  46872  dirkertrigeqlem2  46873  dirkertrigeqlem3  46874  dirkertrigeq  46875  dirkeritg  46876  dirkercncflem2  46878  dirkercncflem4  46880  fourierdlem26  46907  fourierdlem30  46911  fourierdlem39  46920  fourierdlem42  46923  fourierdlem47  46927  fourierdlem48  46928  fourierdlem56  46936  fourierdlem57  46937  fourierdlem58  46938  fourierdlem62  46942  fourierdlem65  46945  fourierdlem66  46946  fourierdlem68  46948  fourierdlem72  46952  fourierdlem73  46953  fourierdlem76  46956  fourierdlem80  46960  fourierdlem83  46963  fourierdlem85  46965  fourierdlem89  46969  fourierdlem90  46970  fourierdlem91  46971  fourierdlem95  46975  fourierdlem97  46977  fourierdlem101  46981  fourierdlem103  46983  fourierdlem104  46984  fourierdlem111  46991  sqwvfoura  47002  sqwvfourb  47003  fourierswlem  47004  fouriersw  47005  elaa2lem  47007  etransclem8  47016  etransclem18  47026  etransclem20  47028  etransclem21  47029  etransclem23  47031  etransclem24  47032  etransclem31  47039  etransclem33  47041  etransclem35  47043  etransclem45  47053  etransclem46  47054  etransclem47  47055  etransclem48  47056  hoicvrrex  47330  hoidmvlelem2  47370  smfmullem1  47565  sigarim  47625  sigarac  47626  sigaraf  47627  sigarmf  47628  sigarls  47631  sigardiv  47635  sigarcol  47638  cevathlem1  47641  sin3t  47668  cos3t  47669  sin5tlem1  47670  sin5tlem2  47671  sin5tlem3  47672  sin5tlem4  47673  sin5tlem5  47674  sin5t  47675  cos5t  47676  fldivmod  48141  fmtnorec2lem  48354  fmtnorec3  48360  fmtnorec4  48361  fmtnoprmfac1  48377  fmtnoprmfac2  48379  fmtnofac2lem  48380  sfprmdvdsmersenne  48415  lighneallem3  48419  quad1  48445  requad01  48446  requad2  48448  opeoALTV  48509  perfectALTVlem2  48547  fppr2odd  48556  0nodd  48994  2nodd  48996  2zlidl  49064  2zrngnmlid  49079  altgsumbcALT  49192  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  nn0sumshdiglem2  49461  nn0mullong  49464  itcovalt2lem2lem2  49513  ackval2  49521  submuladdmuld  49540  affinecomb2  49542  affineid  49543  1subrec1sub  49544  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  rrx2linest  49581  line2x  49593  line2y  49594  itschlc0yqe  49599  itsclc0yqsollem1  49601  itsclc0yqsol  49603  itscnhlc0xyqsol  49604  itschlc0xyqsol1  49605  itschlc0xyqsol  49606  itsclc0xyqsolr  49608  2itscplem1  49617  2itscplem2  49618  2itscplem3  49619  2itscp  49620  itscnhlinecirc02plem1  49621  itscnhlinecirc02plem2  49622  inlinecirc02plem  49625  inlinecirc02p  49626  i2linesd  50616  aacllem  50680  crossp3d  50708  amgmwlem  50709  amgmlemALT  50710