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

Theorem mulid2d 9505
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 9485 . 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 1370    e. wcel 1758  (class class class)co 6190   CCcc 9381   1c1 9384    x. cmul 9388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-mulcl 9445  ax-mulcom 9447  ax-mulass 9449  ax-distr 9450  ax-1rid 9453  ax-cnre 9456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193
This theorem is referenced by:  addid1  9650  mulcand  10070  receu  10082  divdivdiv  10133  divcan5  10134  subrec  10261  ltrec  10314  recp1lt1  10331  nndivtr  10464  gtndiv  10820  lincmb01cmp  11529  iccf1o  11530  ltdifltdiv  11779  modfrac  11822  modvalp1  11827  m1expcl2  11988  expgt1  12003  ltexp2a  12016  leexp2a  12020  binom3  12086  faclbnd  12167  faclbnd4lem4  12173  facavg  12178  bcval5  12195  cshweqrep  12557  sqrlem2  12835  absimle  12900  reccn2  13176  iseraltlem2  13262  iseraltlem3  13263  o1fsum  13378  abscvgcvg  13384  ackbijnn  13393  binom1p  13396  binom1dif  13398  incexclem  13401  incexc  13402  climcndslem1  13414  geomulcvg  13438  efcllem  13465  ef01bndlem  13570  efieq1re  13585  eirrlem  13588  iddvds  13648  bitsfzolem  13732  bitsfzo  13733  rpmulgcd  13841  prmind2  13876  isprm5  13900  phiprm  13954  eulerthlem2  13959  fermltl  13961  odzdvds  13969  modprm0  13975  pythagtriplem4  13988  pcexp  14028  4sqlem18  14125  vdwapun  14137  mulgnnass  15757  odinv  16166  odadd2  16435  pgpfaclem2  16688  abvneg  17025  nrginvrcnlem  20387  nmoid  20437  blcvx  20491  icopnfcnv  20630  reparphti  20685  pcorevlem  20714  itg11  21285  itg2mulc  21341  itg2monolem1  21344  itgcnlem  21383  iblabs  21422  dvexp  21543  dvef  21568  lhop1lem  21601  dvcvx  21608  dvfsumlem1  21614  dvfsumlem2  21615  dvfsumlem4  21617  dvfsum2  21622  plypow  21789  dgrcolem1  21856  vieta1lem2  21893  radcnvlem1  21994  radcnvlem2  21995  dvradcnv  22002  abelthlem2  22013  abelthlem6  22017  abelthlem7  22019  abelth2  22023  sinhalfpip  22070  sinhalfpim  22071  coshalfpip  22072  coshalfpim  22073  tangtx  22083  efif1olem4  22117  abslogle  22183  logdivlti  22185  advlog  22215  advlogexp  22216  logtayl  22221  cxpaddlelem  22305  cxpaddle  22306  affineequiv  22337  affineequiv2  22338  chordthmlem5  22347  dcubic2  22355  dcubic  22357  mcubic  22358  binom4  22361  dquartlem1  22362  quart1lem  22366  quart1  22367  quartlem1  22368  quart  22372  efiasin  22399  atantayl  22448  cvxcl  22494  scvxcvx  22495  wilthlem1  22522  wilthlem2  22523  basellem9  22542  fsumfldivdiaglem  22645  muinv  22649  chpub  22675  logexprlim  22680  mersenne  22682  perfectlem2  22685  dchrmulid2  22707  dchrptlem1  22719  dchrsum2  22723  sumdchr2  22725  bposlem2  22740  bposlem9  22747  lgsval2lem  22761  lgsval4a  22773  lgsneg1  22775  lgsdir2lem4  22781  lgsdir  22785  lgsdirnn0  22794  lgsdinn0  22795  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem4  22807  lgsquad2lem1  22813  2sqlem8  22827  chebbnd1lem3  22836  chpchtlim  22844  rplogsumlem1  22849  rplogsumlem2  22850  rpvmasumlem  22852  dchrmusum2  22859  dchrvmasum2lem  22861  dchrvmasumlem2  22863  dchrvmasumlem3  22864  dchrisum0flblem1  22873  mulog2sumlem2  22900  vmalogdivsum2  22903  2vmadivsumlem  22905  log2sumbnd  22909  selberglem2  22911  chpdifbndlem1  22918  selberg3lem1  22922  selberg4lem1  22925  pntrlog2bndlem2  22943  pntrlog2bndlem5  22946  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2  22956  pntlemb  22962  pntlemr  22967  pntlemk  22971  pntlemo  22972  brbtwn2  23286  colinearalglem4  23290  ax5seglem3  23312  axbtwnid  23320  axpaschlem  23321  axeuclidlem  23343  axcontlem7  23351  axcontlem8  23352  ablomul  23977  mulid  23978  nvm1  24187  nvpi  24189  nvmtri  24194  ipval2  24237  ipasslem1  24366  ipasslem4  24369  bcs2  24719  lnfnaddi  25582  sqsscirc1  26472  indsum  26613  eulerpartlemgs2  26897  plymulx0  27082  lgamgulmlem5  27153  lgamcvg2  27175  lgam1  27184  subfacp1lem6  27207  subfaclim  27210  cvxpcon  27265  cvxscon  27266  rescon  27269  sinccvglem  27451  fprodsplit  27610  fallrisefac  27662  bpolysum  28330  bpolydiflem  28331  bpoly4  28336  mblfinlem3  28568  itg2addnclem3  28583  iblabsnc  28594  iblmulc2nc  28595  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  areacirclem1  28622  nn0prpwlem  28655  bfplem2  28860  bfp  28861  rrntotbnd  28873  irrapxlem5  29305  pellexlem2  29309  pellexlem6  29313  pellfundex  29365  jm2.19lem3  29478  jm2.25  29486  jm2.27c  29494  jm3.1lem2  29505  flcidc  29669  hashgcdlem  29703  fmul01lt1lem2  29904  itgsinexp  29933  stoweidlem14  29947  stoweidlem26  29959  wallispilem4  30001  wallispilem5  30002  wallispi2lem1  30004  wallispi2  30006  stirlinglem1  30007  stirlinglem3  30009  stirlinglem4  30010  stirlinglem5  30011  stirlinglem6  30012  stirlinglem7  30013  stirlinglem10  30016  mulsubfacd  30310  powm2modprm  30386  ztprmneprm  30877  altgsumbc  30887  bj-bary1lem1  32906
  Copyright terms: Public domain W3C validator