Theorem mulcld 11253

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   · cmul 11132

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

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

This theorem is referenced by:  mul02lem1  11409  addrid  11413  cnegex  11414  kcnktkm1cn  11666  subaddmulsub  11698  mulsubaddmulsub  11699  receu  11880  divrec  11910  divcan3  11920  muldivdir  11932  subdivcomb1  11934  subdivcomb2  11935  divdivdiv  11940  divsubdiv  11955  lineq  12076  cru  12230  mul2lt0rlt0  13109  lincmb01cmp  13510  iccf1o  13511  flpmodeq  13889  moddiffl  13897  modvalp1  13905  modcyc  13921  modadd1  13923  modmuladdnn0  13931  modmul1  13940  modaddmulmod  13954  mulexpz  14118  expmulz  14124  binom3  14240  bernneq  14245  mulsubdivbinom2  14278  muldivbinom2  14279  remullem  15145  cjreim2  15178  absimle  15326  abstri  15347  sqreulem  15376  sqreu  15377  bhmafibid1cn  15480  bhmafibid2cn  15481  bhmafibid1  15482  bhmafibid2  15483  mulcn2  15610  reccn2  15611  o1rlimmul  15633  rlimmul  15659  isummulc2  15776  fsummulc2  15798  fsumparts  15820  binomlem  15843  binom1dif  15847  incexclem  15850  incexc  15851  incexc2  15852  pwdif  15882  geomulcvg  15890  mertenslem1  15898  mertens  15900  fprodmul  15974  fprodn0f  16005  iprodmul  16017  binomfallfaclem1  16053  binomfallfaclem2  16054  binomrisefac  16056  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  bpoly4  16073  efaddlem  16107  sinadd  16180  cosadd  16181  tanaddlem  16182  tanadd  16183  addsin  16186  sincossq  16192  sin2t  16193  dvds2ln  16306  oddm1even  16360  pwp1fsum  16408  flodddiv4  16432  sadadd2lem2  16467  bezoutlem2  16557  bezoutlem3  16558  bezoutlem4  16559  lcmgcdlem  16623  phiprmpw  16793  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem16  16848  pcpremul  16861  pcaddlem  16906  fldivp1  16915  mul4sqlem  16971  4sqlem14  16976  vdwapun  16992  vdwlem2  17000  vdwlem6  17004  ablsimpgfindlem1  20088  zringlpirlem3  21423  znunit  21522  blcvx  24735  icopnfcnv  24889  cphipipcj  25150  cphipval2  25191  4cphipval2  25192  cphipval  25193  mbfmulc2re  25599  mbfmulc2  25614  itg1addlem4  25650  itg1addlem5  25651  itg1mulc  25655  mbfmul  25677  itgcl  25735  itgcnlem  25741  iblmulc2  25782  itgmulc2  25785  itgabs  25786  itgsplit  25787  dvmulbr  25891  dvmulbrOLD  25892  dvcmul  25897  dvcmulf  25898  dvexp  25907  dvmptcmul  25918  dvmptdiv  25928  dvexp3  25932  dvsincos  25935  cmvth  25945  cmvthOLD  25946  dvlipcn  25949  dvfsumabs  25979  dvfsumlem1  25982  ftc1lem4  25996  itgparts  26004  itgpowd  26007  plyf  26153  ply1termlem  26158  plyeq0lem  26165  plypf1  26167  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  coeidlem  26192  coeid3  26195  plyco  26196  coemullem  26205  coemulhi  26209  coemulc  26210  dgrcolem2  26230  plycjlem  26232  plyrecj  26237  dvply1  26241  vieta1lem2  26269  vieta1  26270  elqaalem3  26279  aareccl  26284  aalioulem1  26290  taylfvallem1  26314  tayl0  26319  dvtaylp  26328  taylthlem2  26332  taylthlem2OLD  26333  psergf  26371  radcnvlem1  26372  dvradcnv  26380  psercn2  26382  psercn2OLD  26383  pserdvlem2  26388  pserdv2  26390  abelthlem4  26394  abelthlem5  26395  abelthlem6  26396  abelthlem7  26398  abelthlem9  26400  tanregt0  26498  efgh  26500  efabl  26509  efsubm  26510  cosargd  26567  abslogle  26577  tanarg  26578  advlogexp  26614  logtayllem  26618  logtayl  26619  cxpadd  26638  mulcxp  26644  cxpmul  26647  cxpmul2  26648  cxpmul2z  26650  abscxp  26651  abscxp2  26652  dvcxp2  26700  abscxpbnd  26713  root1eq1  26715  cxpeq  26717  angcan  26762  pythag  26777  ssscongptld  26782  affineequiv  26783  affineequiv2  26784  affineequiv3  26785  affineequiv4  26786  chordthmlem2  26793  chordthmlem3  26794  chordthmlem4  26795  chordthmlem5  26796  heron  26798  quad2  26799  quad  26800  dcubic1lem  26803  dcubic2  26804  dcubic1  26805  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  binom4  26810  dquartlem1  26811  dquartlem2  26812  dquart  26813  quart1cl  26814  quart1lem  26815  quart1  26816  quartlem1  26817  quartlem2  26818  atantayl3  26899  leibpi  26902  birthdaylem2  26912  divsqrtsumo1  26944  cvxcl  26945  jensenlem2  26948  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamgulm2  26996  lgamcvg2  27015  gamcvg  27016  gamcvg2lem  27019  wilthlem2  27029  ftalem1  27033  ftalem2  27034  ftalem4  27036  ftalem5  27037  basellem2  27042  basellem3  27043  basellem8  27048  muinv  27153  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  logfacrlim  27185  logexprlim  27186  perfectlem2  27191  bposlem9  27253  gausslemma2dlem4  27330  lgsquad2lem1  27345  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2sqlem3  27381  2sqmod  27397  rplogsumlem1  27445  dchrisumlem2  27451  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasum2lem  27457  dchrvmasum2if  27458  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  rpvmasum2  27473  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrmusumlem  27483  dchrvmasumlem  27484  rplogsum  27488  mudivsum  27491  mulogsumlem  27492  mulogsum  27493  mulog2sumlem1  27495  mulog2sumlem2  27496  mulog2sumlem3  27497  vmalogdivsum  27500  logsqvma  27503  log2sumbnd  27505  selberglem1  27506  selberglem2  27507  selberglem3  27508  selberg  27509  selberg2lem  27511  selberg2  27512  selberg3lem1  27518  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrsumo1  27526  selbergr  27529  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntsval2  27537  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntlemb  27558  pntlemf  27566  pntlemo  27568  ostth2lem2  27595  ostth2lem3  27596  ttgcontlem1  28810  brbtwn2  28830  colinearalg  28835  ax5seglem2  28854  ax5seglem9  28862  axeuclidlem  28887  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  axcontlem8  28896  finsumvtxdg2ssteplem4  29474  ex-ind-dvds  30388  nrt2irr  30400  ipval2  30634  dipcl  30639  riesz3i  31989  re0cj  32667  pythagreim  32669  quad3d  32673  indsum  32784  indsumin  32785  dpfrac1  32812  wrdt2ind  32875  zringfrac  33515  ccfldsrarelvec  33658  ccfldextdgrr  33659  constrrtll  33711  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  constrconj  33725  constrfin  33726  constrelextdg2  33727  nn0constr  33741  constraddcl  33742  constrnegcl  33743  constrdircl  33745  iconstr  33746  constrremulcl  33747  constrrecl  33749  constrimcl  33750  constrmulcl  33751  constrreinvcl  33752  constrinvcl  33753  constrresqrtcl  33757  constrabscl  33758  constrsqrtcl  33759  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpiminply  33768  cos9thpinconstrlem1  33769  cnre2csqima  33888  rmulccn  33905  dya2icoseg  34255  oddpwdc  34332  eulerpartlems  34338  eulerpartlemsv3  34339  eulerpartlemgs2  34358  signsplypnf  34528  itgexpif  34584  breprexplemc  34610  breprexp  34611  vtscl  34616  vtsprod  34617  circlemeth  34618  logdivsqrle  34628  hgt750lemf  34631  hgt750leme  34636  subfacval2  35155  subfaclim  35156  resconn  35214  iprodgam  35705  fwddifnp1  36129  knoppcnlem10  36466  knoppndvlem2  36477  knoppndvlem7  36482  knoppndvlem9  36484  knoppndvlem11  36486  knoppndvlem14  36489  knoppndvlem16  36491  knoppndvlem17  36492  bj-subcom  37272  bj-bary1lem  37274  bj-bary1lem1  37275  bj-bary1  37276  iblmulc2nc  37655  itgmulc2nc  37658  itgabsnc  37659  ftc1cnnclem  37661  ftc1anclem3  37665  dvasin  37674  areacirclem1  37678  areacirclem4  37681  areacirc  37683  cntotbnd  37766  3factsumint1  41980  3factsumint3  41982  3factsumint4  41983  lcmineqlem2  41989  lcmineqlem6  41993  lcmineqlem8  41995  lcmineqlem10  41997  lcmineqlem11  41998  lcmineqlem12  41999  lcmineqlem16  42003  lcmineqlem18  42005  lcmineqlem23  42010  3lexlogpow5ineq5  42019  aks4d1p1p1  42022  dvrelogpow2b  42027  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij  42061  primrootspoweq0  42065  2np3bcnp1  42103  2ap1caineq  42104  oddnumth  42307  nicomachus  42308  sumcubes  42309  ef11d  42335  cxp112d  42337  cxp111d  42338  readvrec2  42351  sn-addlid  42394  sn-it0e0  42405  sn-negex12  42406  sn-mul01  42415  sn-mullid  42425  sn-0tie0  42429  sn-mul02  42430  cnreeu  42460  fltnltalem  42632  fltnlta  42633  cu3addd  42651  3cubeslem2  42655  3cubeslem3l  42656  3cubeslem3r  42657  3cubeslem4  42659  pellexlem1  42799  pellexlem2  42800  pellexlem6  42804  pell1234qrne0  42823  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell1234qrdich  42831  pell14qrdich  42839  pell1qrge1  42840  pell1qrgaplem  42843  rmspecsqrtnq  42876  qirropth  42878  rmxyneg  42891  rmxyadd  42892  rmxm1  42905  rmym1  42906  rmxluc  42907  rmyluc  42908  rmxdbl  42910  rmydbl  42911  jm2.18  42959  jm2.19lem1  42960  jm2.19lem2  42961  jm2.19lem4  42963  jm2.19  42964  jm2.22  42966  jm2.23  42967  jm2.25  42970  jm2.27c  42978  jm3.1lem2  42989  flcidc  43141  areaquad  43187  sqrtcval  43612  inductionexd  44126  imo72b2lem0  44136  int-leftdistd  44150  radcnvrat  44286  expgrowth  44307  binomcxplemwb  44320  binomcxplemnn0  44321  binomcxplemfrat  44323  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  sineq0ALT  44909  mul13d  45256  fperiodmullem  45280  fperiodmul  45281  divcan8d  45289  dmmcand  45290  ltdiv23neg  45369  mulc1cncfg  45566  mccllem  45574  clim1fr1  45578  mullimc  45593  mullimcf  45600  sumnnodd  45607  reclimc  45630  sinmulcos  45842  coskpi2  45843  cosknegpi  45846  dvsinexp  45888  dvasinbx  45897  dvdivf  45899  dvdivbd  45900  dvdivcncf  45904  dvbdfbdioolem2  45906  dvxpaek  45917  dvnxpaek  45919  dvnmul  45920  dvmptfprodlem  45921  dvnprodlem2  45924  itgsinexplem1  45931  itgsinexp  45932  itgcoscmulx  45946  itgsincmulx  45951  itgiccshift  45957  itgperiod  45958  stoweidlem1  45978  stoweidlem11  45988  stoweidlem13  45990  stoweidlem14  45991  stoweidlem17  45994  stoweidlem25  46002  stoweidlem26  46003  stoweidlem42  46019  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem8  46058  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  dirker2re  46069  dirkerdenne0  46070  dirkerper  46073  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem26  46110  fourierdlem30  46114  fourierdlem39  46123  fourierdlem42  46126  fourierdlem47  46130  fourierdlem48  46131  fourierdlem56  46139  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem65  46148  fourierdlem66  46149  fourierdlem68  46151  fourierdlem72  46155  fourierdlem73  46156  fourierdlem76  46159  fourierdlem80  46163  fourierdlem83  46166  fourierdlem85  46168  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem95  46178  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  elaa2lem  46210  etransclem8  46219  etransclem18  46229  etransclem20  46231  etransclem21  46232  etransclem23  46234  etransclem24  46235  etransclem31  46242  etransclem33  46244  etransclem35  46246  etransclem45  46256  etransclem46  46257  etransclem47  46258  etransclem48  46259  hoicvrrex  46533  hoidmvlelem2  46573  smfmullem1  46768  sigarim  46828  sigarac  46829  sigaraf  46830  sigarmf  46831  sigarls  46834  sigardiv  46838  sigarcol  46841  cevathlem1  46844  fldivmod  47315  fmtnorec2lem  47504  fmtnorec3  47510  fmtnorec4  47511  fmtnoprmfac1  47527  fmtnoprmfac2  47529  fmtnofac2lem  47530  sfprmdvdsmersenne  47565  lighneallem3  47569  quad1  47582  requad01  47583  requad2  47585  opeoALTV  47646  perfectALTVlem2  47684  fppr2odd  47693  0nodd  48093  2nodd  48095  2zlidl  48163  2zrngnmlid  48178  altgsumbcALT  48276  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdiglem2  48550  nn0mullong  48553  itcovalt2lem2lem2  48602  ackval2  48610  submuladdmuld  48629  affinecomb2  48631  affineid  48632  1subrec1sub  48633  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrx2linest  48670  line2x  48682  line2y  48683  itschlc0yqe  48688  itsclc0yqsollem1  48690  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itschlc0xyqsol  48695  itsclc0xyqsolr  48697  2itscplem1  48706  2itscplem2  48707  2itscplem3  48708  2itscp  48709  itscnhlinecirc02plem1  48710  itscnhlinecirc02plem2  48711  inlinecirc02plem  48714  inlinecirc02p  48715  i2linesd  49591  aacllem  49613  amgmwlem  49614  amgmlemALT  49615