Theorem mulcld 11201

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

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

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

This theorem is referenced by:  mul02lem1  11357  addrid  11361  cnegex  11362  kcnktkm1cn  11616  subaddmulsub  11648  mulsubaddmulsub  11649  receu  11830  divrec  11860  divcan3  11870  muldivdir  11882  subdivcomb1  11884  subdivcomb2  11885  divdivdiv  11890  divsubdiv  11905  lineq  12026  cru  12185  mul2lt0rlt0  13062  lincmb01cmp  13463  iccf1o  13464  flpmodeq  13843  moddiffl  13851  modvalp1  13859  modcyc  13875  modadd1  13877  modmuladdnn0  13887  modmul1  13896  modaddmulmod  13910  mulexpz  14074  expmulz  14080  binom3  14196  bernneq  14201  mulsubdivbinom2  14234  muldivbinom2  14235  remullem  15101  cjreim2  15134  absimle  15282  abstri  15304  sqreulem  15333  sqreu  15334  bhmafibid1cn  15439  bhmafibid2cn  15440  bhmafibid1  15441  bhmafibid2  15442  mulcn2  15569  reccn2  15570  o1rlimmul  15592  rlimmul  15618  isummulc2  15735  fsummulc2  15757  fsumparts  15779  binomlem  15802  binom1dif  15806  incexclem  15809  incexc  15810  incexc2  15811  pwdif  15841  geomulcvg  15849  mertenslem1  15857  mertens  15859  fprodmul  15933  fprodn0f  15964  iprodmul  15976  binomfallfaclem1  16012  binomfallfaclem2  16013  binomrisefac  16015  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  bpoly4  16032  efaddlem  16066  sinadd  16139  cosadd  16140  tanaddlem  16141  tanadd  16142  addsin  16145  sincossq  16151  sin2t  16152  dvds2ln  16266  oddm1even  16320  pwp1fsum  16368  flodddiv4  16392  sadadd2lem2  16427  bezoutlem2  16517  bezoutlem3  16518  bezoutlem4  16519  lcmgcdlem  16583  phiprmpw  16753  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem16  16808  pcpremul  16821  pcaddlem  16866  fldivp1  16875  mul4sqlem  16931  4sqlem14  16936  vdwapun  16952  vdwlem2  16960  vdwlem6  16964  ablsimpgfindlem1  20046  zringlpirlem3  21381  znunit  21480  blcvx  24693  icopnfcnv  24847  cphipipcj  25107  cphipval2  25148  4cphipval2  25149  cphipval  25150  mbfmulc2re  25556  mbfmulc2  25571  itg1addlem4  25607  itg1addlem5  25608  itg1mulc  25612  mbfmul  25634  itgcl  25692  itgcnlem  25698  iblmulc2  25739  itgmulc2  25742  itgabs  25743  itgsplit  25744  dvmulbr  25848  dvmulbrOLD  25849  dvcmul  25854  dvcmulf  25855  dvexp  25864  dvmptcmul  25875  dvmptdiv  25885  dvexp3  25889  dvsincos  25892  cmvth  25902  cmvthOLD  25903  dvlipcn  25906  dvfsumabs  25936  dvfsumlem1  25939  ftc1lem4  25953  itgparts  25961  itgpowd  25964  plyf  26110  ply1termlem  26115  plyeq0lem  26122  plypf1  26124  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coeidlem  26149  coeid3  26152  plyco  26153  coemullem  26162  coemulhi  26166  coemulc  26167  dgrcolem2  26187  plycjlem  26189  plyrecj  26194  dvply1  26198  vieta1lem2  26226  vieta1  26227  elqaalem3  26236  aareccl  26241  aalioulem1  26247  taylfvallem1  26271  tayl0  26276  dvtaylp  26285  taylthlem2  26289  taylthlem2OLD  26290  psergf  26328  radcnvlem1  26329  dvradcnv  26337  psercn2  26339  psercn2OLD  26340  pserdvlem2  26345  pserdv2  26347  abelthlem4  26351  abelthlem5  26352  abelthlem6  26353  abelthlem7  26355  abelthlem9  26357  tanregt0  26455  efgh  26457  efabl  26466  efsubm  26467  cosargd  26524  abslogle  26534  tanarg  26535  advlogexp  26571  logtayllem  26575  logtayl  26576  cxpadd  26595  mulcxp  26601  cxpmul  26604  cxpmul2  26605  cxpmul2z  26607  abscxp  26608  abscxp2  26609  dvcxp2  26657  abscxpbnd  26670  root1eq1  26672  cxpeq  26674  angcan  26719  pythag  26734  ssscongptld  26739  affineequiv  26740  affineequiv2  26741  affineequiv3  26742  affineequiv4  26743  chordthmlem2  26750  chordthmlem3  26751  chordthmlem4  26752  chordthmlem5  26753  heron  26755  quad2  26756  quad  26757  dcubic1lem  26760  dcubic2  26761  dcubic1  26762  dcubic  26763  mcubic  26764  cubic2  26765  cubic  26766  binom4  26767  dquartlem1  26768  dquartlem2  26769  dquart  26770  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem1  26774  quartlem2  26775  atantayl3  26856  leibpi  26859  birthdaylem2  26869  divsqrtsumo1  26901  cvxcl  26902  jensenlem2  26905  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamgulm2  26953  lgamcvg2  26972  gamcvg  26973  gamcvg2lem  26976  wilthlem2  26986  ftalem1  26990  ftalem2  26991  ftalem4  26993  ftalem5  26994  basellem2  26999  basellem3  27000  basellem8  27005  muinv  27110  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  logfacrlim  27142  logexprlim  27143  perfectlem2  27148  bposlem9  27210  gausslemma2dlem4  27287  lgsquad2lem1  27302  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2sqlem3  27338  2sqmod  27354  rplogsumlem1  27402  dchrisumlem2  27408  dchrisumlem3  27409  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasum2if  27415  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  rpvmasum2  27430  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrmusumlem  27440  dchrvmasumlem  27441  rplogsum  27445  mudivsum  27448  mulogsumlem  27449  mulogsum  27450  mulog2sumlem1  27452  mulog2sumlem2  27453  mulog2sumlem3  27454  vmalogdivsum  27457  logsqvma  27460  log2sumbnd  27462  selberglem1  27463  selberglem2  27464  selberglem3  27465  selberg  27466  selberg2lem  27468  selberg2  27469  selberg3lem1  27475  selberg3  27477  selberg4lem1  27478  selberg4  27479  pntrsumo1  27483  selbergr  27486  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntsval2  27494  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntlemb  27515  pntlemf  27523  pntlemo  27525  ostth2lem2  27552  ostth2lem3  27553  ttgcontlem1  28819  brbtwn2  28839  colinearalg  28844  ax5seglem2  28863  ax5seglem9  28871  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  finsumvtxdg2ssteplem4  29483  ex-ind-dvds  30397  nrt2irr  30409  ipval2  30643  dipcl  30648  riesz3i  31998  re0cj  32674  pythagreim  32676  quad3d  32680  indsum  32791  indsumin  32792  dpfrac1  32819  wrdt2ind  32882  zringfrac  33532  ccfldsrarelvec  33673  ccfldextdgrr  33674  constrrtll  33728  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  constrconj  33742  constrfin  33743  constrelextdg2  33744  nn0constr  33758  constraddcl  33759  constrnegcl  33760  constrdircl  33762  iconstr  33763  constrremulcl  33764  constrrecl  33766  constrimcl  33767  constrmulcl  33768  constrreinvcl  33769  constrinvcl  33770  constrresqrtcl  33774  constrabscl  33775  constrsqrtcl  33776  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminply  33785  cos9thpinconstrlem1  33786  cos9thpinconstrlem2  33787  cos9thpinconstr  33788  cnre2csqima  33908  rmulccn  33925  dya2icoseg  34275  oddpwdc  34352  eulerpartlems  34358  eulerpartlemsv3  34359  eulerpartlemgs2  34378  signsplypnf  34548  itgexpif  34604  breprexplemc  34630  breprexp  34631  vtscl  34636  vtsprod  34637  circlemeth  34638  logdivsqrle  34648  hgt750lemf  34651  hgt750leme  34656  subfacval2  35181  subfaclim  35182  resconn  35240  iprodgam  35736  fwddifnp1  36160  knoppcnlem10  36497  knoppndvlem2  36508  knoppndvlem7  36513  knoppndvlem9  36515  knoppndvlem11  36517  knoppndvlem14  36520  knoppndvlem16  36522  knoppndvlem17  36523  bj-subcom  37303  bj-bary1lem  37305  bj-bary1lem1  37306  bj-bary1  37307  iblmulc2nc  37686  itgmulc2nc  37689  itgabsnc  37690  ftc1cnnclem  37692  ftc1anclem3  37696  dvasin  37705  areacirclem1  37709  areacirclem4  37712  areacirc  37714  cntotbnd  37797  3factsumint1  42016  3factsumint3  42018  3factsumint4  42019  lcmineqlem2  42025  lcmineqlem6  42029  lcmineqlem8  42031  lcmineqlem10  42033  lcmineqlem11  42034  lcmineqlem12  42035  lcmineqlem16  42039  lcmineqlem18  42041  lcmineqlem23  42046  3lexlogpow5ineq5  42055  aks4d1p1p1  42058  dvrelogpow2b  42063  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  primrootscoprmpow  42094  posbezout  42095  primrootscoprbij  42097  primrootspoweq0  42101  2np3bcnp1  42139  2ap1caineq  42140  oddnumth  42306  nicomachus  42307  sumcubes  42308  ef11d  42334  cxp112d  42336  cxp111d  42337  readvrec2  42356  sn-addlid  42399  sn-it0e0  42411  sn-negex12  42412  sn-mul01  42421  sn-mullid  42431  sn-0tie0  42446  sn-mul02  42447  cnreeu  42485  fltnltalem  42657  fltnlta  42658  cu3addd  42676  3cubeslem2  42680  3cubeslem3l  42681  3cubeslem3r  42682  3cubeslem4  42684  pellexlem1  42824  pellexlem2  42825  pellexlem6  42829  pell1234qrne0  42848  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell1234qrdich  42856  pell14qrdich  42864  pell1qrge1  42865  pell1qrgaplem  42868  rmspecsqrtnq  42901  qirropth  42903  rmxyneg  42916  rmxyadd  42917  rmxm1  42930  rmym1  42931  rmxluc  42932  rmyluc  42933  rmxdbl  42935  rmydbl  42936  jm2.18  42984  jm2.19lem1  42985  jm2.19lem2  42986  jm2.19lem4  42988  jm2.19  42989  jm2.22  42991  jm2.23  42992  jm2.25  42995  jm2.27c  43003  jm3.1lem2  43014  flcidc  43166  areaquad  43212  sqrtcval  43637  inductionexd  44151  imo72b2lem0  44161  int-leftdistd  44175  radcnvrat  44310  expgrowth  44331  binomcxplemwb  44344  binomcxplemnn0  44345  binomcxplemfrat  44347  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  sineq0ALT  44933  mul13d  45285  fperiodmullem  45308  fperiodmul  45309  divcan8d  45317  dmmcand  45318  ltdiv23neg  45397  mulc1cncfg  45594  mccllem  45602  clim1fr1  45606  mullimc  45621  mullimcf  45628  sumnnodd  45635  reclimc  45658  sinmulcos  45870  coskpi2  45871  cosknegpi  45874  dvsinexp  45916  dvasinbx  45925  dvdivf  45927  dvdivbd  45928  dvdivcncf  45932  dvbdfbdioolem2  45934  dvxpaek  45945  dvnxpaek  45947  dvnmul  45948  dvmptfprodlem  45949  dvnprodlem2  45952  itgsinexplem1  45959  itgsinexp  45960  itgcoscmulx  45974  itgsincmulx  45979  itgiccshift  45985  itgperiod  45986  stoweidlem1  46006  stoweidlem11  46016  stoweidlem13  46018  stoweidlem14  46019  stoweidlem17  46022  stoweidlem25  46030  stoweidlem26  46031  stoweidlem42  46047  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  dirker2re  46097  dirkerdenne0  46098  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkeritg  46107  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem26  46138  fourierdlem30  46142  fourierdlem39  46151  fourierdlem42  46154  fourierdlem47  46158  fourierdlem48  46159  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem65  46176  fourierdlem66  46177  fourierdlem68  46179  fourierdlem72  46183  fourierdlem73  46184  fourierdlem76  46187  fourierdlem80  46191  fourierdlem83  46194  fourierdlem85  46196  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem95  46206  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  elaa2lem  46238  etransclem8  46247  etransclem18  46257  etransclem20  46259  etransclem21  46260  etransclem23  46262  etransclem24  46263  etransclem31  46270  etransclem33  46272  etransclem35  46274  etransclem45  46284  etransclem46  46285  etransclem47  46286  etransclem48  46287  hoicvrrex  46561  hoidmvlelem2  46601  smfmullem1  46796  sigarim  46856  sigarac  46857  sigaraf  46858  sigarmf  46859  sigarls  46862  sigardiv  46866  sigarcol  46869  cevathlem1  46872  fldivmod  47343  fmtnorec2lem  47547  fmtnorec3  47553  fmtnorec4  47554  fmtnoprmfac1  47570  fmtnoprmfac2  47572  fmtnofac2lem  47573  sfprmdvdsmersenne  47608  lighneallem3  47612  quad1  47625  requad01  47626  requad2  47628  opeoALTV  47689  perfectALTVlem2  47727  fppr2odd  47736  0nodd  48162  2nodd  48164  2zlidl  48232  2zrngnmlid  48247  altgsumbcALT  48345  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem2  48615  nn0mullong  48618  itcovalt2lem2lem2  48667  ackval2  48675  submuladdmuld  48694  affinecomb2  48696  affineid  48697  1subrec1sub  48698  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2linest  48735  line2x  48747  line2y  48748  itschlc0yqe  48753  itsclc0yqsollem1  48755  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itschlc0xyqsol  48760  itsclc0xyqsolr  48762  2itscplem1  48771  2itscplem2  48772  2itscplem3  48773  2itscp  48774  itscnhlinecirc02plem1  48775  itscnhlinecirc02plem2  48776  inlinecirc02plem  48779  inlinecirc02p  48780  i2linesd  49772  aacllem  49794  amgmwlem  49795  amgmlemALT  49796