Theorem mulcld 11231

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   · cmul 11112

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

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

This theorem is referenced by:  mul02lem1  11387  addrid  11391  cnegex  11392  kcnktkm1cn  11642  subaddmulsub  11674  mulsubaddmulsub  11675  receu  11856  divrec  11885  divcan3  11895  muldivdir  11904  subdivcomb1  11906  subdivcomb2  11907  divdivdiv  11912  divsubdiv  11927  lineq  12048  cru  12201  mul2lt0rlt0  13073  lincmb01cmp  13469  iccf1o  13470  flpmodeq  13836  moddiffl  13844  modvalp1  13852  modcyc  13868  modadd1  13870  modmuladdnn0  13877  modmul1  13886  modaddmulmod  13900  mulexpz  14065  expmulz  14071  binom3  14184  bernneq  14189  mulsubdivbinom2  14219  muldivbinom2  14220  remullem  15072  cjreim2  15105  absimle  15253  abstri  15274  sqreulem  15303  sqreu  15304  bhmafibid1cn  15407  bhmafibid2cn  15408  bhmafibid1  15409  bhmafibid2  15410  mulcn2  15537  reccn2  15538  o1rlimmul  15560  rlimmul  15587  isummulc2  15705  fsummulc2  15727  fsumparts  15749  binomlem  15772  binom1dif  15776  incexclem  15779  incexc  15780  incexc2  15781  pwdif  15811  geomulcvg  15819  mertenslem1  15827  mertens  15829  fprodmul  15901  fprodn0f  15932  iprodmul  15944  binomfallfaclem1  15980  binomfallfaclem2  15981  binomrisefac  15983  bpolycl  15993  bpolysum  15994  bpolydiflem  15995  bpoly4  16000  efaddlem  16033  sinadd  16104  cosadd  16105  tanaddlem  16106  tanadd  16107  addsin  16110  sincossq  16116  sin2t  16117  dvds2ln  16229  oddm1even  16283  pwp1fsum  16331  flodddiv4  16353  sadadd2lem2  16388  bezoutlem2  16479  bezoutlem3  16480  bezoutlem4  16481  lcmgcdlem  16540  phiprmpw  16706  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem16  16760  pcpremul  16773  pcaddlem  16818  fldivp1  16827  mul4sqlem  16883  4sqlem14  16888  vdwapun  16904  vdwlem2  16912  vdwlem6  16916  ablsimpgfindlem1  19972  zringlpirlem3  21026  znunit  21111  blcvx  24306  icopnfcnv  24450  cphipipcj  24709  cphipval2  24750  4cphipval2  24751  cphipval  24752  mbfmulc2re  25157  mbfmulc2  25172  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  itg1mulc  25214  mbfmul  25236  itgcl  25293  itgcnlem  25299  iblmulc2  25340  itgmulc2  25343  itgabs  25344  itgsplit  25345  dvmulbr  25448  dvcmul  25453  dvcmulf  25454  dvexp  25462  dvmptcmul  25473  dvmptdiv  25483  dvexp3  25487  dvsincos  25490  cmvth  25500  dvlipcn  25503  dvfsumabs  25532  dvfsumlem1  25535  ftc1lem4  25548  itgparts  25556  itgpowd  25559  plyf  25704  ply1termlem  25709  plyeq0lem  25716  plypf1  25718  plyaddlem1  25719  plymullem1  25720  coeeulem  25730  coeidlem  25743  coeid3  25746  plyco  25747  coemullem  25756  coemulhi  25760  coemulc  25761  dgrcolem2  25780  plycjlem  25782  plyrecj  25785  dvply1  25789  vieta1lem2  25816  vieta1  25817  elqaalem3  25826  aareccl  25831  aalioulem1  25837  taylfvallem1  25861  tayl0  25866  dvtaylp  25874  taylthlem2  25878  psergf  25916  radcnvlem1  25917  dvradcnv  25925  psercn2  25927  pserdvlem2  25932  pserdv2  25934  abelthlem4  25938  abelthlem5  25939  abelthlem6  25940  abelthlem7  25942  abelthlem9  25944  tanregt0  26040  efgh  26042  efabl  26051  efsubm  26052  cosargd  26108  abslogle  26118  tanarg  26119  advlogexp  26155  logtayllem  26159  logtayl  26160  cxpadd  26179  mulcxp  26185  cxpmul  26188  cxpmul2  26189  cxpmul2z  26191  abscxp  26192  abscxp2  26193  dvcxp2  26239  abscxpbnd  26251  root1eq1  26253  cxpeq  26255  angcan  26297  pythag  26312  ssscongptld  26317  affineequiv  26318  affineequiv2  26319  affineequiv3  26320  affineequiv4  26321  chordthmlem2  26328  chordthmlem3  26329  chordthmlem4  26330  chordthmlem5  26331  heron  26333  quad2  26334  quad  26335  dcubic1lem  26338  dcubic2  26339  dcubic1  26340  dcubic  26341  mcubic  26342  cubic2  26343  cubic  26344  binom4  26345  dquartlem1  26346  dquartlem2  26347  dquart  26348  quart1cl  26349  quart1lem  26350  quart1  26351  quartlem1  26352  quartlem2  26353  atantayl3  26434  leibpi  26437  birthdaylem2  26447  divsqrtsumo1  26478  cvxcl  26479  jensenlem2  26482  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulmlem6  26528  lgamgulm2  26530  lgamcvg2  26549  gamcvg  26550  gamcvg2lem  26553  wilthlem2  26563  ftalem1  26567  ftalem2  26568  ftalem4  26570  ftalem5  26571  basellem2  26576  basellem3  26577  basellem8  26582  muinv  26687  fsumdvdsmul  26689  logfacrlim  26717  logexprlim  26718  perfectlem2  26723  bposlem9  26785  gausslemma2dlem4  26862  lgsquad2lem1  26877  2lgslem3b  26890  2lgslem3c  26891  2lgslem3d  26892  2sqlem3  26913  2sqmod  26929  rplogsumlem1  26977  dchrisumlem2  26983  dchrisumlem3  26984  dchrmusum2  26987  dchrvmasumlem1  26988  dchrvmasum2lem  26989  dchrvmasum2if  26990  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  rpvmasum2  27005  dchrisum0lem1  27009  dchrisum0lem2a  27010  dchrisum0lem2  27011  dchrmusumlem  27015  dchrvmasumlem  27016  rplogsum  27020  mudivsum  27023  mulogsumlem  27024  mulogsum  27025  mulog2sumlem1  27027  mulog2sumlem2  27028  mulog2sumlem3  27029  vmalogdivsum  27032  logsqvma  27035  log2sumbnd  27037  selberglem1  27038  selberglem2  27039  selberglem3  27040  selberg  27041  selberg2lem  27043  selberg2  27044  selberg3lem1  27050  selberg3  27052  selberg4lem1  27053  selberg4  27054  pntrsumo1  27058  selbergr  27061  selberg3r  27062  selberg4r  27063  selberg34r  27064  pntsval2  27069  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntlemb  27090  pntlemf  27098  pntlemo  27100  ostth2lem2  27127  ostth2lem3  27128  ttgcontlem1  28132  brbtwn2  28153  colinearalg  28158  ax5seglem2  28177  ax5seglem9  28185  axeuclidlem  28210  axcontlem2  28213  axcontlem4  28215  axcontlem7  28218  axcontlem8  28219  finsumvtxdg2ssteplem4  28795  ex-ind-dvds  29704  ipval2  29948  dipcl  29953  riesz3i  31303  dpfrac1  32046  wrdt2ind  32105  ccfldsrarelvec  32734  ccfldextdgrr  32735  cnre2csqima  32880  rmulccn  32897  indsum  33008  indsumin  33009  dya2icoseg  33265  oddpwdc  33342  eulerpartlems  33348  eulerpartlemsv3  33349  eulerpartlemgs2  33368  signsplypnf  33550  itgexpif  33607  breprexplemc  33633  breprexp  33634  vtscl  33639  vtsprod  33640  circlemeth  33641  logdivsqrle  33651  hgt750lemf  33654  hgt750leme  33659  subfacval2  34167  subfaclim  34168  resconn  34226  iprodgam  34701  fwddifnp1  35126  mpomulcn  35151  gg-dvmulbr  35164  gg-psercn2  35167  gg-rmulccn  35168  gg-cmvth  35170  knoppndvlem2  35378  knoppndvlem7  35383  knoppndvlem9  35385  knoppndvlem11  35387  knoppndvlem14  35390  knoppndvlem16  35392  knoppndvlem17  35393  bj-subcom  36178  bj-bary1lem  36180  bj-bary1lem1  36181  bj-bary1  36182  iblmulc2nc  36542  itgmulc2nc  36545  itgabsnc  36546  ftc1cnnclem  36548  ftc1anclem3  36552  dvasin  36561  areacirclem1  36565  areacirclem4  36568  areacirc  36570  cntotbnd  36653  3factsumint1  40875  3factsumint3  40877  3factsumint4  40878  lcmineqlem2  40884  lcmineqlem6  40888  lcmineqlem8  40890  lcmineqlem10  40892  lcmineqlem11  40893  lcmineqlem12  40894  lcmineqlem16  40898  lcmineqlem18  40900  lcmineqlem23  40905  3lexlogpow5ineq5  40914  aks4d1p1p1  40917  dvrelogpow2b  40922  aks4d1p1p6  40927  aks4d1p1p7  40928  aks4d1p1p5  40929  2np3bcnp1  40949  2ap1caineq  40950  oddnumth  41205  nicomachus  41206  sumcubes  41207  sn-addlid  41274  sn-it0e0  41285  sn-negex12  41286  sn-mul01  41295  sn-mullid  41305  sn-0tie0  41309  sn-mul02  41310  cnreeu  41338  fltnltalem  41401  fltnlta  41402  cu3addd  41404  3cubeslem2  41409  3cubeslem3l  41410  3cubeslem3r  41411  3cubeslem4  41413  pellexlem1  41553  pellexlem2  41554  pellexlem6  41558  pell1234qrne0  41577  pell1234qrreccl  41578  pell1234qrmulcl  41579  pell1234qrdich  41585  pell14qrdich  41593  pell1qrge1  41594  pell1qrgaplem  41597  rmspecsqrtnq  41630  qirropth  41632  rmxyneg  41645  rmxyadd  41646  rmxm1  41659  rmym1  41660  rmxluc  41661  rmyluc  41662  rmxdbl  41664  rmydbl  41665  jm2.18  41713  jm2.19lem1  41714  jm2.19lem2  41715  jm2.19lem4  41717  jm2.19  41718  jm2.22  41720  jm2.23  41721  jm2.25  41724  jm2.27c  41732  jm3.1lem2  41743  flcidc  41902  areaquad  41951  sqrtcval  42378  inductionexd  42892  imo72b2lem0  42903  int-leftdistd  42917  radcnvrat  43059  expgrowth  43080  binomcxplemwb  43093  binomcxplemnn0  43094  binomcxplemfrat  43096  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  sineq0ALT  43684  mul13d  43976  fperiodmullem  44000  fperiodmul  44001  divcan8d  44009  dmmcand  44010  ltdiv23neg  44091  mulc1cncfg  44292  mccllem  44300  clim1fr1  44304  mullimc  44319  mullimcf  44326  sumnnodd  44333  reclimc  44356  sinmulcos  44568  coskpi2  44569  cosknegpi  44572  dvsinexp  44614  dvasinbx  44623  dvdivf  44625  dvdivbd  44626  dvdivcncf  44630  dvbdfbdioolem2  44632  dvxpaek  44643  dvnxpaek  44645  dvnmul  44646  dvmptfprodlem  44647  dvnprodlem2  44650  itgsinexplem1  44657  itgsinexp  44658  itgcoscmulx  44672  itgsincmulx  44677  itgiccshift  44683  itgperiod  44684  stoweidlem1  44704  stoweidlem11  44714  stoweidlem13  44716  stoweidlem14  44717  stoweidlem17  44720  stoweidlem25  44728  stoweidlem26  44729  stoweidlem42  44745  wallispilem4  44771  wallispilem5  44772  wallispi  44773  wallispi2lem1  44774  wallispi2lem2  44775  wallispi2  44776  stirlinglem1  44777  stirlinglem3  44779  stirlinglem4  44780  stirlinglem5  44781  stirlinglem6  44782  stirlinglem7  44783  stirlinglem8  44784  stirlinglem10  44786  stirlinglem11  44787  stirlinglem12  44788  stirlinglem13  44789  stirlinglem14  44790  stirlinglem15  44791  dirker2re  44795  dirkerdenne0  44796  dirkerper  44799  dirkertrigeqlem1  44801  dirkertrigeqlem2  44802  dirkertrigeqlem3  44803  dirkertrigeq  44804  dirkeritg  44805  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem26  44836  fourierdlem30  44840  fourierdlem39  44849  fourierdlem42  44852  fourierdlem47  44856  fourierdlem48  44857  fourierdlem56  44865  fourierdlem57  44866  fourierdlem58  44867  fourierdlem62  44871  fourierdlem65  44874  fourierdlem66  44875  fourierdlem68  44877  fourierdlem72  44881  fourierdlem73  44882  fourierdlem76  44885  fourierdlem80  44889  fourierdlem83  44892  fourierdlem85  44894  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem95  44904  fourierdlem97  44906  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  sqwvfoura  44931  sqwvfourb  44932  fourierswlem  44933  fouriersw  44934  elaa2lem  44936  etransclem8  44945  etransclem18  44955  etransclem20  44957  etransclem21  44958  etransclem23  44960  etransclem24  44961  etransclem31  44968  etransclem33  44970  etransclem35  44972  etransclem45  44982  etransclem46  44983  etransclem47  44984  etransclem48  44985  hoicvrrex  45259  hoidmvlelem2  45299  smfmullem1  45494  sigarim  45554  sigarac  45555  sigaraf  45556  sigarmf  45557  sigarls  45560  sigardiv  45564  sigarcol  45567  cevathlem1  45570  fmtnorec2lem  46197  fmtnorec3  46203  fmtnorec4  46204  fmtnoprmfac1  46220  fmtnoprmfac2  46222  fmtnofac2lem  46223  sfprmdvdsmersenne  46258  lighneallem3  46262  quad1  46275  requad01  46276  requad2  46278  opeoALTV  46339  perfectALTVlem2  46377  fppr2odd  46386  0nodd  46567  2nodd  46569  2zlidl  46786  2zrngnmlid  46801  altgsumbcALT  46983  fldivmod  47158  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  nn0sumshdiglem2  47262  nn0mullong  47265  itcovalt2lem2lem2  47314  ackval2  47322  submuladdmuld  47341  affinecomb2  47343  affineid  47344  1subrec1sub  47345  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378  rrx2linest  47382  line2x  47394  line2y  47395  itschlc0yqe  47400  itsclc0yqsollem1  47402  itsclc0yqsol  47404  itscnhlc0xyqsol  47405  itschlc0xyqsol1  47406  itschlc0xyqsol  47407  itsclc0xyqsolr  47409  2itscplem1  47418  2itscplem2  47419  2itscplem3  47420  2itscp  47421  itscnhlinecirc02plem1  47422  itscnhlinecirc02plem2  47423  inlinecirc02plem  47426  inlinecirc02p  47427  i2linesd  47780  aacllem  47802  amgmwlem  47803  amgmlemALT  47804