Theorem mulcld 11234

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

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

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  mul02lem1  11390  addrid  11394  cnegex  11395  kcnktkm1cn  11645  subaddmulsub  11677  mulsubaddmulsub  11678  receu  11859  divrec  11888  divcan3  11898  muldivdir  11907  subdivcomb1  11909  subdivcomb2  11910  divdivdiv  11915  divsubdiv  11930  lineq  12051  cru  12204  mul2lt0rlt0  13076  lincmb01cmp  13472  iccf1o  13473  flpmodeq  13839  moddiffl  13847  modvalp1  13855  modcyc  13871  modadd1  13873  modmuladdnn0  13880  modmul1  13889  modaddmulmod  13903  mulexpz  14068  expmulz  14074  binom3  14187  bernneq  14192  mulsubdivbinom2  14222  muldivbinom2  14223  remullem  15075  cjreim2  15108  absimle  15256  abstri  15277  sqreulem  15306  sqreu  15307  bhmafibid1cn  15410  bhmafibid2cn  15411  bhmafibid1  15412  bhmafibid2  15413  mulcn2  15540  reccn2  15541  o1rlimmul  15563  rlimmul  15590  isummulc2  15708  fsummulc2  15730  fsumparts  15752  binomlem  15775  binom1dif  15779  incexclem  15782  incexc  15783  incexc2  15784  pwdif  15814  geomulcvg  15822  mertenslem1  15830  mertens  15832  fprodmul  15904  fprodn0f  15935  iprodmul  15947  binomfallfaclem1  15983  binomfallfaclem2  15984  binomrisefac  15986  bpolycl  15996  bpolysum  15997  bpolydiflem  15998  bpoly4  16003  efaddlem  16036  sinadd  16107  cosadd  16108  tanaddlem  16109  tanadd  16110  addsin  16113  sincossq  16119  sin2t  16120  dvds2ln  16232  oddm1even  16286  pwp1fsum  16334  flodddiv4  16356  sadadd2lem2  16391  bezoutlem2  16482  bezoutlem3  16483  bezoutlem4  16484  lcmgcdlem  16543  phiprmpw  16709  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  pcpremul  16776  pcaddlem  16821  fldivp1  16830  mul4sqlem  16886  4sqlem14  16891  vdwapun  16907  vdwlem2  16915  vdwlem6  16919  ablsimpgfindlem1  19977  zringlpirlem3  21034  znunit  21119  blcvx  24314  icopnfcnv  24458  cphipipcj  24717  cphipval2  24758  4cphipval2  24759  cphipval  24760  mbfmulc2re  25165  mbfmulc2  25180  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  itg1mulc  25222  mbfmul  25244  itgcl  25301  itgcnlem  25307  iblmulc2  25348  itgmulc2  25351  itgabs  25352  itgsplit  25353  dvmulbr  25456  dvcmul  25461  dvcmulf  25462  dvexp  25470  dvmptcmul  25481  dvmptdiv  25491  dvexp3  25495  dvsincos  25498  cmvth  25508  dvlipcn  25511  dvfsumabs  25540  dvfsumlem1  25543  ftc1lem4  25556  itgparts  25564  itgpowd  25567  plyf  25712  ply1termlem  25717  plyeq0lem  25724  plypf1  25726  plyaddlem1  25727  plymullem1  25728  coeeulem  25738  coeidlem  25751  coeid3  25754  plyco  25755  coemullem  25764  coemulhi  25768  coemulc  25769  dgrcolem2  25788  plycjlem  25790  plyrecj  25793  dvply1  25797  vieta1lem2  25824  vieta1  25825  elqaalem3  25834  aareccl  25839  aalioulem1  25845  taylfvallem1  25869  tayl0  25874  dvtaylp  25882  taylthlem2  25886  psergf  25924  radcnvlem1  25925  dvradcnv  25933  psercn2  25935  pserdvlem2  25940  pserdv2  25942  abelthlem4  25946  abelthlem5  25947  abelthlem6  25948  abelthlem7  25950  abelthlem9  25952  tanregt0  26048  efgh  26050  efabl  26059  efsubm  26060  cosargd  26116  abslogle  26126  tanarg  26127  advlogexp  26163  logtayllem  26167  logtayl  26168  cxpadd  26187  mulcxp  26193  cxpmul  26196  cxpmul2  26197  cxpmul2z  26199  abscxp  26200  abscxp2  26201  dvcxp2  26249  abscxpbnd  26261  root1eq1  26263  cxpeq  26265  angcan  26307  pythag  26322  ssscongptld  26327  affineequiv  26328  affineequiv2  26329  affineequiv3  26330  affineequiv4  26331  chordthmlem2  26338  chordthmlem3  26339  chordthmlem4  26340  chordthmlem5  26341  heron  26343  quad2  26344  quad  26345  dcubic1lem  26348  dcubic2  26349  dcubic1  26350  dcubic  26351  mcubic  26352  cubic2  26353  cubic  26354  binom4  26355  dquartlem1  26356  dquartlem2  26357  dquart  26358  quart1cl  26359  quart1lem  26360  quart1  26361  quartlem1  26362  quartlem2  26363  atantayl3  26444  leibpi  26447  birthdaylem2  26457  divsqrtsumo1  26488  cvxcl  26489  jensenlem2  26492  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamgulm2  26540  lgamcvg2  26559  gamcvg  26560  gamcvg2lem  26563  wilthlem2  26573  ftalem1  26577  ftalem2  26578  ftalem4  26580  ftalem5  26581  basellem2  26586  basellem3  26587  basellem8  26592  muinv  26697  fsumdvdsmul  26699  logfacrlim  26727  logexprlim  26728  perfectlem2  26733  bposlem9  26795  gausslemma2dlem4  26872  lgsquad2lem1  26887  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2sqlem3  26923  2sqmod  26939  rplogsumlem1  26987  dchrisumlem2  26993  dchrisumlem3  26994  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrvmasum2if  27000  dchrvmasumlem3  27002  dchrvmasumiflem1  27004  dchrvmasumiflem2  27005  rpvmasum2  27015  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrmusumlem  27025  dchrvmasumlem  27026  rplogsum  27030  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  mulog2sumlem1  27037  mulog2sumlem2  27038  mulog2sumlem3  27039  vmalogdivsum  27042  logsqvma  27045  log2sumbnd  27047  selberglem1  27048  selberglem2  27049  selberglem3  27050  selberg  27051  selberg2lem  27053  selberg2  27054  selberg3lem1  27060  selberg3  27062  selberg4lem1  27063  selberg4  27064  pntrsumo1  27068  selbergr  27071  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntsval2  27079  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntlemb  27100  pntlemf  27108  pntlemo  27110  ostth2lem2  27137  ostth2lem3  27138  ttgcontlem1  28142  brbtwn2  28163  colinearalg  28168  ax5seglem2  28187  ax5seglem9  28195  axeuclidlem  28220  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  axcontlem8  28229  finsumvtxdg2ssteplem4  28805  ex-ind-dvds  29714  nrt2irr  29726  ipval2  29960  dipcl  29965  riesz3i  31315  dpfrac1  32058  wrdt2ind  32117  ccfldsrarelvec  32745  ccfldextdgrr  32746  cnre2csqima  32891  rmulccn  32908  indsum  33019  indsumin  33020  dya2icoseg  33276  oddpwdc  33353  eulerpartlems  33359  eulerpartlemsv3  33360  eulerpartlemgs2  33379  signsplypnf  33561  itgexpif  33618  breprexplemc  33644  breprexp  33645  vtscl  33650  vtsprod  33651  circlemeth  33652  logdivsqrle  33662  hgt750lemf  33665  hgt750leme  33670  subfacval2  34178  subfaclim  34179  resconn  34237  iprodgam  34712  fwddifnp1  35137  mpomulcn  35162  gg-dvmulbr  35175  gg-psercn2  35178  gg-rmulccn  35179  gg-cmvth  35181  knoppndvlem2  35389  knoppndvlem7  35394  knoppndvlem9  35396  knoppndvlem11  35398  knoppndvlem14  35401  knoppndvlem16  35403  knoppndvlem17  35404  bj-subcom  36189  bj-bary1lem  36191  bj-bary1lem1  36192  bj-bary1  36193  iblmulc2nc  36553  itgmulc2nc  36556  itgabsnc  36557  ftc1cnnclem  36559  ftc1anclem3  36563  dvasin  36572  areacirclem1  36576  areacirclem4  36579  areacirc  36581  cntotbnd  36664  3factsumint1  40886  3factsumint3  40888  3factsumint4  40889  lcmineqlem2  40895  lcmineqlem6  40899  lcmineqlem8  40901  lcmineqlem10  40903  lcmineqlem11  40904  lcmineqlem12  40905  lcmineqlem16  40909  lcmineqlem18  40911  lcmineqlem23  40916  3lexlogpow5ineq5  40925  aks4d1p1p1  40928  dvrelogpow2b  40933  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  2np3bcnp1  40960  2ap1caineq  40961  oddnumth  41209  nicomachus  41210  sumcubes  41211  sn-addlid  41277  sn-it0e0  41288  sn-negex12  41289  sn-mul01  41298  sn-mullid  41308  sn-0tie0  41312  sn-mul02  41313  cnreeu  41341  fltnltalem  41404  fltnlta  41405  cu3addd  41418  3cubeslem2  41423  3cubeslem3l  41424  3cubeslem3r  41425  3cubeslem4  41427  pellexlem1  41567  pellexlem2  41568  pellexlem6  41572  pell1234qrne0  41591  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell1234qrdich  41599  pell14qrdich  41607  pell1qrge1  41608  pell1qrgaplem  41611  rmspecsqrtnq  41644  qirropth  41646  rmxyneg  41659  rmxyadd  41660  rmxm1  41673  rmym1  41674  rmxluc  41675  rmyluc  41676  rmxdbl  41678  rmydbl  41679  jm2.18  41727  jm2.19lem1  41728  jm2.19lem2  41729  jm2.19lem4  41731  jm2.19  41732  jm2.22  41734  jm2.23  41735  jm2.25  41738  jm2.27c  41746  jm3.1lem2  41757  flcidc  41916  areaquad  41965  sqrtcval  42392  inductionexd  42906  imo72b2lem0  42917  int-leftdistd  42931  radcnvrat  43073  expgrowth  43094  binomcxplemwb  43107  binomcxplemnn0  43108  binomcxplemfrat  43110  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  sineq0ALT  43698  mul13d  43989  fperiodmullem  44013  fperiodmul  44014  divcan8d  44022  dmmcand  44023  ltdiv23neg  44104  mulc1cncfg  44305  mccllem  44313  clim1fr1  44317  mullimc  44332  mullimcf  44339  sumnnodd  44346  reclimc  44369  sinmulcos  44581  coskpi2  44582  cosknegpi  44585  dvsinexp  44627  dvasinbx  44636  dvdivf  44638  dvdivbd  44639  dvdivcncf  44643  dvbdfbdioolem2  44645  dvxpaek  44656  dvnxpaek  44658  dvnmul  44659  dvmptfprodlem  44660  dvnprodlem2  44663  itgsinexplem1  44670  itgsinexp  44671  itgcoscmulx  44685  itgsincmulx  44690  itgiccshift  44696  itgperiod  44697  stoweidlem1  44717  stoweidlem11  44727  stoweidlem13  44729  stoweidlem14  44730  stoweidlem17  44733  stoweidlem25  44741  stoweidlem26  44742  stoweidlem42  44758  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  wallispi2  44789  stirlinglem1  44790  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem8  44797  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  dirker2re  44808  dirkerdenne0  44809  dirkerper  44812  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkeritg  44818  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem26  44849  fourierdlem30  44853  fourierdlem39  44862  fourierdlem42  44865  fourierdlem47  44869  fourierdlem48  44870  fourierdlem56  44878  fourierdlem57  44879  fourierdlem58  44880  fourierdlem62  44884  fourierdlem65  44887  fourierdlem66  44888  fourierdlem68  44890  fourierdlem72  44894  fourierdlem73  44895  fourierdlem76  44898  fourierdlem80  44902  fourierdlem83  44905  fourierdlem85  44907  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem95  44917  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  elaa2lem  44949  etransclem8  44958  etransclem18  44968  etransclem20  44970  etransclem21  44971  etransclem23  44973  etransclem24  44974  etransclem31  44981  etransclem33  44983  etransclem35  44985  etransclem45  44995  etransclem46  44996  etransclem47  44997  etransclem48  44998  hoicvrrex  45272  hoidmvlelem2  45312  smfmullem1  45507  sigarim  45567  sigarac  45568  sigaraf  45569  sigarmf  45570  sigarls  45573  sigardiv  45577  sigarcol  45580  cevathlem1  45583  fmtnorec2lem  46210  fmtnorec3  46216  fmtnorec4  46217  fmtnoprmfac1  46233  fmtnoprmfac2  46235  fmtnofac2lem  46236  sfprmdvdsmersenne  46271  lighneallem3  46275  quad1  46288  requad01  46289  requad2  46291  opeoALTV  46352  perfectALTVlem2  46390  fppr2odd  46399  0nodd  46580  2nodd  46582  2zlidl  46832  2zrngnmlid  46847  altgsumbcALT  47029  fldivmod  47204  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  nn0sumshdiglem2  47308  nn0mullong  47311  itcovalt2lem2lem2  47360  ackval2  47368  submuladdmuld  47387  affinecomb2  47389  affineid  47390  1subrec1sub  47391  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  rrx2linest  47428  line2x  47440  line2y  47441  itschlc0yqe  47446  itsclc0yqsollem1  47448  itsclc0yqsol  47450  itscnhlc0xyqsol  47451  itschlc0xyqsol1  47452  itschlc0xyqsol  47453  itsclc0xyqsolr  47455  2itscplem1  47464  2itscplem2  47465  2itscplem3  47466  2itscp  47467  itscnhlinecirc02plem1  47468  itscnhlinecirc02plem2  47469  inlinecirc02plem  47472  inlinecirc02p  47473  i2linesd  47826  aacllem  47848  amgmwlem  47849  amgmlemALT  47850