Theorem mulcld 10661

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mul02lem1  10816  addid1  10820  cnegex  10821  kcnktkm1cn  11071  subaddmulsub  11103  mulsubaddmulsub  11104  receu  11285  divrec  11314  divcan3  11324  muldivdir  11333  subdivcomb1  11335  subdivcomb2  11336  divdivdiv  11341  divsubdiv  11356  lineq  11477  cru  11630  mul2lt0rlt0  12492  lincmb01cmp  12882  iccf1o  12883  flpmodeq  13243  moddiffl  13251  modvalp1  13259  modcyc  13275  modadd1  13277  modmuladdnn0  13284  modmul1  13293  modaddmulmod  13307  mulexpz  13470  expmulz  13476  binom3  13586  bernneq  13591  mulsubdivbinom2  13623  muldivbinom2  13624  remullem  14487  cjreim2  14520  absimle  14669  abstri  14690  sqreulem  14719  sqreu  14720  bhmafibid1cn  14823  bhmafibid2cn  14824  bhmafibid1  14825  bhmafibid2  14826  mulcn2  14952  reccn2  14953  o1rlimmul  14975  isummulc2  15117  fsummulc2  15139  fsumparts  15161  binomlem  15184  binom1dif  15188  incexclem  15191  incexc  15192  incexc2  15193  pwdif  15223  geomulcvg  15232  mertenslem1  15240  mertens  15242  fprodmul  15314  fprodn0f  15345  iprodmul  15357  binomfallfaclem1  15393  binomfallfaclem2  15394  binomrisefac  15396  bpolycl  15406  bpolysum  15407  bpolydiflem  15408  bpoly4  15413  efaddlem  15446  sinadd  15517  cosadd  15518  tanaddlem  15519  tanadd  15520  addsin  15523  sincossq  15529  sin2t  15530  dvds2ln  15642  oddm1even  15692  pwp1fsum  15742  flodddiv4  15764  sadadd2lem2  15799  bezoutlem2  15888  bezoutlem3  15889  bezoutlem4  15890  lcmgcdlem  15950  phiprmpw  16113  pythagtriplem12  16163  pythagtriplem14  16165  pythagtriplem16  16167  pcpremul  16180  pcaddlem  16224  fldivp1  16233  mul4sqlem  16289  4sqlem14  16294  vdwapun  16310  vdwlem2  16318  vdwlem6  16322  ablsimpgfindlem1  19229  zringlpirlem3  20633  znunit  20710  blcvx  23406  icopnfcnv  23546  cphipipcj  23804  cphipval2  23844  4cphipval2  23845  cphipval  23846  mbfmulc2re  24249  mbfmulc2  24264  itg1addlem4  24300  itg1addlem5  24301  itg1mulc  24305  mbfmul  24327  itgcl  24384  itgcnlem  24390  iblmulc2  24431  itgmulc2  24434  itgabs  24435  itgsplit  24436  dvmulbr  24536  dvcmul  24541  dvcmulf  24542  dvexp  24550  dvmptcmul  24561  dvmptdiv  24571  dvexp3  24575  dvsincos  24578  cmvth  24588  dvlipcn  24591  dvfsumabs  24620  dvfsumlem1  24623  ftc1lem4  24636  itgparts  24644  plyf  24788  ply1termlem  24793  plyeq0lem  24800  plypf1  24802  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeidlem  24827  coeid3  24830  plyco  24831  coemullem  24840  coemulhi  24844  coemulc  24845  dgrcolem2  24864  plycjlem  24866  plyrecj  24869  dvply1  24873  vieta1lem2  24900  vieta1  24901  elqaalem3  24910  aareccl  24915  aalioulem1  24921  taylfvallem1  24945  tayl0  24950  dvtaylp  24958  taylthlem2  24962  psergf  25000  radcnvlem1  25001  dvradcnv  25009  psercn2  25011  pserdvlem2  25016  pserdv2  25018  abelthlem4  25022  abelthlem5  25023  abelthlem6  25024  abelthlem7  25026  abelthlem9  25028  tanregt0  25123  efgh  25125  efabl  25134  efsubm  25135  cosargd  25191  abslogle  25201  tanarg  25202  advlogexp  25238  logtayllem  25242  logtayl  25243  cxpadd  25262  mulcxp  25268  cxpmul  25271  cxpmul2  25272  cxpmul2z  25274  abscxp  25275  abscxp2  25276  dvcxp2  25322  abscxpbnd  25334  root1eq1  25336  cxpeq  25338  angcan  25380  pythag  25395  ssscongptld  25400  affineequiv  25401  affineequiv2  25402  affineequiv3  25403  affineequiv4  25404  chordthmlem2  25411  chordthmlem3  25412  chordthmlem4  25413  chordthmlem5  25414  heron  25416  quad2  25417  quad  25418  dcubic1lem  25421  dcubic2  25422  dcubic1  25423  dcubic  25424  mcubic  25425  cubic2  25426  cubic  25427  binom4  25428  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1cl  25432  quart1lem  25433  quart1  25434  quartlem1  25435  quartlem2  25436  atantayl3  25517  leibpi  25520  birthdaylem2  25530  divsqrtsumo1  25561  cvxcl  25562  jensenlem2  25565  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamgulm2  25613  lgamcvg2  25632  gamcvg  25633  gamcvg2lem  25636  wilthlem2  25646  ftalem1  25650  ftalem2  25651  ftalem4  25653  ftalem5  25654  basellem2  25659  basellem3  25660  basellem8  25665  muinv  25770  fsumdvdsmul  25772  logfacrlim  25800  logexprlim  25801  perfectlem2  25806  bposlem9  25868  gausslemma2dlem4  25945  lgsquad2lem1  25960  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2sqlem3  25996  2sqmod  26012  rplogsumlem1  26060  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasum2if  26073  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrvmasumiflem2  26078  rpvmasum2  26088  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrmusumlem  26098  dchrvmasumlem  26099  rplogsum  26103  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  mulog2sumlem1  26110  mulog2sumlem2  26111  mulog2sumlem3  26112  vmalogdivsum  26115  logsqvma  26118  log2sumbnd  26120  selberglem1  26121  selberglem2  26122  selberglem3  26123  selberg  26124  selberg2lem  26126  selberg2  26127  selberg3lem1  26133  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  selbergr  26144  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntsval2  26152  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntlemb  26173  pntlemf  26181  pntlemo  26183  ostth2lem2  26210  ostth2lem3  26211  ttgcontlem1  26671  brbtwn2  26691  colinearalg  26696  ax5seglem2  26715  ax5seglem9  26723  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  finsumvtxdg2ssteplem4  27330  ex-ind-dvds  28240  ipval2  28484  dipcl  28489  riesz3i  29839  dpfrac1  30568  wrdt2ind  30627  ccfldsrarelvec  31056  ccfldextdgrr  31057  cnre2csqima  31154  rmulccn  31171  indsum  31280  indsumin  31281  dya2icoseg  31535  oddpwdc  31612  eulerpartlems  31618  eulerpartlemsv3  31619  eulerpartlemgs2  31638  signsplypnf  31820  itgexpif  31877  breprexplemc  31903  breprexp  31904  vtscl  31909  vtsprod  31910  circlemeth  31911  logdivsqrle  31921  hgt750lemf  31924  hgt750leme  31929  subfacval2  32434  subfaclim  32435  resconn  32493  iprodgam  32974  fwddifnp1  33626  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem9  33859  knoppndvlem11  33861  knoppndvlem14  33864  knoppndvlem16  33866  knoppndvlem17  33867  bj-subcom  34592  bj-bary1lem  34594  bj-bary1lem1  34595  bj-bary1  34596  iblmulc2nc  34972  itgmulc2nc  34975  itgabsnc  34976  ftc1cnnclem  34980  ftc1anclem3  34984  dvasin  34993  areacirclem1  34997  areacirclem4  35000  areacirc  35002  cntotbnd  35089  sn-addid2  39254  fltnltalem  39294  fltnlta  39295  cu3addd  39297  3cubeslem2  39302  3cubeslem3l  39303  3cubeslem3r  39304  3cubeslem4  39306  pellexlem1  39446  pellexlem2  39447  pellexlem6  39451  pell1234qrne0  39470  pell1234qrreccl  39471  pell1234qrmulcl  39472  pell1234qrdich  39478  pell14qrdich  39486  pell1qrge1  39487  pell1qrgaplem  39490  rmspecsqrtnq  39523  qirropth  39525  rmxyneg  39537  rmxyadd  39538  rmxm1  39551  rmym1  39552  rmxluc  39553  rmyluc  39554  rmxdbl  39556  rmydbl  39557  jm2.18  39605  jm2.19lem1  39606  jm2.19lem2  39607  jm2.19lem4  39609  jm2.19  39610  jm2.22  39612  jm2.23  39613  jm2.25  39616  jm2.27c  39624  jm3.1lem2  39635  flcidc  39794  itgpowd  39841  areaquad  39843  inductionexd  40525  imo72b2lem0  40536  int-leftdistd  40552  radcnvrat  40666  expgrowth  40687  binomcxplemwb  40700  binomcxplemnn0  40701  binomcxplemfrat  40703  binomcxplemdvbinom  40705  binomcxplemnotnn0  40708  sineq0ALT  41291  mul13d  41565  fperiodmullem  41590  fperiodmul  41591  divcan8d  41599  dmmcand  41600  ltdiv23neg  41686  mulc1cncfg  41890  mccllem  41898  clim1fr1  41902  mullimc  41917  mullimcf  41924  sumnnodd  41931  reclimc  41954  sinmulcos  42166  coskpi2  42167  cosknegpi  42170  dvsinexp  42215  dvasinbx  42225  dvdivf  42227  dvdivbd  42228  dvdivcncf  42232  dvbdfbdioolem2  42234  dvxpaek  42245  dvnxpaek  42247  dvnmul  42248  dvmptfprodlem  42249  dvnprodlem2  42252  itgsinexplem1  42259  itgsinexp  42260  itgcoscmulx  42274  itgsincmulx  42279  itgiccshift  42285  itgperiod  42286  stoweidlem1  42306  stoweidlem11  42316  stoweidlem13  42318  stoweidlem14  42319  stoweidlem17  42322  stoweidlem25  42330  stoweidlem26  42331  stoweidlem42  42347  wallispilem4  42373  wallispilem5  42374  wallispi  42375  wallispi2lem1  42376  wallispi2lem2  42377  wallispi2  42378  stirlinglem1  42379  stirlinglem3  42381  stirlinglem4  42382  stirlinglem5  42383  stirlinglem6  42384  stirlinglem7  42385  stirlinglem8  42386  stirlinglem10  42388  stirlinglem11  42389  stirlinglem12  42390  stirlinglem13  42391  stirlinglem14  42392  stirlinglem15  42393  dirker2re  42397  dirkerdenne0  42398  dirkerper  42401  dirkertrigeqlem1  42403  dirkertrigeqlem2  42404  dirkertrigeqlem3  42405  dirkertrigeq  42406  dirkeritg  42407  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem26  42438  fourierdlem30  42442  fourierdlem39  42451  fourierdlem42  42454  fourierdlem47  42458  fourierdlem48  42459  fourierdlem56  42467  fourierdlem57  42468  fourierdlem58  42469  fourierdlem62  42473  fourierdlem65  42476  fourierdlem66  42477  fourierdlem68  42479  fourierdlem72  42483  fourierdlem73  42484  fourierdlem76  42487  fourierdlem80  42491  fourierdlem83  42494  fourierdlem85  42496  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem95  42506  fourierdlem97  42508  fourierdlem101  42512  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  elaa2lem  42538  etransclem8  42547  etransclem18  42557  etransclem20  42559  etransclem21  42560  etransclem23  42562  etransclem24  42563  etransclem31  42570  etransclem33  42572  etransclem35  42574  etransclem45  42584  etransclem46  42585  etransclem47  42586  etransclem48  42587  hoicvrrex  42858  hoidmvlelem2  42898  smfmullem1  43086  sigarim  43128  sigarac  43129  sigaraf  43130  sigarmf  43131  sigarls  43134  sigardiv  43138  sigarcol  43141  cevathlem1  43144  fmtnorec2lem  43724  fmtnorec3  43730  fmtnorec4  43731  fmtnoprmfac1  43747  fmtnoprmfac2  43749  fmtnofac2lem  43750  sfprmdvdsmersenne  43788  lighneallem3  43792  quad1  43805  requad01  43806  requad2  43808  opeoALTV  43869  perfectALTVlem2  43907  fppr2odd  43916  0nodd  44097  2nodd  44099  2zlidl  44225  2zrngnmlid  44240  altgsumbcALT  44421  fldivmod  44598  nn0sumshdiglemA  44699  nn0sumshdiglemB  44700  nn0sumshdiglem2  44702  nn0mullong  44705  submuladdmuld  44708  affinecomb2  44710  affineid  44711  1subrec1sub  44712  eenglngeehlnmlem1  44744  eenglngeehlnmlem2  44745  rrx2linest  44749  line2x  44761  line2y  44762  itschlc0yqe  44767  itsclc0yqsollem1  44769  itsclc0yqsol  44771  itscnhlc0xyqsol  44772  itschlc0xyqsol1  44773  itschlc0xyqsol  44774  itsclc0xyqsolr  44776  2itscplem1  44785  2itscplem2  44786  2itscplem3  44787  2itscp  44788  itscnhlinecirc02plem1  44789  itscnhlinecirc02plem2  44790  inlinecirc02plem  44793  inlinecirc02p  44794  i2linesd  44900  aacllem  44922  amgmwlem  44923  amgmlemALT  44924