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

Theorem mulid2d 10653
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
mulid2d (𝜑 → (1 · 𝐴) = 𝐴)

Proof of Theorem mulid2d
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mulid2 10634 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  (class class class)co 7146  cc 10529  1c1 10532   · cmul 10536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-mulcl 10593  ax-mulcom 10595  ax-mulass 10597  ax-distr 10598  ax-1rid 10601  ax-cnre 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3138  df-rex 3139  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4826  df-br 5054  df-iota 6303  df-fv 6352  df-ov 7149
This theorem is referenced by:  adddirp1d  10661  addid1  10814  mulsubfacd  11095  mulcand  11267  receu  11279  divdivdiv  11335  divcan5  11336  subrec  11463  ltrec  11516  recp1lt1  11532  nndivtr  11679  subhalfhalf  11866  xp1d2m1eqxm1d2  11886  gtndiv  12054  lincmb01cmp  12880  iccf1o  12881  ltdifltdiv  13206  modfrac  13254  negmod  13286  addmodid  13289  m1expcl2  13454  expgt1  13470  ltexp2a  13533  leexp2a  13539  binom3  13588  faclbnd  13653  faclbnd4lem4  13659  facavg  13664  bcval5  13681  cshweqrep  14181  sqrlem2  14601  absimle  14667  reccn2  14951  iseraltlem2  15037  iseraltlem3  15038  o1fsum  15166  abscvgcvg  15172  ackbijnn  15181  binom1p  15184  binom1dif  15186  incexclem  15189  incexc  15190  climcndslem1  15202  pwdif  15221  geomulcvg  15230  fprodsplit  15318  fallrisefac  15377  bpolysum  15405  bpolydiflem  15406  bpoly4  15411  efcllem  15429  ef01bndlem  15535  efieq1re  15550  eirrlem  15555  iddvds  15621  pwp1fsum  15738  oddpwp1fsum  15739  bitsfzolem  15779  bitsfzo  15780  rpmulgcd  15902  prmind2  16025  isprm5  16047  phiprm  16110  eulerthlem2  16115  fermltl  16117  hashgcdlem  16121  odzdvds  16128  powm2modprm  16136  modprm0  16138  pythagtriplem4  16152  4sqlem18  16294  vdwapun  16306  mulgnnass  18260  odinv  18686  odadd2  18967  pgpfaclem2  19202  abvneg  19600  nrginvrcnlem  23295  nmoid  23346  blcvx  23401  icopnfcnv  23545  reparphti  23600  pcorevlem  23629  ncvsm1  23757  ncvspi  23759  cphipval2  23843  cphipval  23845  itg11  24293  itg2mulc  24349  itg2monolem1  24352  itgcnlem  24391  iblabs  24430  dvexp  24554  dvmptdiv  24575  dvef  24581  lhop1lem  24614  dvcvx  24621  dvfsumlem1  24627  dvfsumlem2  24628  dvfsumlem4  24630  dvfsum2  24635  plypow  24800  dgrcolem1  24868  vieta1lem2  24905  radcnvlem1  25006  radcnvlem2  25007  dvradcnv  25014  abelthlem6  25029  abelthlem7  25031  abelth2  25035  sinhalfpip  25083  sinhalfpim  25084  coshalfpip  25085  coshalfpim  25086  tangtx  25096  efif1olem4  25135  abslogle  25207  logdivlti  25209  advlog  25243  advlogexp  25244  logtayl  25249  cxpaddlelem  25338  cxpaddle  25339  affineequiv  25407  affineequiv2  25408  chordthmlem5  25420  dcubic2  25428  dcubic  25430  mcubic  25431  binom4  25434  dquartlem1  25435  quart1lem  25439  quart1  25440  quartlem1  25441  quart  25445  efiasin  25472  atantayl  25521  cvxcl  25568  scvxcvx  25569  lgamgulmlem5  25616  lgamcvg2  25638  lgam1  25647  wilthlem1  25651  wilthlem2  25652  basellem9  25672  fsumfldivdiaglem  25772  muinv  25776  chpub  25802  logexprlim  25807  mersenne  25809  perfectlem2  25812  dchrmulid2  25834  dchrptlem1  25846  dchrsum2  25850  sumdchr2  25852  bposlem2  25867  bposlem9  25874  lgsval2lem  25889  lgsval4a  25901  lgsneg1  25904  lgsdir2lem4  25910  lgsdir  25914  lgsmulsqcoprm  25925  lgsdirnn0  25926  lgsdinn0  25927  gausslemma2dlem1a  25947  gausslemma2dlem4  25951  gausslemma2dlem7  25955  gausslemma2d  25956  lgseisenlem1  25957  lgseisenlem2  25958  lgseisenlem4  25960  lgsquad2lem1  25966  2sqlem8  26008  chebbnd1lem3  26053  chpchtlim  26061  rplogsumlem1  26066  rplogsumlem2  26067  rpvmasumlem  26069  dchrmusum2  26076  dchrvmasum2lem  26078  dchrvmasumlem2  26080  dchrvmasumlem3  26081  dchrisum0flblem1  26090  mulog2sumlem2  26117  vmalogdivsum2  26120  2vmadivsumlem  26122  log2sumbnd  26126  selberglem2  26128  selberg3lem1  26139  selberg4lem1  26142  pntrlog2bndlem2  26160  pntrlog2bndlem5  26163  pntpbnd1  26168  pntpbnd2  26169  pntibndlem2  26173  pntlemb  26179  pntlemr  26184  pntlemk  26188  pntlemo  26189  brbtwn2  26697  colinearalglem4  26701  ax5seglem3  26723  axbtwnid  26731  axpaschlem  26732  axeuclidlem  26754  axcontlem7  26762  axcontlem8  26763  elntg2  26777  nvm1  28446  nvpi  28448  nvmtri  28452  ipval2  28488  ipasslem1  28612  ipasslem4  28615  bcs2  28963  lnfnaddi  29824  nnmulge  30480  ccfldsrarelvec  31086  sqsscirc1  31178  indsum  31307  indsumin  31308  eulerpartlemgs2  31665  plymulx0  31844  logdivsqrle  31948  subfacp1lem6  32459  subfaclim  32462  cvxpconn  32516  cvxsconn  32517  resconn  32520  sinccvglem  32942  fwddifn0  33652  nn0prpwlem  33697  knoppndvlem9  33886  knoppndvlem14  33891  bj-bary1lem1  34640  mblfinlem3  35008  itg2addnclem3  35022  iblabsnc  35033  iblmulc2nc  35034  ftc1anclem6  35047  ftc1anclem7  35048  ftc1anclem8  35049  areacirclem1  35057  bfplem2  35173  bfp  35174  rrntotbnd  35186  lcmineqlem1  39225  lcmineqlem12  39236  lcmineqlem18  39242  3lexlogpow5ineq2  39250  fltnlta  39475  3cubeslem2  39482  3cubeslem3r  39484  irrapxlem5  39623  pellexlem2  39627  pellexlem6  39631  pellfundex  39683  jm2.19lem3  39788  jm2.25  39796  jm2.27c  39804  jm3.1lem2  39815  flcidc  39974  reabssgn  40192  sqrtcval  40197  int-mul12d  40748  cvgdvgrat  40877  bccn1  40908  binomcxplemnotnn0  40920  fperiodmullem  41801  xralrple2  41852  fmul01lt1lem2  42093  mccllem  42105  reclimc  42161  cosknegpi  42377  dvsinax  42421  dvnxpaek  42450  dvnmul  42451  itgsinexp  42463  stoweidlem14  42522  stoweidlem26  42534  wallispilem4  42576  wallispilem5  42577  wallispi2lem1  42579  wallispi2  42581  stirlinglem1  42582  stirlinglem3  42584  stirlinglem4  42585  stirlinglem5  42586  stirlinglem6  42587  stirlinglem7  42588  stirlinglem10  42591  dirkertrigeqlem2  42607  dirkertrigeqlem3  42608  dirkercncflem2  42612  fourierdlem26  42641  fourierdlem41  42656  fourierdlem42  42657  fourierdlem56  42670  fourierdlem57  42671  fourierdlem58  42672  fourierdlem62  42676  fourierdlem64  42678  fourierdlem65  42679  fourierdlem95  42709  sqwvfoura  42736  sqwvfourb  42737  fouriersw  42739  etransclem23  42765  etransclem35  42777  etransclem46  42788  fmtnorec2lem  43925  fmtnorec3  43931  m1expoddALTV  44032  perfectALTVlem2  44106  ztprmneprm  44614  altgsumbc  44619  divge1b  44786  divgt1b  44787  ackval1  44949  affineid  44972  1subrec1sub  44973  rrx2vlinest  45009  line2x  45022
  Copyright terms: Public domain W3C validator