MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulcld Structured version   Visualization version   GIF version

Theorem mulcld 10650
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
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 mulcl 10610 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  (class class class)co 7140  cc 10524   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 10588
This theorem depends on definitions:  df-bi 210  df-an 400
This theorem is referenced by:  mul02lem1  10805  addid1  10809  cnegex  10810  kcnktkm1cn  11060  subaddmulsub  11092  mulsubaddmulsub  11093  receu  11274  divrec  11303  divcan3  11313  muldivdir  11322  subdivcomb1  11324  subdivcomb2  11325  divdivdiv  11330  divsubdiv  11345  lineq  11466  cru  11617  mul2lt0rlt0  12479  lincmb01cmp  12873  iccf1o  12874  flpmodeq  13237  moddiffl  13245  modvalp1  13253  modcyc  13269  modadd1  13271  modmuladdnn0  13278  modmul1  13287  modaddmulmod  13301  mulexpz  13465  expmulz  13471  binom3  13581  bernneq  13586  mulsubdivbinom2  13618  muldivbinom2  13619  remullem  14478  cjreim2  14511  absimle  14660  abstri  14681  sqreulem  14710  sqreu  14711  bhmafibid1cn  14814  bhmafibid2cn  14815  bhmafibid1  14816  bhmafibid2  14817  mulcn2  14943  reccn2  14944  o1rlimmul  14966  isummulc2  15108  fsummulc2  15130  fsumparts  15152  binomlem  15175  binom1dif  15179  incexclem  15182  incexc  15183  incexc2  15184  pwdif  15214  geomulcvg  15223  mertenslem1  15231  mertens  15233  fprodmul  15305  fprodn0f  15336  iprodmul  15348  binomfallfaclem1  15384  binomfallfaclem2  15385  binomrisefac  15387  bpolycl  15397  bpolysum  15398  bpolydiflem  15399  bpoly4  15404  efaddlem  15437  sinadd  15508  cosadd  15509  tanaddlem  15510  tanadd  15511  addsin  15514  sincossq  15520  sin2t  15521  dvds2ln  15633  oddm1even  15683  pwp1fsum  15731  flodddiv4  15753  sadadd2lem2  15788  bezoutlem2  15877  bezoutlem3  15878  bezoutlem4  15879  lcmgcdlem  15939  phiprmpw  16102  pythagtriplem12  16152  pythagtriplem14  16154  pythagtriplem16  16156  pcpremul  16169  pcaddlem  16213  fldivp1  16222  mul4sqlem  16278  4sqlem14  16283  vdwapun  16299  vdwlem2  16307  vdwlem6  16311  ablsimpgfindlem1  19220  zringlpirlem3  20177  znunit  20253  blcvx  23401  icopnfcnv  23545  cphipipcj  23803  cphipval2  23843  4cphipval2  23844  cphipval  23845  mbfmulc2re  24250  mbfmulc2  24265  itg1addlem4  24301  itg1addlem5  24302  itg1mulc  24306  mbfmul  24328  itgcl  24385  itgcnlem  24391  iblmulc2  24432  itgmulc2  24435  itgabs  24436  itgsplit  24437  dvmulbr  24540  dvcmul  24545  dvcmulf  24546  dvexp  24554  dvmptcmul  24565  dvmptdiv  24575  dvexp3  24579  dvsincos  24582  cmvth  24592  dvlipcn  24595  dvfsumabs  24624  dvfsumlem1  24627  ftc1lem4  24640  itgparts  24648  itgpowd  24651  plyf  24793  ply1termlem  24798  plyeq0lem  24805  plypf1  24807  plyaddlem1  24808  plymullem1  24809  coeeulem  24819  coeidlem  24832  coeid3  24835  plyco  24836  coemullem  24845  coemulhi  24849  coemulc  24850  dgrcolem2  24869  plycjlem  24871  plyrecj  24874  dvply1  24878  vieta1lem2  24905  vieta1  24906  elqaalem3  24915  aareccl  24920  aalioulem1  24926  taylfvallem1  24950  tayl0  24955  dvtaylp  24963  taylthlem2  24967  psergf  25005  radcnvlem1  25006  dvradcnv  25014  psercn2  25016  pserdvlem2  25021  pserdv2  25023  abelthlem4  25027  abelthlem5  25028  abelthlem6  25029  abelthlem7  25031  abelthlem9  25033  tanregt0  25129  efgh  25131  efabl  25140  efsubm  25141  cosargd  25197  abslogle  25207  tanarg  25208  advlogexp  25244  logtayllem  25248  logtayl  25249  cxpadd  25268  mulcxp  25274  cxpmul  25277  cxpmul2  25278  cxpmul2z  25280  abscxp  25281  abscxp2  25282  dvcxp2  25328  abscxpbnd  25340  root1eq1  25342  cxpeq  25344  angcan  25386  pythag  25401  ssscongptld  25406  affineequiv  25407  affineequiv2  25408  affineequiv3  25409  affineequiv4  25410  chordthmlem2  25417  chordthmlem3  25418  chordthmlem4  25419  chordthmlem5  25420  heron  25422  quad2  25423  quad  25424  dcubic1lem  25427  dcubic2  25428  dcubic1  25429  dcubic  25430  mcubic  25431  cubic2  25432  cubic  25433  binom4  25434  dquartlem1  25435  dquartlem2  25436  dquart  25437  quart1cl  25438  quart1lem  25439  quart1  25440  quartlem1  25441  quartlem2  25442  atantayl3  25523  leibpi  25526  birthdaylem2  25536  divsqrtsumo1  25567  cvxcl  25568  jensenlem2  25571  lgamgulmlem2  25613  lgamgulmlem3  25614  lgamgulmlem4  25615  lgamgulmlem5  25616  lgamgulmlem6  25617  lgamgulm2  25619  lgamcvg2  25638  gamcvg  25639  gamcvg2lem  25642  wilthlem2  25652  ftalem1  25656  ftalem2  25657  ftalem4  25659  ftalem5  25660  basellem2  25665  basellem3  25666  basellem8  25671  muinv  25776  fsumdvdsmul  25778  logfacrlim  25806  logexprlim  25807  perfectlem2  25812  bposlem9  25874  gausslemma2dlem4  25951  lgsquad2lem1  25966  2lgslem3b  25979  2lgslem3c  25980  2lgslem3d  25981  2sqlem3  26002  2sqmod  26018  rplogsumlem1  26066  dchrisumlem2  26072  dchrisumlem3  26073  dchrmusum2  26076  dchrvmasumlem1  26077  dchrvmasum2lem  26078  dchrvmasum2if  26079  dchrvmasumlem3  26081  dchrvmasumiflem1  26083  dchrvmasumiflem2  26084  rpvmasum2  26094  dchrisum0lem1  26098  dchrisum0lem2a  26099  dchrisum0lem2  26100  dchrmusumlem  26104  dchrvmasumlem  26105  rplogsum  26109  mudivsum  26112  mulogsumlem  26113  mulogsum  26114  mulog2sumlem1  26116  mulog2sumlem2  26117  mulog2sumlem3  26118  vmalogdivsum  26121  logsqvma  26124  log2sumbnd  26126  selberglem1  26127  selberglem2  26128  selberglem3  26129  selberg  26130  selberg2lem  26132  selberg2  26133  selberg3lem1  26139  selberg3  26141  selberg4lem1  26142  selberg4  26143  pntrsumo1  26147  selbergr  26150  selberg3r  26151  selberg4r  26152  selberg34r  26153  pntsval2  26158  pntrlog2bndlem1  26159  pntrlog2bndlem2  26160  pntrlog2bndlem3  26161  pntrlog2bndlem4  26162  pntrlog2bndlem5  26163  pntrlog2bndlem6  26165  pntrlog2bnd  26166  pntlemb  26179  pntlemf  26187  pntlemo  26189  ostth2lem2  26216  ostth2lem3  26217  ttgcontlem1  26677  brbtwn2  26697  colinearalg  26702  ax5seglem2  26721  ax5seglem9  26729  axeuclidlem  26754  axcontlem2  26757  axcontlem4  26759  axcontlem7  26762  axcontlem8  26763  finsumvtxdg2ssteplem4  27336  ex-ind-dvds  28244  ipval2  28488  dipcl  28493  riesz3i  29843  dpfrac1  30578  wrdt2ind  30637  ccfldsrarelvec  31113  ccfldextdgrr  31114  cnre2csqima  31228  rmulccn  31245  indsum  31354  indsumin  31355  dya2icoseg  31609  oddpwdc  31686  eulerpartlems  31692  eulerpartlemsv3  31693  eulerpartlemgs2  31712  signsplypnf  31894  itgexpif  31951  breprexplemc  31977  breprexp  31978  vtscl  31983  vtsprod  31984  circlemeth  31985  logdivsqrle  31995  hgt750lemf  31998  hgt750leme  32003  subfacval2  32508  subfaclim  32509  resconn  32567  iprodgam  33048  fwddifnp1  33700  knoppndvlem2  33926  knoppndvlem7  33931  knoppndvlem9  33933  knoppndvlem11  33935  knoppndvlem14  33938  knoppndvlem16  33940  knoppndvlem17  33941  bj-subcom  34683  bj-bary1lem  34685  bj-bary1lem1  34686  bj-bary1  34687  iblmulc2nc  35084  itgmulc2nc  35087  itgabsnc  35088  ftc1cnnclem  35090  ftc1anclem3  35094  dvasin  35103  areacirclem1  35107  areacirclem4  35110  areacirc  35112  cntotbnd  35196  3factsumint1  39274  3factsumint3  39276  3factsumint4  39277  lcmineqlem2  39283  lcmineqlem6  39287  lcmineqlem8  39289  lcmineqlem10  39291  lcmineqlem11  39292  lcmineqlem12  39293  lcmineqlem16  39297  lcmineqlem18  39299  lcmineqlem23  39304  2np3bcnp1  39311  2ap1caineq  39312  sn-addid2  39490  sn-it0e0  39500  sn-negex12  39501  sn-mul01  39509  sn-mulid2  39519  fltnltalem  39552  fltnlta  39553  cu3addd  39555  3cubeslem2  39560  3cubeslem3l  39561  3cubeslem3r  39562  3cubeslem4  39564  pellexlem1  39704  pellexlem2  39705  pellexlem6  39709  pell1234qrne0  39728  pell1234qrreccl  39729  pell1234qrmulcl  39730  pell1234qrdich  39736  pell14qrdich  39744  pell1qrge1  39745  pell1qrgaplem  39748  rmspecsqrtnq  39781  qirropth  39783  rmxyneg  39795  rmxyadd  39796  rmxm1  39809  rmym1  39810  rmxluc  39811  rmyluc  39812  rmxdbl  39814  rmydbl  39815  jm2.18  39863  jm2.19lem1  39864  jm2.19lem2  39865  jm2.19lem4  39867  jm2.19  39868  jm2.22  39870  jm2.23  39871  jm2.25  39874  jm2.27c  39882  jm3.1lem2  39893  flcidc  40052  areaquad  40100  sqrtcval  40275  inductionexd  40795  imo72b2lem0  40806  int-leftdistd  40822  radcnvrat  40956  expgrowth  40977  binomcxplemwb  40990  binomcxplemnn0  40991  binomcxplemfrat  40993  binomcxplemdvbinom  40995  binomcxplemnotnn0  40998  sineq0ALT  41581  mul13d  41853  fperiodmullem  41878  fperiodmul  41879  divcan8d  41887  dmmcand  41888  ltdiv23neg  41973  mulc1cncfg  42174  mccllem  42182  clim1fr1  42186  mullimc  42201  mullimcf  42208  sumnnodd  42215  reclimc  42238  sinmulcos  42450  coskpi2  42451  cosknegpi  42454  dvsinexp  42496  dvasinbx  42505  dvdivf  42507  dvdivbd  42508  dvdivcncf  42512  dvbdfbdioolem2  42514  dvxpaek  42525  dvnxpaek  42527  dvnmul  42528  dvmptfprodlem  42529  dvnprodlem2  42532  itgsinexplem1  42539  itgsinexp  42540  itgcoscmulx  42554  itgsincmulx  42559  itgiccshift  42565  itgperiod  42566  stoweidlem1  42586  stoweidlem11  42596  stoweidlem13  42598  stoweidlem14  42599  stoweidlem17  42602  stoweidlem25  42610  stoweidlem26  42611  stoweidlem42  42627  wallispilem4  42653  wallispilem5  42654  wallispi  42655  wallispi2lem1  42656  wallispi2lem2  42657  wallispi2  42658  stirlinglem1  42659  stirlinglem3  42661  stirlinglem4  42662  stirlinglem5  42663  stirlinglem6  42664  stirlinglem7  42665  stirlinglem8  42666  stirlinglem10  42668  stirlinglem11  42669  stirlinglem12  42670  stirlinglem13  42671  stirlinglem14  42672  stirlinglem15  42673  dirker2re  42677  dirkerdenne0  42678  dirkerper  42681  dirkertrigeqlem1  42683  dirkertrigeqlem2  42684  dirkertrigeqlem3  42685  dirkertrigeq  42686  dirkeritg  42687  dirkercncflem2  42689  dirkercncflem4  42691  fourierdlem26  42718  fourierdlem30  42722  fourierdlem39  42731  fourierdlem42  42734  fourierdlem47  42738  fourierdlem48  42739  fourierdlem56  42747  fourierdlem57  42748  fourierdlem58  42749  fourierdlem62  42753  fourierdlem65  42756  fourierdlem66  42757  fourierdlem68  42759  fourierdlem72  42763  fourierdlem73  42764  fourierdlem76  42767  fourierdlem80  42771  fourierdlem83  42774  fourierdlem85  42776  fourierdlem89  42780  fourierdlem90  42781  fourierdlem91  42782  fourierdlem95  42786  fourierdlem97  42788  fourierdlem101  42792  fourierdlem103  42794  fourierdlem104  42795  fourierdlem111  42802  sqwvfoura  42813  sqwvfourb  42814  fourierswlem  42815  fouriersw  42816  elaa2lem  42818  etransclem8  42827  etransclem18  42837  etransclem20  42839  etransclem21  42840  etransclem23  42842  etransclem24  42843  etransclem31  42850  etransclem33  42852  etransclem35  42854  etransclem45  42864  etransclem46  42865  etransclem47  42866  etransclem48  42867  hoicvrrex  43138  hoidmvlelem2  43178  smfmullem1  43366  sigarim  43408  sigarac  43409  sigaraf  43410  sigarmf  43411  sigarls  43414  sigardiv  43418  sigarcol  43421  cevathlem1  43424  fmtnorec2lem  44002  fmtnorec3  44008  fmtnorec4  44009  fmtnoprmfac1  44025  fmtnoprmfac2  44027  fmtnofac2lem  44028  sfprmdvdsmersenne  44064  lighneallem3  44068  quad1  44081  requad01  44082  requad2  44084  opeoALTV  44145  perfectALTVlem2  44183  fppr2odd  44192  0nodd  44373  2nodd  44375  2zlidl  44501  2zrngnmlid  44516  altgsumbcALT  44698  fldivmod  44875  nn0sumshdiglemA  44976  nn0sumshdiglemB  44977  nn0sumshdiglem2  44979  nn0mullong  44982  itcovalt2lem2lem2  45031  ackval2  45039  submuladdmuld  45058  affinecomb2  45060  affineid  45061  1subrec1sub  45062  eenglngeehlnmlem1  45094  eenglngeehlnmlem2  45095  rrx2linest  45099  line2x  45111  line2y  45112  itschlc0yqe  45117  itsclc0yqsollem1  45119  itsclc0yqsol  45121  itscnhlc0xyqsol  45122  itschlc0xyqsol1  45123  itschlc0xyqsol  45124  itsclc0xyqsolr  45126  2itscplem1  45135  2itscplem2  45136  2itscplem3  45137  2itscp  45138  itscnhlinecirc02plem1  45139  itscnhlinecirc02plem2  45140  inlinecirc02plem  45143  inlinecirc02p  45144  i2linesd  45250  aacllem  45272  amgmwlem  45273  amgmlemALT  45274
  Copyright terms: Public domain W3C validator