Theorem mulcld 11135

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   · cmul 11014

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

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

This theorem is referenced by:  mul02lem1  11292  addrid  11296  cnegex  11297  kcnktkm1cn  11551  subaddmulsub  11583  mulsubaddmulsub  11584  receu  11765  divrec  11795  divcan3  11805  muldivdir  11817  subdivcomb1  11819  subdivcomb2  11820  divdivdiv  11825  divsubdiv  11840  lineq  11961  cru  12120  mul2lt0rlt0  12997  lincmb01cmp  13398  iccf1o  13399  flpmodeq  13778  moddiffl  13786  modvalp1  13794  modcyc  13810  modadd1  13812  modmuladdnn0  13822  modmul1  13831  modaddmulmod  13845  mulexpz  14009  expmulz  14015  binom3  14131  bernneq  14136  mulsubdivbinom2  14169  muldivbinom2  14170  remullem  15035  cjreim2  15068  absimle  15216  abstri  15238  sqreulem  15267  sqreu  15268  bhmafibid1cn  15373  bhmafibid2cn  15374  bhmafibid1  15375  bhmafibid2  15376  mulcn2  15503  reccn2  15504  o1rlimmul  15526  rlimmul  15552  isummulc2  15669  fsummulc2  15691  fsumparts  15713  binomlem  15736  binom1dif  15740  incexclem  15743  incexc  15744  incexc2  15745  pwdif  15775  geomulcvg  15783  mertenslem1  15791  mertens  15793  fprodmul  15867  fprodn0f  15898  iprodmul  15910  binomfallfaclem1  15946  binomfallfaclem2  15947  binomrisefac  15949  bpolycl  15959  bpolysum  15960  bpolydiflem  15961  bpoly4  15966  efaddlem  16000  sinadd  16073  cosadd  16074  tanaddlem  16075  tanadd  16076  addsin  16079  sincossq  16085  sin2t  16086  dvds2ln  16200  oddm1even  16254  pwp1fsum  16302  flodddiv4  16326  sadadd2lem2  16361  bezoutlem2  16451  bezoutlem3  16452  bezoutlem4  16453  lcmgcdlem  16517  phiprmpw  16687  pythagtriplem12  16738  pythagtriplem14  16740  pythagtriplem16  16742  pcpremul  16755  pcaddlem  16800  fldivp1  16809  mul4sqlem  16865  4sqlem14  16870  vdwapun  16886  vdwlem2  16894  vdwlem6  16898  ablsimpgfindlem1  19988  zringlpirlem3  21371  znunit  21470  blcvx  24684  icopnfcnv  24838  cphipipcj  25098  cphipval2  25139  4cphipval2  25140  cphipval  25141  mbfmulc2re  25547  mbfmulc2  25562  itg1addlem4  25598  itg1addlem5  25599  itg1mulc  25603  mbfmul  25625  itgcl  25683  itgcnlem  25689  iblmulc2  25730  itgmulc2  25733  itgabs  25734  itgsplit  25735  dvmulbr  25839  dvmulbrOLD  25840  dvcmul  25845  dvcmulf  25846  dvexp  25855  dvmptcmul  25866  dvmptdiv  25876  dvexp3  25880  dvsincos  25883  cmvth  25893  cmvthOLD  25894  dvlipcn  25897  dvfsumabs  25927  dvfsumlem1  25930  ftc1lem4  25944  itgparts  25952  itgpowd  25955  plyf  26101  ply1termlem  26106  plyeq0lem  26113  plypf1  26115  plyaddlem1  26116  plymullem1  26117  coeeulem  26127  coeidlem  26140  coeid3  26143  plyco  26144  coemullem  26153  coemulhi  26157  coemulc  26158  dgrcolem2  26178  plycjlem  26180  plyrecj  26185  dvply1  26189  vieta1lem2  26217  vieta1  26218  elqaalem3  26227  aareccl  26232  aalioulem1  26238  taylfvallem1  26262  tayl0  26267  dvtaylp  26276  taylthlem2  26280  taylthlem2OLD  26281  psergf  26319  radcnvlem1  26320  dvradcnv  26328  psercn2  26330  psercn2OLD  26331  pserdvlem2  26336  pserdv2  26338  abelthlem4  26342  abelthlem5  26343  abelthlem6  26344  abelthlem7  26346  abelthlem9  26348  tanregt0  26446  efgh  26448  efabl  26457  efsubm  26458  cosargd  26515  abslogle  26525  tanarg  26526  advlogexp  26562  logtayllem  26566  logtayl  26567  cxpadd  26586  mulcxp  26592  cxpmul  26595  cxpmul2  26596  cxpmul2z  26598  abscxp  26599  abscxp2  26600  dvcxp2  26648  abscxpbnd  26661  root1eq1  26663  cxpeq  26665  angcan  26710  pythag  26725  ssscongptld  26730  affineequiv  26731  affineequiv2  26732  affineequiv3  26733  affineequiv4  26734  chordthmlem2  26741  chordthmlem3  26742  chordthmlem4  26743  chordthmlem5  26744  heron  26746  quad2  26747  quad  26748  dcubic1lem  26751  dcubic2  26752  dcubic1  26753  dcubic  26754  mcubic  26755  cubic2  26756  cubic  26757  binom4  26758  dquartlem1  26759  dquartlem2  26760  dquart  26761  quart1cl  26762  quart1lem  26763  quart1  26764  quartlem1  26765  quartlem2  26766  atantayl3  26847  leibpi  26850  birthdaylem2  26860  divsqrtsumo1  26892  cvxcl  26893  jensenlem2  26896  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem4  26940  lgamgulmlem5  26941  lgamgulmlem6  26942  lgamgulm2  26944  lgamcvg2  26963  gamcvg  26964  gamcvg2lem  26967  wilthlem2  26977  ftalem1  26981  ftalem2  26982  ftalem4  26984  ftalem5  26985  basellem2  26990  basellem3  26991  basellem8  26996  muinv  27101  fsumdvdsmul  27103  fsumdvdsmulOLD  27105  logfacrlim  27133  logexprlim  27134  perfectlem2  27139  bposlem9  27201  gausslemma2dlem4  27278  lgsquad2lem1  27293  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2sqlem3  27329  2sqmod  27345  rplogsumlem1  27393  dchrisumlem2  27399  dchrisumlem3  27400  dchrmusum2  27403  dchrvmasumlem1  27404  dchrvmasum2lem  27405  dchrvmasum2if  27406  dchrvmasumlem3  27408  dchrvmasumiflem1  27410  dchrvmasumiflem2  27411  rpvmasum2  27421  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrmusumlem  27431  dchrvmasumlem  27432  rplogsum  27436  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  mulog2sumlem1  27443  mulog2sumlem2  27444  mulog2sumlem3  27445  vmalogdivsum  27448  logsqvma  27451  log2sumbnd  27453  selberglem1  27454  selberglem2  27455  selberglem3  27456  selberg  27457  selberg2lem  27459  selberg2  27460  selberg3lem1  27466  selberg3  27468  selberg4lem1  27469  selberg4  27470  pntrsumo1  27474  selbergr  27477  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntsval2  27485  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntlemb  27506  pntlemf  27514  pntlemo  27516  ostth2lem2  27543  ostth2lem3  27544  ttgcontlem1  28830  brbtwn2  28850  colinearalg  28855  ax5seglem2  28874  ax5seglem9  28882  axeuclidlem  28907  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  axcontlem8  28916  finsumvtxdg2ssteplem4  29494  ex-ind-dvds  30405  nrt2irr  30417  ipval2  30651  dipcl  30656  riesz3i  32006  re0cj  32687  pythagreim  32689  quad3d  32693  indsum  32804  indsumin  32805  dpfrac1  32832  wrdt2ind  32895  zringfrac  33491  ccfldsrarelvec  33638  ccfldextdgrr  33639  constrrtll  33698  constrrtlc1  33699  constrrtcclem  33701  constrrtcc  33702  constrconj  33712  constrfin  33713  constrelextdg2  33714  nn0constr  33728  constraddcl  33729  constrnegcl  33730  constrdircl  33732  iconstr  33733  constrremulcl  33734  constrrecl  33736  constrimcl  33737  constrmulcl  33738  constrreinvcl  33739  constrinvcl  33740  constrresqrtcl  33744  constrabscl  33745  constrsqrtcl  33746  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  cos9thpiminply  33755  cos9thpinconstrlem1  33756  cos9thpinconstrlem2  33757  cos9thpinconstr  33758  cnre2csqima  33878  rmulccn  33895  dya2icoseg  34245  oddpwdc  34322  eulerpartlems  34328  eulerpartlemsv3  34329  eulerpartlemgs2  34348  signsplypnf  34518  itgexpif  34574  breprexplemc  34600  breprexp  34601  vtscl  34606  vtsprod  34607  circlemeth  34608  logdivsqrle  34618  hgt750lemf  34621  hgt750leme  34626  subfacval2  35164  subfaclim  35165  resconn  35223  iprodgam  35719  fwddifnp1  36143  knoppcnlem10  36480  knoppndvlem2  36491  knoppndvlem7  36496  knoppndvlem9  36498  knoppndvlem11  36500  knoppndvlem14  36503  knoppndvlem16  36505  knoppndvlem17  36506  bj-subcom  37286  bj-bary1lem  37288  bj-bary1lem1  37289  bj-bary1  37290  iblmulc2nc  37669  itgmulc2nc  37672  itgabsnc  37673  ftc1cnnclem  37675  ftc1anclem3  37679  dvasin  37688  areacirclem1  37692  areacirclem4  37695  areacirc  37697  cntotbnd  37780  3factsumint1  41998  3factsumint3  42000  3factsumint4  42001  lcmineqlem2  42007  lcmineqlem6  42011  lcmineqlem8  42013  lcmineqlem10  42015  lcmineqlem11  42016  lcmineqlem12  42017  lcmineqlem16  42021  lcmineqlem18  42023  lcmineqlem23  42028  3lexlogpow5ineq5  42037  aks4d1p1p1  42040  dvrelogpow2b  42045  aks4d1p1p6  42050  aks4d1p1p7  42051  aks4d1p1p5  42052  primrootscoprmpow  42076  posbezout  42077  primrootscoprbij  42079  primrootspoweq0  42083  2np3bcnp1  42121  2ap1caineq  42122  oddnumth  42288  nicomachus  42289  sumcubes  42290  ef11d  42316  cxp112d  42318  cxp111d  42319  readvrec2  42338  sn-addlid  42381  sn-it0e0  42393  sn-negex12  42394  sn-mul01  42403  sn-mullid  42413  sn-0tie0  42428  sn-mul02  42429  cnreeu  42467  fltnltalem  42639  fltnlta  42640  cu3addd  42658  3cubeslem2  42662  3cubeslem3l  42663  3cubeslem3r  42664  3cubeslem4  42666  pellexlem1  42806  pellexlem2  42807  pellexlem6  42811  pell1234qrne0  42830  pell1234qrreccl  42831  pell1234qrmulcl  42832  pell1234qrdich  42838  pell14qrdich  42846  pell1qrge1  42847  pell1qrgaplem  42850  rmspecsqrtnq  42883  qirropth  42885  rmxyneg  42897  rmxyadd  42898  rmxm1  42911  rmym1  42912  rmxluc  42913  rmyluc  42914  rmxdbl  42916  rmydbl  42917  jm2.18  42965  jm2.19lem1  42966  jm2.19lem2  42967  jm2.19lem4  42969  jm2.19  42970  jm2.22  42972  jm2.23  42973  jm2.25  42976  jm2.27c  42984  jm3.1lem2  42995  flcidc  43147  areaquad  43193  sqrtcval  43618  inductionexd  44132  imo72b2lem0  44142  int-leftdistd  44156  radcnvrat  44291  expgrowth  44312  binomcxplemwb  44325  binomcxplemnn0  44326  binomcxplemfrat  44328  binomcxplemdvbinom  44330  binomcxplemnotnn0  44333  sineq0ALT  44914  mul13d  45266  fperiodmullem  45289  fperiodmul  45290  divcan8d  45298  dmmcand  45299  ltdiv23neg  45377  mulc1cncfg  45574  mccllem  45582  clim1fr1  45586  mullimc  45601  mullimcf  45608  sumnnodd  45615  reclimc  45638  sinmulcos  45850  coskpi2  45851  cosknegpi  45854  dvsinexp  45896  dvasinbx  45905  dvdivf  45907  dvdivbd  45908  dvdivcncf  45912  dvbdfbdioolem2  45914  dvxpaek  45925  dvnxpaek  45927  dvnmul  45928  dvmptfprodlem  45929  dvnprodlem2  45932  itgsinexplem1  45939  itgsinexp  45940  itgcoscmulx  45954  itgsincmulx  45959  itgiccshift  45965  itgperiod  45966  stoweidlem1  45986  stoweidlem11  45996  stoweidlem13  45998  stoweidlem14  45999  stoweidlem17  46002  stoweidlem25  46010  stoweidlem26  46011  stoweidlem42  46027  wallispilem4  46053  wallispilem5  46054  wallispi  46055  wallispi2lem1  46056  wallispi2lem2  46057  wallispi2  46058  stirlinglem1  46059  stirlinglem3  46061  stirlinglem4  46062  stirlinglem5  46063  stirlinglem6  46064  stirlinglem7  46065  stirlinglem8  46066  stirlinglem10  46068  stirlinglem11  46069  stirlinglem12  46070  stirlinglem13  46071  stirlinglem14  46072  stirlinglem15  46073  dirker2re  46077  dirkerdenne0  46078  dirkerper  46081  dirkertrigeqlem1  46083  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  dirkertrigeq  46086  dirkeritg  46087  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem26  46118  fourierdlem30  46122  fourierdlem39  46131  fourierdlem42  46134  fourierdlem47  46138  fourierdlem48  46139  fourierdlem56  46147  fourierdlem57  46148  fourierdlem58  46149  fourierdlem62  46153  fourierdlem65  46156  fourierdlem66  46157  fourierdlem68  46159  fourierdlem72  46163  fourierdlem73  46164  fourierdlem76  46167  fourierdlem80  46171  fourierdlem83  46174  fourierdlem85  46176  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem95  46186  fourierdlem97  46188  fourierdlem101  46192  fourierdlem103  46194  fourierdlem104  46195  fourierdlem111  46202  sqwvfoura  46213  sqwvfourb  46214  fourierswlem  46215  fouriersw  46216  elaa2lem  46218  etransclem8  46227  etransclem18  46237  etransclem20  46239  etransclem21  46240  etransclem23  46242  etransclem24  46243  etransclem31  46250  etransclem33  46252  etransclem35  46254  etransclem45  46264  etransclem46  46265  etransclem47  46266  etransclem48  46267  hoicvrrex  46541  hoidmvlelem2  46581  smfmullem1  46776  sigarim  46836  sigarac  46837  sigaraf  46838  sigarmf  46839  sigarls  46842  sigardiv  46846  sigarcol  46849  cevathlem1  46852  fldivmod  47326  fmtnorec2lem  47530  fmtnorec3  47536  fmtnorec4  47537  fmtnoprmfac1  47553  fmtnoprmfac2  47555  fmtnofac2lem  47556  sfprmdvdsmersenne  47591  lighneallem3  47595  quad1  47608  requad01  47609  requad2  47611  opeoALTV  47672  perfectALTVlem2  47710  fppr2odd  47719  0nodd  48158  2nodd  48160  2zlidl  48228  2zrngnmlid  48243  altgsumbcALT  48341  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem2  48611  nn0mullong  48614  itcovalt2lem2lem2  48663  ackval2  48671  submuladdmuld  48690  affinecomb2  48692  affineid  48693  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2linest  48731  line2x  48743  line2y  48744  itschlc0yqe  48749  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  itsclc0xyqsolr  48758  2itscplem1  48767  2itscplem2  48768  2itscplem3  48769  2itscp  48770  itscnhlinecirc02plem1  48771  itscnhlinecirc02plem2  48772  inlinecirc02plem  48775  inlinecirc02p  48776  i2linesd  49768  aacllem  49790  amgmwlem  49791  amgmlemALT  49792