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

Theorem mulid2d 10881
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 10862 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2112  (class class class)co 7235  cc 10757  1c1 10760   · cmul 10764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-mulcl 10821  ax-mulcom 10823  ax-mulass 10825  ax-distr 10826  ax-1rid 10829  ax-cnre 10832
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6359  df-fv 6409  df-ov 7238
This theorem is referenced by:  adddirp1d  10889  addid1  11042  mulsubfacd  11323  mulcand  11495  receu  11507  divdivdiv  11563  divcan5  11564  subrec  11691  ltrec  11744  recp1lt1  11760  nndivtr  11907  subhalfhalf  12094  xp1d2m1eqxm1d2  12114  gtndiv  12284  lincmb01cmp  13113  iccf1o  13114  ltdifltdiv  13439  modfrac  13489  negmod  13521  addmodid  13524  m1expcl2  13689  expgt1  13706  ltexp2a  13769  leexp2a  13775  binom3  13824  faclbnd  13889  faclbnd4lem4  13895  facavg  13900  bcval5  13917  cshweqrep  14419  sqrlem2  14840  absimle  14906  reccn2  15191  iseraltlem2  15279  iseraltlem3  15280  o1fsum  15410  abscvgcvg  15416  ackbijnn  15425  binom1p  15428  binom1dif  15430  incexclem  15433  incexc  15434  climcndslem1  15446  pwdif  15465  geomulcvg  15473  fprodsplit  15561  fallrisefac  15620  bpolysum  15648  bpolydiflem  15649  bpoly4  15654  efcllem  15672  ef01bndlem  15778  efieq1re  15793  eirrlem  15798  iddvds  15864  pwp1fsum  15985  oddpwp1fsum  15986  bitsfzolem  16026  bitsfzo  16027  rpmulgcd  16151  prmind2  16275  isprm5  16297  phiprm  16363  eulerthlem2  16368  fermltl  16370  hashgcdlem  16374  odzdvds  16381  powm2modprm  16389  modprm0  16391  pythagtriplem4  16405  4sqlem18  16548  vdwapun  16560  mulgnnass  18559  odinv  18985  odadd2  19267  pgpfaclem2  19502  abvneg  19903  nrginvrcnlem  23621  nmoid  23672  blcvx  23727  icopnfcnv  23871  reparphti  23926  pcorevlem  23955  ncvsm1  24083  ncvspi  24085  cphipval2  24170  cphipval  24172  itg11  24620  itg2mulc  24677  itg2monolem1  24680  itgcnlem  24719  iblabs  24758  dvexp  24882  dvmptdiv  24903  dvef  24909  lhop1lem  24942  dvcvx  24949  dvfsumlem1  24955  dvfsumlem2  24956  dvfsumlem4  24958  dvfsum2  24963  plypow  25131  dgrcolem1  25199  vieta1lem2  25236  radcnvlem1  25337  radcnvlem2  25338  dvradcnv  25345  abelthlem6  25360  abelthlem7  25362  abelth2  25366  sinhalfpip  25414  sinhalfpim  25415  coshalfpip  25416  coshalfpim  25417  tangtx  25427  efif1olem4  25466  abslogle  25538  logdivlti  25540  advlog  25574  advlogexp  25575  logtayl  25580  cxpaddlelem  25669  cxpaddle  25670  affineequiv  25738  affineequiv2  25739  chordthmlem5  25751  dcubic2  25759  dcubic  25761  mcubic  25762  binom4  25765  dquartlem1  25766  quart1lem  25770  quart1  25771  quartlem1  25772  quart  25776  efiasin  25803  atantayl  25852  cvxcl  25899  scvxcvx  25900  lgamgulmlem5  25947  lgamcvg2  25969  lgam1  25978  wilthlem1  25982  wilthlem2  25983  basellem9  26003  fsumfldivdiaglem  26103  muinv  26107  chpub  26133  logexprlim  26138  mersenne  26140  perfectlem2  26143  dchrmulid2  26165  dchrptlem1  26177  dchrsum2  26181  sumdchr2  26183  bposlem2  26198  bposlem9  26205  lgsval2lem  26220  lgsval4a  26232  lgsneg1  26235  lgsdir2lem4  26241  lgsdir  26245  lgsmulsqcoprm  26256  lgsdirnn0  26257  lgsdinn0  26258  gausslemma2dlem1a  26278  gausslemma2dlem4  26282  gausslemma2dlem7  26286  gausslemma2d  26287  lgseisenlem1  26288  lgseisenlem2  26289  lgseisenlem4  26291  lgsquad2lem1  26297  2sqlem8  26339  chebbnd1lem3  26384  chpchtlim  26392  rplogsumlem1  26397  rplogsumlem2  26398  rpvmasumlem  26400  dchrmusum2  26407  dchrvmasum2lem  26409  dchrvmasumlem2  26411  dchrvmasumlem3  26412  dchrisum0flblem1  26421  mulog2sumlem2  26448  vmalogdivsum2  26451  2vmadivsumlem  26453  log2sumbnd  26457  selberglem2  26459  selberg3lem1  26470  selberg4lem1  26473  pntrlog2bndlem2  26491  pntrlog2bndlem5  26494  pntpbnd1  26499  pntpbnd2  26500  pntibndlem2  26504  pntlemb  26510  pntlemr  26515  pntlemk  26519  pntlemo  26520  brbtwn2  27028  colinearalglem4  27032  ax5seglem3  27054  axbtwnid  27062  axpaschlem  27063  axeuclidlem  27085  axcontlem7  27093  axcontlem8  27094  elntg2  27108  nvm1  28778  nvpi  28780  nvmtri  28784  ipval2  28820  ipasslem1  28944  ipasslem4  28947  bcs2  29295  lnfnaddi  30156  nnmulge  30825  ccfldsrarelvec  31487  sqsscirc1  31604  indsum  31733  indsumin  31734  eulerpartlemgs2  32091  plymulx0  32270  logdivsqrle  32374  subfacp1lem6  32891  subfaclim  32894  cvxpconn  32948  cvxsconn  32949  resconn  32952  sinccvglem  33374  fwddifn0  34237  nn0prpwlem  34282  knoppndvlem9  34471  knoppndvlem14  34476  bj-bary1lem1  35253  mblfinlem3  35590  itg2addnclem3  35604  iblabsnc  35615  iblmulc2nc  35616  ftc1anclem6  35629  ftc1anclem7  35630  ftc1anclem8  35631  areacirclem1  35639  bfplem2  35755  bfp  35756  rrntotbnd  35768  lcmineqlem1  39808  lcmineqlem12  39819  lcmineqlem18  39825  aks4d1p1p7  39852  fltnlta  40251  3cubeslem2  40258  3cubeslem3r  40260  irrapxlem5  40399  pellexlem2  40403  pellexlem6  40407  pellfundex  40459  jm2.19lem3  40564  jm2.25  40572  jm2.27c  40580  jm3.1lem2  40591  flcidc  40750  reabssgn  40968  sqrtcval  40973  int-mul12d  41520  cvgdvgrat  41652  bccn1  41683  binomcxplemnotnn0  41695  fperiodmullem  42563  xralrple2  42614  fmul01lt1lem2  42847  mccllem  42859  reclimc  42915  cosknegpi  43131  dvsinax  43175  dvnxpaek  43204  dvnmul  43205  itgsinexp  43217  stoweidlem14  43276  stoweidlem26  43288  wallispilem4  43330  wallispilem5  43331  wallispi2lem1  43333  wallispi2  43335  stirlinglem1  43336  stirlinglem3  43338  stirlinglem4  43339  stirlinglem5  43340  stirlinglem6  43341  stirlinglem7  43342  stirlinglem10  43345  dirkertrigeqlem2  43361  dirkertrigeqlem3  43362  dirkercncflem2  43366  fourierdlem26  43395  fourierdlem41  43410  fourierdlem42  43411  fourierdlem56  43424  fourierdlem57  43425  fourierdlem58  43426  fourierdlem62  43430  fourierdlem64  43432  fourierdlem65  43433  fourierdlem95  43463  sqwvfoura  43490  sqwvfourb  43491  fouriersw  43493  etransclem23  43519  etransclem35  43531  etransclem46  43542  fmtnorec2lem  44713  fmtnorec3  44719  m1expoddALTV  44819  perfectALTVlem2  44893  ztprmneprm  45402  altgsumbc  45407  divge1b  45572  divgt1b  45573  ackval1  45746  affineid  45769  1subrec1sub  45770  rrx2vlinest  45806  line2x  45819
  Copyright terms: Public domain W3C validator