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

Theorem mulid2d 8853
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 8836 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 15 1  |-  ( ph  ->  ( 1  x.  A
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735   1c1 8738    x. cmul 8742
This theorem is referenced by:  addid1  8992  mulcand  9401  receu  9413  divdivdiv  9461  divcan5  9462  subrec  9589  ltrec  9637  recp1lt1  9654  nndivtr  9787  gtndiv  10089  lincmb01cmp  10777  iccf1o  10778  modfrac  10984  m1expcl2  11125  expgt1  11140  ltexp2a  11153  leexp2a  11157  binom3  11222  faclbnd  11303  faclbnd4lem4  11309  facavg  11314  bcval5  11330  sqrlem2  11729  absimle  11794  reccn2  12070  iseraltlem2  12155  iseraltlem3  12156  o1fsum  12271  abscvgcvg  12277  ackbijnn  12286  binom1p  12289  binom1dif  12291  incexclem  12295  incexc  12296  climcndslem1  12308  geomulcvg  12332  efcllem  12359  ef01bndlem  12464  efieq1re  12479  eirrlem  12482  iddvds  12542  bitsfzolem  12625  bitsfzo  12626  rpmulgcd  12734  prmind2  12769  isprm5  12791  phiprm  12845  eulerthlem2  12850  fermltl  12852  odzdvds  12860  pythagtriplem4  12872  pcexp  12912  4sqlem18  13009  vdwapun  13021  mulgnnass  14595  odinv  14874  odadd2  15141  pgpfaclem2  15317  abvneg  15599  nrginvrcnlem  18201  nmoid  18251  blcvx  18304  icopnfcnv  18440  reparphti  18495  pcorevlem  18524  itg11  19046  itg2mulc  19102  itg2monolem1  19105  itgcnlem  19144  iblabs  19183  dvexp  19302  dvef  19327  lhop1lem  19360  dvcvx  19367  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem4  19376  dvfsum2  19381  plypow  19587  dgrcolem1  19654  vieta1lem2  19691  radcnvlem1  19789  radcnvlem2  19790  dvradcnv  19797  abelthlem2  19808  abelthlem6  19812  abelthlem7  19814  abelth2  19818  sinhalfpip  19860  sinhalfpim  19861  coshalfpip  19862  coshalfpim  19863  tangtx  19873  efif1olem4  19907  logdivlti  19971  advlog  20001  advlogexp  20002  logtayl  20007  cxpaddlelem  20091  cxpaddle  20092  affineequiv  20123  affineequiv2  20124  chordthmlem5  20133  dcubic2  20140  dcubic  20142  mcubic  20143  binom4  20146  dquartlem1  20147  quart1lem  20151  quart1  20152  quartlem1  20153  quart  20157  efiasin  20184  atantayl  20233  cvxcl  20279  scvxcvx  20280  wilthlem1  20306  wilthlem2  20307  basellem9  20326  fsumfldivdiaglem  20429  muinv  20433  chpub  20459  logexprlim  20464  mersenne  20466  perfectlem2  20469  dchrmulid2  20491  dchrptlem1  20503  dchrsum2  20507  sumdchr2  20509  bposlem2  20524  bposlem9  20531  lgsval2lem  20545  lgsval4a  20557  lgsneg1  20559  lgsdir2lem4  20565  lgsdir  20569  lgsdirnn0  20578  lgsdinn0  20579  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem4  20591  lgsquad2lem1  20597  2sqlem8  20611  chebbnd1lem3  20620  chpchtlim  20628  rplogsumlem1  20633  rplogsumlem2  20634  rpvmasumlem  20636  dchrmusum2  20643  dchrvmasum2lem  20645  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrisum0flblem1  20657  mulog2sumlem2  20684  vmalogdivsum2  20687  2vmadivsumlem  20689  log2sumbnd  20693  selberglem2  20695  chpdifbndlem1  20702  selberg3lem1  20706  selberg4lem1  20709  pntrlog2bndlem2  20727  pntrlog2bndlem5  20730  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntlemb  20746  pntlemr  20751  pntlemk  20755  pntlemo  20756  ablomul  21022  mulid  21023  nvm1  21230  nvpi  21232  nvmtri  21237  ipval2  21280  ipasslem1  21409  ipasslem4  21412  bcs2  21761  lnfnaddi  22623  subfacp1lem6  23127  subfaclim  23130  cvxpcon  23184  cvxscon  23185  rescon  23188  sinccvglem  23416  brbtwn2  23944  colinearalglem4  23948  ax5seglem3  23970  axbtwnid  23978  axpaschlem  23979  axeuclidlem  24001  axcontlem7  24009  axcontlem8  24010  bpolysum  24199  bpolydiflem  24200  bpoly4  24205  areacirclem2  24337  mulone  25097  nn0prpwlem  25650  bfplem2  25959  bfp  25960  rrntotbnd  25972  irrapxlem5  26323  pellexlem2  26327  pellexlem6  26331  pellfundex  26383  jm2.19lem3  26496  jm2.25  26504  jm2.27c  26512  jm3.1lem2  26523  flcidc  26791  hashgcdlem  26928  itgsinexp  27161  wallispilem5  27230  wallispi2lem1  27232  wallispi2  27234  stirlinglem1  27235  stirlinglem3  27237  stirlinglem4  27238  stirlinglem5  27239  stirlinglem6  27240  stirlinglem7  27241  stirlinglem10  27244
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-mulcom 8801  ax-mulass 8803  ax-distr 8804  ax-1rid 8807  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator