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

Theorem mulid2d 9392
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
mulid2d  |-  ( ph  ->  ( 1  x.  A
)  =  A )

Proof of Theorem mulid2d
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mulid2 9372 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 1  x.  A
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755  (class class class)co 6080   CCcc 9268   1c1 9271    x. cmul 9275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-mulcl 9332  ax-mulcom 9334  ax-mulass 9336  ax-distr 9337  ax-1rid 9340  ax-cnre 9343
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083
This theorem is referenced by:  addid1  9537  mulcand  9957  receu  9969  divdivdiv  10020  divcan5  10021  subrec  10148  ltrec  10201  recp1lt1  10218  nndivtr  10351  gtndiv  10707  lincmb01cmp  11415  iccf1o  11416  ltdifltdiv  11662  modfrac  11705  modvalp1  11710  m1expcl2  11871  expgt1  11886  ltexp2a  11899  leexp2a  11903  binom3  11969  faclbnd  12050  faclbnd4lem4  12056  facavg  12061  bcval5  12078  cshweqrep  12439  sqrlem2  12717  absimle  12782  reccn2  13058  iseraltlem2  13144  iseraltlem3  13145  o1fsum  13259  abscvgcvg  13265  ackbijnn  13274  binom1p  13277  binom1dif  13279  incexclem  13282  incexc  13283  climcndslem1  13295  geomulcvg  13319  efcllem  13346  ef01bndlem  13451  efieq1re  13466  eirrlem  13469  iddvds  13529  bitsfzolem  13613  bitsfzo  13614  rpmulgcd  13722  prmind2  13757  isprm5  13781  phiprm  13835  eulerthlem2  13840  fermltl  13842  odzdvds  13850  modprm0  13856  pythagtriplem4  13869  pcexp  13909  4sqlem18  14006  vdwapun  14018  mulgnnass  15635  odinv  16042  odadd2  16311  pgpfaclem2  16557  abvneg  16843  nrginvrcnlem  20113  nmoid  20163  blcvx  20217  icopnfcnv  20356  reparphti  20411  pcorevlem  20440  itg11  21011  itg2mulc  21067  itg2monolem1  21070  itgcnlem  21109  iblabs  21148  dvexp  21269  dvef  21294  lhop1lem  21327  dvcvx  21334  dvfsumlem1  21340  dvfsumlem2  21341  dvfsumlem4  21343  dvfsum2  21348  plypow  21558  dgrcolem1  21625  vieta1lem2  21662  radcnvlem1  21763  radcnvlem2  21764  dvradcnv  21771  abelthlem2  21782  abelthlem6  21786  abelthlem7  21788  abelth2  21792  sinhalfpip  21839  sinhalfpim  21840  coshalfpip  21841  coshalfpim  21842  tangtx  21852  efif1olem4  21886  abslogle  21952  logdivlti  21954  advlog  21984  advlogexp  21985  logtayl  21990  cxpaddlelem  22074  cxpaddle  22075  affineequiv  22106  affineequiv2  22107  chordthmlem5  22116  dcubic2  22124  dcubic  22126  mcubic  22127  binom4  22130  dquartlem1  22131  quart1lem  22135  quart1  22136  quartlem1  22137  quart  22141  efiasin  22168  atantayl  22217  cvxcl  22263  scvxcvx  22264  wilthlem1  22291  wilthlem2  22292  basellem9  22311  fsumfldivdiaglem  22414  muinv  22418  chpub  22444  logexprlim  22449  mersenne  22451  perfectlem2  22454  dchrmulid2  22476  dchrptlem1  22488  dchrsum2  22492  sumdchr2  22494  bposlem2  22509  bposlem9  22516  lgsval2lem  22530  lgsval4a  22542  lgsneg1  22544  lgsdir2lem4  22550  lgsdir  22554  lgsdirnn0  22563  lgsdinn0  22564  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem4  22576  lgsquad2lem1  22582  2sqlem8  22596  chebbnd1lem3  22605  chpchtlim  22613  rplogsumlem1  22618  rplogsumlem2  22619  rpvmasumlem  22621  dchrmusum2  22628  dchrvmasum2lem  22630  dchrvmasumlem2  22632  dchrvmasumlem3  22633  dchrisum0flblem1  22642  mulog2sumlem2  22669  vmalogdivsum2  22672  2vmadivsumlem  22674  log2sumbnd  22678  selberglem2  22680  chpdifbndlem1  22687  selberg3lem1  22691  selberg4lem1  22694  pntrlog2bndlem2  22712  pntrlog2bndlem5  22715  pntpbnd1  22720  pntpbnd2  22721  pntibndlem2  22725  pntlemb  22731  pntlemr  22736  pntlemk  22740  pntlemo  22741  brbtwn2  22974  colinearalglem4  22978  ax5seglem3  23000  axbtwnid  23008  axpaschlem  23009  axeuclidlem  23031  axcontlem7  23039  axcontlem8  23040  ablomul  23665  mulid  23666  nvm1  23875  nvpi  23877  nvmtri  23882  ipval2  23925  ipasslem1  24054  ipasslem4  24057  bcs2  24407  lnfnaddi  25270  sqsscirc1  26192  indsum  26333  eulerpartlemgs2  26611  plymulx0  26796  lgamgulmlem5  26867  lgamcvg2  26889  lgam1  26898  subfacp1lem6  26921  subfaclim  26924  cvxpcon  26979  cvxscon  26980  rescon  26983  sinccvglem  27164  fprodsplit  27323  fallrisefac  27375  bpolysum  28043  bpolydiflem  28044  bpoly4  28049  mblfinlem3  28274  itg2addnclem3  28289  iblabsnc  28300  iblmulc2nc  28301  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  areacirclem1  28328  nn0prpwlem  28361  bfplem2  28566  bfp  28567  rrntotbnd  28579  irrapxlem5  29012  pellexlem2  29016  pellexlem6  29020  pellfundex  29072  jm2.19lem3  29185  jm2.25  29193  jm2.27c  29201  jm3.1lem2  29212  flcidc  29376  hashgcdlem  29410  fmul01lt1lem2  29611  itgsinexp  29641  stoweidlem14  29655  stoweidlem26  29667  wallispilem4  29709  wallispilem5  29710  wallispi2lem1  29712  wallispi2  29714  stirlinglem1  29715  stirlinglem3  29717  stirlinglem4  29718  stirlinglem5  29719  stirlinglem6  29720  stirlinglem7  29721  stirlinglem10  29724  mulsubfacd  30018  powm2modprm  30094  ztprmneprm  30584  bj-bary1lem1  32196
  Copyright terms: Public domain W3C validator