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

Theorem mulid2d 10096
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 10076 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972  1c1 9975   · cmul 9979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-mulcom 10038  ax-mulass 10040  ax-distr 10041  ax-1rid 10044  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  adddirp1d  10104  addid1  10254  mulsubfacd  10530  mulcand  10698  receu  10710  divdivdiv  10764  divcan5  10765  subrec  10892  ltrec  10943  recp1lt1  10959  nndivtr  11100  subhalfhalf  11304  xp1d2m1eqxm1d2  11324  gtndiv  11492  lincmb01cmp  12353  iccf1o  12354  ltdifltdiv  12675  modfrac  12723  negmod  12755  addmodid  12758  m1expcl2  12922  expgt1  12938  ltexp2a  12952  leexp2a  12956  binom3  13025  faclbnd  13117  faclbnd4lem4  13123  facavg  13128  bcval5  13145  cshweqrep  13613  sqrlem2  14028  absimle  14093  reccn2  14371  iseraltlem2  14457  iseraltlem3  14458  o1fsum  14589  abscvgcvg  14595  ackbijnn  14604  binom1p  14607  binom1dif  14609  incexclem  14612  incexc  14613  climcndslem1  14625  geomulcvg  14651  fprodsplit  14740  fallrisefac  14800  bpolysum  14828  bpolydiflem  14829  bpoly4  14834  efcllem  14852  ef01bndlem  14958  efieq1re  14973  eirrlem  14976  iddvds  15042  pwp1fsum  15161  oddpwp1fsum  15162  bitsfzolem  15203  bitsfzo  15204  rpmulgcd  15322  prmind2  15445  isprm5  15466  phiprm  15529  eulerthlem2  15534  fermltl  15536  hashgcdlem  15540  odzdvds  15547  powm2modprm  15555  modprm0  15557  pythagtriplem4  15571  pcexp  15611  4sqlem18  15713  vdwapun  15725  mulgnnass  17623  mulgnnassOLD  17624  odinv  18024  odadd2  18298  pgpfaclem2  18527  abvneg  18882  nrginvrcnlem  22542  nmoid  22593  blcvx  22648  icopnfcnv  22788  reparphti  22843  pcorevlem  22872  ncvsm1  23000  ncvspi  23002  cphipval2  23086  cphipval  23088  itg11  23503  itg2mulc  23559  itg2monolem1  23562  itgcnlem  23601  iblabs  23640  dvexp  23761  dvmptdiv  23782  dvef  23788  lhop1lem  23821  dvcvx  23828  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumlem4  23837  dvfsum2  23842  plypow  24006  dgrcolem1  24074  vieta1lem2  24111  radcnvlem1  24212  radcnvlem2  24213  dvradcnv  24220  abelthlem2  24231  abelthlem6  24235  abelthlem7  24237  abelth2  24241  sinhalfpip  24289  sinhalfpim  24290  coshalfpip  24291  coshalfpim  24292  tangtx  24302  efif1olem4  24336  abslogle  24409  logdivlti  24411  advlog  24445  advlogexp  24446  logtayl  24451  cxpaddlelem  24537  cxpaddle  24538  affineequiv  24598  affineequiv2  24599  chordthmlem5  24608  dcubic2  24616  dcubic  24618  mcubic  24619  binom4  24622  dquartlem1  24623  quart1lem  24627  quart1  24628  quartlem1  24629  quart  24633  efiasin  24660  atantayl  24709  cvxcl  24756  scvxcvx  24757  lgamgulmlem5  24804  lgamcvg2  24826  lgam1  24835  wilthlem1  24839  wilthlem2  24840  basellem9  24860  fsumfldivdiaglem  24960  muinv  24964  chpub  24990  logexprlim  24995  mersenne  24997  perfectlem2  25000  dchrmulid2  25022  dchrptlem1  25034  dchrsum2  25038  sumdchr2  25040  bposlem2  25055  bposlem9  25062  lgsval2lem  25077  lgsval4a  25089  lgsneg1  25092  lgsdir2lem4  25098  lgsdir  25102  lgsmulsqcoprm  25113  lgsdirnn0  25114  lgsdinn0  25115  gausslemma2dlem1a  25135  gausslemma2dlem4  25139  gausslemma2dlem7  25143  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem4  25148  lgsquad2lem1  25154  2sqlem8  25196  chebbnd1lem3  25205  chpchtlim  25213  rplogsumlem1  25218  rplogsumlem2  25219  rpvmasumlem  25221  dchrmusum2  25228  dchrvmasum2lem  25230  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrisum0flblem1  25242  mulog2sumlem2  25269  vmalogdivsum2  25272  2vmadivsumlem  25274  log2sumbnd  25278  selberglem2  25280  chpdifbndlem1  25287  selberg3lem1  25291  selberg4lem1  25294  pntrlog2bndlem2  25312  pntrlog2bndlem5  25315  pntpbnd1  25320  pntpbnd2  25321  pntibndlem2  25325  pntlemb  25331  pntlemr  25336  pntlemk  25340  pntlemo  25341  brbtwn2  25830  colinearalglem4  25834  ax5seglem3  25856  axbtwnid  25864  axpaschlem  25865  axeuclidlem  25887  axcontlem7  25895  axcontlem8  25896  nvm1  27648  nvpi  27650  nvmtri  27654  ipval2  27690  ipasslem1  27814  ipasslem4  27817  bcs2  28167  lnfnaddi  29030  nnmulge  29643  sqsscirc1  30082  indsum  30211  indsumin  30212  eulerpartlemgs2  30570  plymulx0  30752  logdivsqrle  30856  subfacp1lem6  31293  subfaclim  31296  cvxpconn  31350  cvxsconn  31351  resconn  31354  sinccvglem  31692  fwddifn0  32396  nn0prpwlem  32442  knoppndvlem9  32636  knoppndvlem14  32641  bj-bary1lem1  33291  mblfinlem3  33578  itg2addnclem3  33593  iblabsnc  33604  iblmulc2nc  33605  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  areacirclem1  33630  bfplem2  33752  bfp  33753  rrntotbnd  33765  irrapxlem5  37707  pellexlem2  37711  pellexlem6  37715  pellfundex  37767  jm2.19lem3  37875  jm2.25  37883  jm2.27c  37891  jm3.1lem2  37902  flcidc  38061  int-mul12d  38803  cvgdvgrat  38829  bccn1  38860  binomcxplemnotnn0  38872  fperiodmullem  39831  xralrple2  39883  fmul01lt1lem2  40135  mccllem  40147  reclimc  40203  cosknegpi  40398  dvsinax  40445  dvnxpaek  40475  dvnmul  40476  itgsinexp  40488  stoweidlem14  40549  stoweidlem26  40561  wallispilem4  40603  wallispilem5  40604  wallispi2lem1  40606  wallispi2  40608  stirlinglem1  40609  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkercncflem2  40639  fourierdlem26  40668  fourierdlem41  40683  fourierdlem42  40684  fourierdlem56  40697  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem64  40705  fourierdlem65  40706  fourierdlem95  40736  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  etransclem23  40792  etransclem35  40804  etransclem46  40815  fmtnorec2lem  41779  fmtnorec3  41785  pwdif  41826  m1expoddALTV  41886  perfectALTVlem2  41956  ztprmneprm  42450  altgsumbc  42455  divge1b  42627  divgt1b  42628
  Copyright terms: Public domain W3C validator