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

Theorem mulcld 9527
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
mulcld  |-  ( ph  ->  ( A  x.  B
)  e.  CC )

Proof of Theorem mulcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 mulcl 9487 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826  (class class class)co 6196   CCcc 9401    x. cmul 9408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9465
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  mul02lem1  9667  addid1  9671  cnegex  9672  kcnktkm1cn  9906  receu  10111  divrec  10140  divcan3  10148  divdivdiv  10162  divsubdiv  10177  cru  10444  lincmb01cmp  11584  iccf1o  11585  flpmodeq  11901  moddiffl  11908  modvalp1  11915  modcyc  11932  modadd1  11934  modmul1  11943  modaddmulmod  11956  mulexpz  12109  expmulz  12115  binom3  12189  bernneq  12194  remullem  12963  cjreim2  12996  absimle  13144  abstri  13165  sqreulem  13194  sqreu  13195  mulcn2  13420  reccn2  13421  o1rlimmul  13443  isummulc2  13579  fsummulc2  13601  fsumparts  13622  binomlem  13643  binom1dif  13647  incexclem  13650  incexc  13651  incexc2  13652  geomulcvg  13687  mertenslem1  13695  mertens  13697  fprodmul  13767  iprodmul  13798  efaddlem  13830  sinadd  13901  cosadd  13902  tanaddlem  13903  tanadd  13904  addsin  13907  sincossq  13913  sin2t  13914  dvds2ln  14016  oddm1even  14049  sadadd2lem2  14102  bezoutlem2  14179  bezoutlem3  14180  bezoutlem4  14181  phiprmpw  14308  pythagtriplem12  14352  pythagtriplem14  14354  pythagtriplem16  14356  pcpremul  14369  pcaddlem  14409  fldivp1  14418  mul4sqlem  14473  4sqlem14  14478  vdwapun  14494  vdwlem2  14502  vdwlem6  14506  zringlpirlem3  18617  znunit  18693  blcvx  21388  icopnfcnv  21527  mbfmulc2re  22140  mbfmulc2  22155  itg1addlem4  22191  itg1addlem5  22192  itg1mulc  22196  mbfmul  22218  itgcl  22275  itgcnlem  22281  iblmulc2  22322  itgmulc2  22325  itgabs  22326  itgsplit  22327  dvmulbr  22427  dvcmul  22432  dvcmulf  22433  dvexp  22441  dvmptcmul  22452  dvexp3  22464  dvsincos  22467  cmvth  22477  dvlipcn  22480  dvfsumabs  22509  dvfsumlem1  22512  ftc1lem4  22525  itgparts  22533  plyf  22680  ply1termlem  22685  plyeq0lem  22692  plypf1  22694  plyaddlem1  22695  plymullem1  22696  coeeulem  22706  coeidlem  22719  coeid3  22722  plyco  22723  coemullem  22732  coemulhi  22736  coemulc  22737  dgrcolem2  22756  plycjlem  22758  plyrecj  22761  dvply1  22765  vieta1lem2  22792  vieta1  22793  elqaalem3  22802  aareccl  22807  aalioulem1  22813  taylfvallem1  22837  tayl0  22842  dvtaylp  22850  taylthlem2  22854  psergf  22892  radcnvlem1  22893  dvradcnv  22901  psercn2  22903  pserdvlem2  22908  pserdv2  22910  abelthlem4  22914  abelthlem5  22915  abelthlem6  22916  abelthlem7  22918  abelthlem9  22920  tanregt0  23011  efgh  23013  efabl  23022  efsubm  23023  cosargd  23080  abslogle  23090  tanarg  23091  advlogexp  23123  logtayllem  23127  logtayl  23128  cxpadd  23147  mulcxp  23153  cxpmul  23156  cxpmul2  23157  cxpmul2z  23159  abscxp  23160  abscxp2  23161  dvcxp2  23204  abscxpbnd  23214  root1eq1  23216  cxpeq  23218  angcan  23252  pythag  23267  ssscongptld  23272  affineequiv  23273  affineequiv2  23274  chordthmlem2  23280  chordthmlem3  23281  chordthmlem4  23282  chordthmlem5  23283  heron  23285  quad2  23286  quad  23287  dcubic1lem  23290  dcubic2  23291  dcubic1  23292  dcubic  23293  mcubic  23294  cubic2  23295  cubic  23296  binom4  23297  dquartlem1  23298  dquartlem2  23299  dquart  23300  quart1cl  23301  quart1lem  23302  quart1  23303  quartlem1  23304  quartlem2  23305  atantayl3  23386  leibpi  23389  birthdaylem2  23399  divsqrtsumo1  23430  cvxcl  23431  jensenlem2  23434  wilthlem2  23460  ftalem1  23463  ftalem2  23464  ftalem4  23466  ftalem5  23467  basellem2  23472  basellem3  23473  basellem8  23478  muinv  23586  fsumdvdsmul  23588  logfacrlim  23616  logexprlim  23617  perfectlem2  23622  bposlem9  23684  lgsquad2lem1  23750  2sqlem3  23758  rplogsumlem1  23786  dchrisumlem2  23792  dchrisumlem3  23793  dchrmusum2  23796  dchrvmasumlem1  23797  dchrvmasum2lem  23798  dchrvmasum2if  23799  dchrvmasumlem3  23801  dchrvmasumiflem1  23803  dchrvmasumiflem2  23804  rpvmasum2  23814  dchrisum0lem1  23818  dchrisum0lem2a  23819  dchrisum0lem2  23820  dchrmusumlem  23824  dchrvmasumlem  23825  rplogsum  23829  mudivsum  23832  mulogsumlem  23833  mulogsum  23834  mulog2sumlem1  23836  mulog2sumlem2  23837  mulog2sumlem3  23838  vmalogdivsum  23841  logsqvma  23844  log2sumbnd  23846  selberglem1  23847  selberglem2  23848  selberglem3  23849  selberg  23850  selberg2lem  23852  selberg2  23853  selberg3lem1  23859  selberg3  23861  selberg4lem1  23862  selberg4  23863  pntrsumo1  23867  selbergr  23870  selberg3r  23871  selberg4r  23872  selberg34r  23873  pntsval2  23878  pntrlog2bndlem1  23879  pntrlog2bndlem2  23880  pntrlog2bndlem3  23881  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  pntrlog2bndlem6  23885  pntrlog2bnd  23886  pntlemb  23899  pntlemf  23907  pntlemo  23909  ostth2lem2  23936  ostth2lem3  23937  ttgcontlem1  24309  brbtwn2  24329  colinearalg  24334  ax5seglem2  24353  ax5seglem9  24361  axeuclidlem  24386  axcontlem2  24389  axcontlem4  24391  axcontlem7  24394  axcontlem8  24395  ex-ind-dvds  25291  ipval2  25734  dipcl  25742  riesz3i  27097  mul2lt0rlt0  27715  bhmafibid1  27785  bhmafibid2  27786  2sqmod  27789  cnre2csqima  28047  rmulccn  28064  indsum  28171  dya2icoseg  28404  oddpwdc  28476  eulerpartlems  28482  eulerpartlemsv3  28483  eulerpartlemgs2  28502  signsplypnf  28690  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem4  28763  lgamgulmlem5  28764  lgamgulmlem6  28765  lgamgulm2  28767  lgamcvg2  28786  gamcvg  28787  gamcvg2lem  28790  subfacval2  28820  subfaclim  28821  rescon  28880  subdivcomb1  29271  subdivcomb2  29272  iprodgam  29291  binomfallfaclem1  29327  binomfallfaclem2  29328  binomrisefac  29330  bpolycl  29967  bpolysum  29968  bpolydiflem  29969  bpoly4  29974  iblmulc2nc  30246  itgmulc2nc  30249  itgabsnc  30250  ftc1cnnclem  30254  ftc1anclem3  30258  dvasin  30269  areacirclem1  30273  areacirclem4  30276  areacirc  30278  cntotbnd  30458  pellexlem1  30930  pellexlem2  30931  pellexlem6  30935  pell1234qrne0  30954  pell1234qrreccl  30955  pell1234qrmulcl  30956  pell1234qrdich  30962  pell14qrdich  30970  pell1qrge1  30971  pell1qrgaplem  30974  qirropth  31009  rmxyneg  31021  rmxyadd  31022  rmxm1  31035  rmym1  31036  rmxluc  31037  rmyluc  31038  rmxdbl  31040  rmydbl  31041  jm2.18  31096  jm2.19lem1  31097  jm2.19lem2  31098  jm2.19lem4  31100  jm2.19  31101  jm2.22  31103  jm2.23  31104  jm2.25  31107  jm2.27c  31115  jm3.1lem2  31126  flcidc  31291  itgpowd  31350  areaquad  31352  radcnvrat  31363  lcmgcdlem  31380  expgrowth  31408  binomcxplemwb  31421  binomcxplemnn0  31422  binomcxplemfrat  31424  binomcxplemdvbinom  31426  binomcxplemnotnn0  31429  mul13d  31628  fperiodmullem  31669  fperiodmul  31670  divcan8d  31681  dmmcand  31683  mulc1cncfg  31749  fprodn0f  31760  mccllem  31771  clim1fr1  31773  mullimc  31788  mullimcf  31795  sumnnodd  31802  reclimc  31825  sinmulcos  31831  coskpi2  31832  cosknegpi  31835  dvsinexp  31871  dvmptdiv  31880  dvasinbx  31883  dvdivf  31885  dvdivbd  31886  dvdivcncf  31890  dvbdfbdioolem2  31892  dvxpaek  31903  dvnxpaek  31905  dvnmul  31906  dvmptfprodlem  31907  dvnprodlem2  31910  itgsinexplem1  31918  itgsinexp  31919  itgcoscmulx  31934  itgsincmulx  31939  itgiccshift  31945  itgperiod  31946  stoweidlem1  31949  stoweidlem11  31959  stoweidlem13  31961  stoweidlem14  31962  stoweidlem17  31965  stoweidlem25  31973  stoweidlem26  31974  stoweidlem42  31990  wallispilem4  32016  wallispilem5  32017  wallispi  32018  wallispi2lem1  32019  wallispi2lem2  32020  wallispi2  32021  stirlinglem1  32022  stirlinglem3  32024  stirlinglem4  32025  stirlinglem5  32026  stirlinglem6  32027  stirlinglem7  32028  stirlinglem8  32029  stirlinglem10  32031  stirlinglem11  32032  stirlinglem12  32033  stirlinglem13  32034  stirlinglem14  32035  stirlinglem15  32036  dirker2re  32040  dirkerdenne0  32041  dirkerper  32044  dirkertrigeqlem1  32046  dirkertrigeqlem2  32047  dirkertrigeqlem3  32048  dirkertrigeq  32049  dirkeritg  32050  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem26  32081  fourierdlem30  32085  fourierdlem39  32094  fourierdlem42  32097  fourierdlem47  32102  fourierdlem48  32103  fourierdlem56  32111  fourierdlem57  32112  fourierdlem58  32113  fourierdlem62  32117  fourierdlem65  32120  fourierdlem66  32121  fourierdlem68  32123  fourierdlem72  32127  fourierdlem73  32128  fourierdlem76  32131  fourierdlem80  32135  fourierdlem83  32138  fourierdlem85  32140  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem95  32150  fourierdlem97  32152  fourierdlem101  32156  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  sqwvfoura  32177  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  elaa2lem  32182  etransclem8  32191  etransclem18  32201  etransclem20  32203  etransclem21  32204  etransclem23  32206  etransclem24  32207  etransclem31  32214  etransclem33  32216  etransclem35  32218  etransclem45  32228  etransclem46  32229  etransclem47  32230  etransclem48  32231  sigarim  32234  sigarac  32235  sigaraf  32236  sigarmf  32237  sigarls  32240  sigardiv  32244  sigarcol  32247  cevathlem1  32250  opeoALTV  32526  perfectALTVlem2  32544  0nodd  32816  2nodd  32818  2zlidl  32940  2zrngnmlid  32955  altgsumbcALT  33142  fldivmod  33331  nn0sumshdiglemA  33440  nn0sumshdiglemB  33441  nn0sumshdiglem2  33443  nn0mullong  33446  i2linesd  33528  aacllem  33550  sineq0ALT  34084  bj-subcom  35017  bj-lineq  35021  bj-bary1lem  35023  bj-bary1lem1  35024  bj-bary1  35025  inductionexd  38496  imo72b2lem0  38511  int-leftdistd  38529
  Copyright terms: Public domain W3C validator