Theorem mulcld 11368

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   · cmul 11244

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

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

This theorem is used by:  mul02lem1  11525  addrid  11529  cnegex  11530  kcnktkm1cn  11786  addmuldir1d  11815  subaddmulsub  11819  mulsubaddmulsub  11820  receu  12001  divrec  12030  divcan3  12040  muldivdir  12049  subdivcomb1  12052  subdivcomb2  12053  divdivdiv  12058  divsubdiv  12073  lineq  12194  cru  12352  mul2lt0rlt0  13264  lincmb01cmp  13666  iccf1o  13667  flpmodeq  14054  moddiffl  14062  modvalp1  14070  modcyc  14086  modadd1  14088  modmuladdnn0  14098  modmul1  14107  modaddmulmod  14121  mulexpz  14285  expmulz  14291  addmuldir2d  14396  binom3  14409  bernneq  14414  mulsubdivbinom2  14447  muldivbinom2  14448  remullem  15338  cjreim2  15371  absimle  15519  abstri  15541  sqreulem  15571  sqreu  15572  bhmafibid1cn  15677  bhmafibid2cn  15678  bhmafibid1  15679  bhmafibid2  15680  mulcn2  15807  reccn2  15808  o1rlimmul  15830  rlimmul  15856  isummulc2  15972  fsummulc2  15994  fsumparts  16017  indsum  16039  binomlem  16042  binom1dif  16046  incexclem  16049  incexc  16050  incexc2  16051  pwdif  16081  geomulcvg  16089  mertenslem1  16097  mertens  16099  fprodmul  16171  fprodn0f  16202  iprodmul  16214  binomfallfaclem1  16249  binomfallfaclem2  16250  binomrisefac  16252  bpolycl  16262  bpolysum  16263  bpolydiflem  16264  bpoly4  16269  efaddlem  16303  sinadd  16376  cosadd  16377  tanaddlem  16378  tanadd  16379  addsin  16382  sincossq  16388  sin2t  16389  dvds2ln  16503  oddm1even  16557  pwp1fsum  16605  flodddiv4  16629  sadadd2lem2  16664  bezoutlem2  16757  bezoutlem3  16758  bezoutlem4  16759  lcmgcdlem  16825  phiprmpw  16997  pythagtriplem12  17048  pythagtriplem14  17050  pythagtriplem16  17052  pcpremul  17065  pcaddlem  17110  fldivp1  17119  mul4sqlem  17175  4sqlem14  17180  vdwapun  17196  vdwlem2  17204  vdwlem6  17208  ablsimpgfindlem1  20374  zringlpirlem3  21825  znunit  21924  blcvx  25172  icopnfcnv  25318  cphipipcj  25576  cphipval2  25617  4cphipval2  25618  cphipval  25619  mbfmulc2re  26024  mbfmulc2  26039  itg1addlem4  26075  itg1addlem5  26076  itg1mulc  26080  mbfmul  26102  itgcl  26159  itgcnlem  26165  iblmulc2  26206  itgmulc2  26209  itgabs  26210  itgsplit  26211  dvmulbr  26314  dvcmul  26319  dvcmulf  26320  dvexp  26328  dvmptcmul  26339  dvmptdiv  26349  dvexp3  26353  dvsincos  26356  cmvth  26366  dvlipcn  26369  dvfsumabs  26398  dvfsumlem1  26401  ftc1lem4  26414  itgparts  26422  itgpowd  26425  plyf  26571  ply1termlem  26576  plyeq0lem  26584  plypf1  26586  plyaddlem1  26587  plymullem1  26588  coeeulem  26598  coeidlem  26611  coeid3  26614  plyco  26615  coemullem  26624  coemulhi  26628  coemulc  26629  dgrcolem2  26648  plycjlem  26650  plyrecj  26653  dvply1  26660  vieta1lem2  26689  vieta1  26690  elqaalem3  26701  aareccl  26710  aalioulem1  26716  taylfvallem1  26741  tayl0  26746  dvtaylp  26754  taylthlem2  26758  psergf  26796  radcnvlem1  26797  dvradcnv  26805  psercn2  26807  pserdvlem2  26812  pserdv2  26814  abelthlem4  26818  abelthlem5  26819  abelthlem6  26820  abelthlem7  26822  abelthlem9  26824  tanregt0  26924  efgh  26926  efabl  26935  efsubm  26936  cosargd  26993  abslogle  27003  tanarg  27004  advlogexp  27040  logtayllem  27044  logtayl  27045  cxpadd  27064  mulcxp  27070  cxpmul  27073  cxpmul2  27074  cxpmul2z  27076  abscxp  27077  abscxp2  27078  dvcxp2  27126  abscxpbnd  27138  root1eq1  27140  cxpeq  27142  angcan  27187  pythag  27202  ssscongptld  27207  affineequiv  27208  affineequiv2  27209  affineequiv3  27210  affineequiv4  27211  chordthmlem2  27218  chordthmlem3  27219  chordthmlem4  27220  chordthmlem5  27221  heron  27223  quad2  27224  quad  27225  dcubic1lem  27228  dcubic2  27229  dcubic1  27230  dcubic  27231  mcubic  27232  cubic2  27233  cubic  27234  binom4  27235  dquartlem1  27236  dquartlem2  27237  dquart  27238  quart1cl  27239  quart1lem  27240  quart1  27241  quartlem1  27242  quartlem2  27243  atantayl3  27324  leibpi  27327  birthdaylem2  27337  divsqrtsumo1  27368  cvxcl  27369  jensenlem2  27372  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamgulmlem4  27416  lgamgulmlem5  27417  lgamgulmlem6  27418  lgamgulm2  27420  lgamcvg2  27439  gamcvg  27440  gamcvg2lem  27443  wilthlem2  27453  ftalem1  27457  ftalem2  27458  ftalem4  27460  ftalem5  27461  basellem2  27466  basellem3  27467  basellem8  27472  muinv  27577  fsumdvdsmul  27579  logfacrlim  27608  logexprlim  27609  perfectlem2  27614  bposlem9  27676  gausslemma2dlem4  27753  lgsquad2lem1  27768  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  2sqlem3  27804  2sqmod  27820  rplogsumlem1  27868  dchrisumlem2  27874  dchrisumlem3  27875  dchrmusum2  27878  dchrvmasumlem1  27879  dchrvmasum2lem  27880  dchrvmasum2if  27881  dchrvmasumlem3  27883  dchrvmasumiflem1  27885  dchrvmasumiflem2  27886  rpvmasum2  27896  dchrisum0lem1  27900  dchrisum0lem2a  27901  dchrisum0lem2  27902  dchrmusumlem  27906  dchrvmasumlem  27907  rplogsum  27911  mudivsum  27914  mulogsumlem  27915  mulogsum  27916  mulog2sumlem1  27918  mulog2sumlem2  27919  mulog2sumlem3  27920  vmalogdivsum  27923  logsqvma  27926  log2sumbnd  27928  selberglem1  27929  selberglem2  27930  selberglem3  27931  selberg  27932  selberg2lem  27934  selberg2  27935  selberg3lem1  27941  selberg3  27943  selberg4lem1  27944  selberg4  27945  pntrsumo1  27949  selbergr  27952  selberg3r  27953  selberg4r  27954  selberg34r  27955  pntsval2  27960  pntrlog2bndlem1  27961  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntrlog2bnd  27968  pntlemb  27981  pntlemf  27989  pntlemo  27991  ostth2lem2  28018  ostth2lem3  28019  ttgcontlem1  29519  brbtwn2  29540  colinearalg  29545  ax5seglem2  29564  ax5seglem9  29572  axeuclidlem  29597  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  axcontlem8  29606  finsumvtxdg2ssteplem4  30186  ex-ind-dvds  31119  nrt2irr  31131  ipval2  31366  dipcl  31371  riesz3i  32721  re0cj  33431  pythagreim  33433  quad3d  33437  indsumin  33524  dpfrac1  33554  wrdt2ind  33612  zringfrac  34189  ccfldsrarelvec  34414  ccfldextdgrr  34415  constrrtll  34474  constrrtlc1  34475  constrrtcclem  34477  constrrtcc  34478  constrconj  34488  constrfin  34489  constrelextdg2  34490  nn0constr  34504  constraddcl  34505  constrnegcl  34506  constrdircl  34508  iconstr  34509  constrremulcl  34510  constrrecl  34512  constrimcl  34513  constrmulcl  34514  constrreinvcl  34515  constrinvcl  34516  constrresqrtcl  34520  constrabscl  34521  constrsqrtcl  34522  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminply  34531  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  cos9thpinconstr  34534  cnre2csqima  34654  rmulccn  34671  dya2icoseg  35020  oddpwdc  35097  eulerpartlems  35103  eulerpartlemsv3  35104  eulerpartlemgs2  35123  signsplypnf  35290  itgexpif  35346  breprexplemc  35372  breprexp  35373  vtscl  35378  vtsprod  35379  circlemeth  35380  logdivsqrle  35390  hgt750lemf  35393  hgt750leme  35398  subfacval2  36160  subfaclim  36161  resconn  36219  iprodgam  36722  fwddifnp1  37145  knoppcnlem10  37583  knoppndvlem2  37594  knoppndvlem7  37599  knoppndvlem9  37601  knoppndvlem11  37603  knoppndvlem14  37606  knoppndvlem16  37608  knoppndvlem17  37609  bj-subcom  38497  bj-bary1lem  38499  bj-bary1lem1  38500  bj-bary1  38501  qdiff  38516  iblmulc2nc  38871  itgmulc2nc  38874  itgabsnc  38875  ftc1cnnclem  38877  ftc1anclem3  38881  dvasin  38890  areacirclem1  38894  areacirclem4  38897  areacirc  38899  cntotbnd  38996  3factsumint1  43337  3factsumint3  43339  3factsumint4  43340  lcmineqlem2  43346  lcmineqlem6  43350  lcmineqlem8  43352  lcmineqlem10  43354  lcmineqlem11  43355  lcmineqlem12  43356  lcmineqlem16  43360  lcmineqlem18  43362  lcmineqlem23  43367  3lexlogpow5ineq5  43376  aks4d1p1p1  43379  dvrelogpow2b  43384  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  primrootscoprmpow  43415  posbezout  43416  primrootscoprbij  43418  primrootspoweq0  43422  2np3bcnp1  43460  2ap1caineq  43461  quadfac  43521  oddnumth  43634  nicomachus  43635  sumcubes  43636  ef11d  43656  cxp112d  43658  cxp111d  43659  readvrec2  43678  sn-addlid  43721  sn-it0e0  43733  sn-negex12  43734  sn-mul01  43743  sn-mullid  43753  sn-0tie0  43781  sn-mul02  43782  cnreeu  43820  fltnltalem  43939  fltnlta  43940  cu3addd  43957  3cubeslem2  43961  3cubeslem3l  43962  3cubeslem3r  43963  3cubeslem4  43965  pellexlem1  44102  pellexlem2  44103  pellexlem6  44107  pell1234qrne0  44126  pell1234qrreccl  44127  pell1234qrmulcl  44128  pell1234qrdich  44134  pell14qrdich  44142  pell1qrge1  44143  pell1qrgaplem  44146  rmspecsqrtnq  44179  qirropth  44181  rmxyneg  44193  rmxyadd  44194  rmxm1  44207  rmym1  44208  rmxluc  44209  rmyluc  44210  rmxdbl  44212  rmydbl  44213  jm2.18  44261  jm2.19lem1  44262  jm2.19lem2  44263  jm2.19lem4  44265  jm2.19  44266  jm2.22  44268  jm2.23  44269  jm2.25  44272  jm2.27c  44280  jm3.1lem2  44291  flcidc  44433  areaquad  44479  sqrtcval  44902  inductionexd  45416  imo72b2lem0  45426  int-leftdistd  45440  radcnvrat  45559  expgrowth  45580  binomcxplemwb  45593  binomcxplemnn0  45594  binomcxplemfrat  45596  binomcxplemdvbinom  45598  binomcxplemnotnn0  45601  sineq0ALT  46179  mul13d  46569  fperiodmullem  46592  fperiodmul  46593  divcan8d  46601  dmmcand  46602  ltdiv23neg  46678  mulc1cncfg  46874  mccllem  46882  clim1fr1  46886  mullimc  46901  mullimcf  46908  sumnnodd  46915  reclimc  46936  sinmulcos  47148  coskpi2  47149  cosknegpi  47152  dvsinexp  47194  dvasinbx  47203  dvdivf  47205  dvdivbd  47206  dvdivcncf  47210  dvbdfbdioolem2  47212  dvxpaek  47223  dvnxpaek  47225  dvnmul  47226  dvmptfprodlem  47227  dvnprodlem2  47230  itgsinexplem1  47237  itgsinexp  47238  itgcoscmulx  47252  itgsincmulx  47257  itgiccshift  47263  itgperiod  47264  stoweidlem1  47284  stoweidlem11  47294  stoweidlem13  47296  stoweidlem14  47297  stoweidlem17  47300  stoweidlem25  47308  stoweidlem26  47309  stoweidlem42  47325  wallispilem4  47351  wallispilem5  47352  wallispi  47353  wallispi2lem1  47354  wallispi2lem2  47355  wallispi2  47356  stirlinglem1  47357  stirlinglem3  47359  stirlinglem4  47360  stirlinglem5  47361  stirlinglem6  47362  stirlinglem7  47363  stirlinglem8  47364  stirlinglem10  47366  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  dirker2re  47375  dirkerdenne0  47376  dirkerper  47379  dirkertrigeqlem1  47381  dirkertrigeqlem2  47382  dirkertrigeqlem3  47383  dirkertrigeq  47384  dirkeritg  47385  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem26  47416  fourierdlem30  47420  fourierdlem39  47429  fourierdlem42  47432  fourierdlem47  47436  fourierdlem48  47437  fourierdlem56  47445  fourierdlem57  47446  fourierdlem58  47447  fourierdlem62  47451  fourierdlem65  47454  fourierdlem66  47455  fourierdlem68  47457  fourierdlem72  47461  fourierdlem73  47462  fourierdlem76  47465  fourierdlem80  47469  fourierdlem83  47472  fourierdlem85  47474  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem95  47484  fourierdlem97  47486  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  sqwvfoura  47511  sqwvfourb  47512  fourierswlem  47513  fouriersw  47514  elaa2lem  47516  etransclem8  47525  etransclem18  47535  etransclem20  47537  etransclem21  47538  etransclem23  47540  etransclem24  47541  etransclem31  47548  etransclem33  47550  etransclem35  47552  etransclem45  47562  etransclem46  47563  etransclem47  47564  etransclem48  47565  hoicvrrex  47839  hoidmvlelem2  47879  smfmullem1  48074  sigarim  48134  sigarac  48135  sigaraf  48136  sigarmf  48137  sigarls  48140  sigardiv  48144  sigarcol  48147  cevathlem1  48150  sin3t  48190  cos3t  48191  sin5tlem1  48192  sin5tlem2  48193  sin5tlem3  48194  sin5tlem4  48195  sin5tlem5  48196  sin5t  48197  cos5t  48198  fldivmod  48687  fmtnorec2lem  48900  fmtnorec3  48906  fmtnorec4  48907  fmtnoprmfac1  48923  fmtnoprmfac2  48925  fmtnofac2lem  48926  sfprmdvdsmersenne  48961  lighneallem3  48965  quad1  48991  requad01  48992  requad2  48994  opeoALTV  49055  perfectALTVlem2  49093  fppr2odd  49102  0nodd  49540  2nodd  49542  2zlidl  49610  2zrngnmlid  49625  linplyfv  49711  adcnmulzlaz  49731  lazlinz  49733  lazaddcl  49738  altgsumbcALT  49796  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0sumshdiglem2  50065  nn0mullong  50068  itcovalt2lem2lem2  50117  ackval2  50125  submuladdmuld  50144  affinecomb2  50146  affineid  50147  1subrec1sub  50148  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  rrx2linest  50185  line2x  50197  line2y  50198  itschlc0yqe  50203  itsclc0yqsollem1  50205  itsclc0yqsol  50207  itscnhlc0xyqsol  50208  itschlc0xyqsol1  50209  itschlc0xyqsol  50210  itsclc0xyqsolr  50212  2itscplem1  50221  2itscplem2  50222  2itscplem3  50223  2itscp  50224  itscnhlinecirc02plem1  50225  itscnhlinecirc02plem2  50226  inlinecirc02plem  50229  inlinecirc02p  50230  sinhf  51239  coshf  51243  coshneg  51246  tanhvaltan  51248  sinhadd  51254  coshadd  51255  sinhsub  51256  coshsub  51257  tanhadd  51258  dvsec  51284  i2linesd  51303  aacllem  51367  crossp3d  51395  amgmwlem  51415  amgmlemALT  51416