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

Theorem mulcld 9398
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 9358 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756  (class class class)co 6086   CCcc 9272    x. cmul 9279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9336
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem1  9537  addid1  9541  cnegex  9542  receu  9973  divrec  10002  divcan3  10010  divdivdiv  10024  divsubdiv  10039  cru  10306  lincmb01cmp  11420  iccf1o  11421  flpmodeq  11705  moddiffl  11711  modvalp1  11718  modcyc  11735  modadd1  11737  modmul1  11744  modaddmulmod  11757  mulexpz  11896  expmulz  11902  binom3  11977  bernneq  11982  remullem  12609  cjreim2  12642  absimle  12790  abstri  12810  sqreulem  12839  sqreu  12840  mulcn2  13065  reccn2  13066  o1rlimmul  13088  isummulc2  13221  fsummulc2  13243  fsumparts  13261  binomlem  13284  binom1dif  13288  incexclem  13291  incexc  13292  incexc2  13293  geomulcvg  13328  mertenslem1  13336  mertens  13338  efaddlem  13370  sinadd  13440  cosadd  13441  tanaddlem  13442  tanadd  13443  addsin  13446  sincossq  13452  sin2t  13453  dvds2ln  13555  oddm1even  13585  sadadd2lem2  13638  bezoutlem2  13715  bezoutlem3  13716  bezoutlem4  13717  phiprmpw  13843  pythagtriplem12  13885  pythagtriplem14  13887  pythagtriplem16  13889  pcpremul  13902  pcaddlem  13942  fldivp1  13951  mul4sqlem  14006  4sqlem14  14011  vdwapun  14027  vdwlem2  14035  vdwlem6  14039  zringlpirlem3  17885  zlpirlem3  17890  znunit  17976  blcvx  20355  icopnfcnv  20494  mbfmulc2re  21106  mbfmulc2  21121  itg1addlem4  21157  itg1addlem5  21158  itg1mulc  21162  mbfmul  21184  itgcl  21241  itgcnlem  21247  iblmulc2  21288  itgmulc2  21291  itgabs  21292  itgsplit  21293  dvmulbr  21393  dvcmul  21398  dvcmulf  21399  dvexp  21407  dvmptcmul  21418  dvexp3  21430  dvsincos  21433  cmvth  21443  dvlipcn  21446  dvfsumabs  21475  dvfsumlem1  21478  ftc1lem4  21491  itgparts  21499  plyf  21646  ply1termlem  21651  plyeq0lem  21658  plypf1  21660  plyaddlem1  21661  plymullem1  21662  coeeulem  21672  coeidlem  21685  coeid3  21688  plyco  21689  coemullem  21697  coemulhi  21701  coemulc  21702  dgrcolem2  21721  plycjlem  21723  plyrecj  21726  dvply1  21730  vieta1lem2  21757  vieta1  21758  elqaalem3  21767  aareccl  21772  aalioulem1  21778  taylfvallem1  21802  tayl0  21807  dvtaylp  21815  taylthlem2  21819  psergf  21857  radcnvlem1  21858  dvradcnv  21866  psercn2  21868  pserdvlem2  21873  pserdv2  21875  abelthlem4  21879  abelthlem5  21880  abelthlem6  21881  abelthlem7  21883  abelthlem9  21885  tanregt0  21975  cosargd  22037  abslogle  22047  tanarg  22048  advlogexp  22080  logtayllem  22084  logtayl  22085  cxpadd  22104  mulcxp  22110  cxpmul  22113  cxpmul2  22114  cxpmul2z  22116  abscxp  22117  abscxp2  22118  dvcxp2  22161  abscxpbnd  22171  root1eq1  22173  cxpeq  22175  angcan  22178  pythag  22193  ssscongptld  22200  affineequiv  22201  affineequiv2  22202  chordthmlem2  22208  chordthmlem3  22209  chordthmlem4  22210  chordthmlem5  22211  heron  22213  quad2  22214  quad  22215  dcubic1lem  22218  dcubic2  22219  dcubic1  22220  dcubic  22221  mcubic  22222  cubic2  22223  cubic  22224  binom4  22225  dquartlem1  22226  dquartlem2  22227  dquart  22228  quart1cl  22229  quart1lem  22230  quart1  22231  quartlem1  22232  quartlem2  22233  atantayl3  22314  leibpi  22317  birthdaylem2  22326  divsqrsumo1  22357  cvxcl  22358  jensenlem2  22361  wilthlem2  22387  ftalem1  22390  ftalem2  22391  ftalem4  22393  ftalem5  22394  basellem2  22399  basellem3  22400  basellem8  22405  muinv  22513  fsumdvdsmul  22515  logfacrlim  22543  logexprlim  22544  perfectlem2  22549  bposlem9  22611  lgsquad2lem1  22677  2sqlem3  22685  rplogsumlem1  22713  dchrisumlem2  22719  dchrisumlem3  22720  dchrmusum2  22723  dchrvmasumlem1  22724  dchrvmasum2lem  22725  dchrvmasum2if  22726  dchrvmasumlem3  22728  dchrvmasumiflem1  22730  dchrvmasumiflem2  22731  rpvmasum2  22741  dchrisum0lem1  22745  dchrisum0lem2a  22746  dchrisum0lem2  22747  dchrmusumlem  22751  dchrvmasumlem  22752  rplogsum  22756  mudivsum  22759  mulogsumlem  22760  mulogsum  22761  mulog2sumlem1  22763  mulog2sumlem2  22764  mulog2sumlem3  22765  vmalogdivsum  22768  logsqvma  22771  log2sumbnd  22773  selberglem1  22774  selberglem2  22775  selberglem3  22776  selberg  22777  selberg2lem  22779  selberg2  22780  selberg3lem1  22786  selberg3  22788  selberg4lem1  22789  selberg4  22790  pntrsumo1  22794  selbergr  22797  selberg3r  22798  selberg4r  22799  selberg34r  22800  pntsval2  22805  pntrlog2bndlem1  22806  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntrlog2bndlem6  22812  pntrlog2bnd  22813  pntlemb  22826  pntlemf  22834  pntlemo  22836  ostth2lem2  22863  ostth2lem3  22864  ttgcontlem1  23099  brbtwn2  23119  colinearalg  23124  ax5seglem2  23143  ax5seglem9  23151  axeuclidlem  23176  axcontlem2  23179  axcontlem4  23181  axcontlem7  23184  axcontlem8  23185  ipval2  24070  dipcl  24078  riesz3i  25434  mul2lt0rlt0  26006  cnre2csqima  26310  rmulccn  26327  indsum  26448  dya2icoseg  26661  oddpwdc  26706  eulerpartlems  26712  eulerpartlemsv3  26713  eulerpartlemgs2  26732  signsplypnf  26920  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamgulmlem4  26987  lgamgulmlem5  26988  lgamgulmlem6  26989  lgamgulm2  26991  lgamcvg2  27010  gamcvg  27011  gamcvg2lem  27014  subfacval2  27044  subfaclim  27045  rescon  27104  subdivcomb1  27353  subdivcomb2  27354  fprodmul  27440  iprodmul  27472  iprodgam  27475  binomfallfaclem1  27511  binomfallfaclem2  27512  binomrisefac  27514  bpolycl  28164  bpolysum  28165  bpolydiflem  28166  bpoly4  28171  iblmulc2nc  28428  itgmulc2nc  28431  itgabsnc  28432  ftc1cnnclem  28436  ftc1anclem3  28440  dvasin  28451  areacirclem1  28455  areacirclem4  28458  areacirc  28460  cntotbnd  28666  pellexlem1  29141  pellexlem2  29142  pellexlem6  29146  pell1234qrne0  29165  pell1234qrreccl  29166  pell1234qrmulcl  29167  pell1234qrdich  29173  pell14qrdich  29181  pell1qrge1  29182  pell1qrgaplem  29185  qirropth  29220  rmxyneg  29232  rmxyadd  29233  rmxm1  29246  rmym1  29247  rmxluc  29248  rmyluc  29249  rmxdbl  29251  rmydbl  29252  jm2.18  29308  jm2.19lem1  29309  jm2.19lem2  29310  jm2.19lem4  29312  jm2.19  29313  jm2.22  29315  jm2.23  29316  jm2.25  29319  jm2.27c  29327  jm3.1lem2  29338  flcidc  29502  itgpowd  29561  areaquad  29563  expgrowth  29580  mulc1cncfg  29741  clim1fr1  29745  dvsinexp  29758  itgsinexplem1  29765  itgsinexp  29766  stoweidlem1  29767  stoweidlem11  29777  stoweidlem13  29779  stoweidlem14  29780  stoweidlem17  29783  stoweidlem25  29791  stoweidlem26  29792  stoweidlem42  29808  wallispilem4  29834  wallispilem5  29835  wallispi  29836  wallispi2lem1  29837  wallispi2lem2  29838  wallispi2  29839  stirlinglem1  29840  stirlinglem3  29842  stirlinglem4  29843  stirlinglem5  29844  stirlinglem6  29845  stirlinglem7  29846  stirlinglem8  29847  stirlinglem10  29849  stirlinglem11  29850  stirlinglem12  29851  stirlinglem13  29852  stirlinglem14  29853  stirlinglem15  29854  sigarim  29858  sigarac  29859  sigaraf  29860  sigarmf  29861  sigarls  29864  sigardiv  29868  sigarcol  29871  cevathlem1  29874  kcnktkm1cn  30141  altgsumbcALT  30719  i2linesd  31060  sineq0ALT  31602  bj-subcom  32485  bj-lineq  32492  bj-bary1lem  32494  bj-bary1lem1  32495  bj-bary1  32496
  Copyright terms: Public domain W3C validator