Theorem mulid2d 10659

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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulid2 10640	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535  1c1 10538   · cmul 10542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulcom 10601  ax-mulass 10603  ax-distr 10604  ax-1rid 10607  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  adddirp1d  10667  addid1  10820  mulsubfacd  11101  mulcand  11273  receu  11285  divdivdiv  11341  divcan5  11342  subrec  11469  ltrec  11522  recp1lt1  11538  nndivtr  11685  subhalfhalf  11872  xp1d2m1eqxm1d2  11892  gtndiv  12060  lincmb01cmp  12882  iccf1o  12883  ltdifltdiv  13205  modfrac  13253  negmod  13285  addmodid  13288  m1expcl2  13452  expgt1  13468  ltexp2a  13531  leexp2a  13537  binom3  13586  faclbnd  13651  faclbnd4lem4  13657  facavg  13662  bcval5  13679  cshweqrep  14183  sqrlem2  14603  absimle  14669  reccn2  14953  iseraltlem2  15039  iseraltlem3  15040  o1fsum  15168  abscvgcvg  15174  ackbijnn  15183  binom1p  15186  binom1dif  15188  incexclem  15191  incexc  15192  climcndslem1  15204  pwdif  15223  geomulcvg  15232  fprodsplit  15320  fallrisefac  15379  bpolysum  15407  bpolydiflem  15408  bpoly4  15413  efcllem  15431  ef01bndlem  15537  efieq1re  15552  eirrlem  15557  iddvds  15623  pwp1fsum  15742  oddpwp1fsum  15743  bitsfzolem  15783  bitsfzo  15784  rpmulgcd  15906  prmind2  16029  isprm5  16051  phiprm  16114  eulerthlem2  16119  fermltl  16121  hashgcdlem  16125  odzdvds  16132  powm2modprm  16140  modprm0  16142  pythagtriplem4  16156  4sqlem18  16298  vdwapun  16310  mulgnnass  18262  odinv  18688  odadd2  18969  pgpfaclem2  19204  abvneg  19605  nrginvrcnlem  23300  nmoid  23351  blcvx  23406  icopnfcnv  23546  reparphti  23601  pcorevlem  23630  ncvsm1  23758  ncvspi  23760  cphipval2  23844  cphipval  23846  itg11  24292  itg2mulc  24348  itg2monolem1  24351  itgcnlem  24390  iblabs  24429  dvexp  24550  dvmptdiv  24571  dvef  24577  lhop1lem  24610  dvcvx  24617  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem4  24626  dvfsum2  24631  plypow  24795  dgrcolem1  24863  vieta1lem2  24900  radcnvlem1  25001  radcnvlem2  25002  dvradcnv  25009  abelthlem6  25024  abelthlem7  25026  abelth2  25030  sinhalfpip  25078  sinhalfpim  25079  coshalfpip  25080  coshalfpim  25081  tangtx  25091  efif1olem4  25129  abslogle  25201  logdivlti  25203  advlog  25237  advlogexp  25238  logtayl  25243  cxpaddlelem  25332  cxpaddle  25333  affineequiv  25401  affineequiv2  25402  chordthmlem5  25414  dcubic2  25422  dcubic  25424  mcubic  25425  binom4  25428  dquartlem1  25429  quart1lem  25433  quart1  25434  quartlem1  25435  quart  25439  efiasin  25466  atantayl  25515  cvxcl  25562  scvxcvx  25563  lgamgulmlem5  25610  lgamcvg2  25632  lgam1  25641  wilthlem1  25645  wilthlem2  25646  basellem9  25666  fsumfldivdiaglem  25766  muinv  25770  chpub  25796  logexprlim  25801  mersenne  25803  perfectlem2  25806  dchrmulid2  25828  dchrptlem1  25840  dchrsum2  25844  sumdchr2  25846  bposlem2  25861  bposlem9  25868  lgsval2lem  25883  lgsval4a  25895  lgsneg1  25898  lgsdir2lem4  25904  lgsdir  25908  lgsmulsqcoprm  25919  lgsdirnn0  25920  lgsdinn0  25921  gausslemma2dlem1a  25941  gausslemma2dlem4  25945  gausslemma2dlem7  25949  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem4  25954  lgsquad2lem1  25960  2sqlem8  26002  chebbnd1lem3  26047  chpchtlim  26055  rplogsumlem1  26060  rplogsumlem2  26061  rpvmasumlem  26063  dchrmusum2  26070  dchrvmasum2lem  26072  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrisum0flblem1  26084  mulog2sumlem2  26111  vmalogdivsum2  26114  2vmadivsumlem  26116  log2sumbnd  26120  selberglem2  26122  selberg3lem1  26133  selberg4lem1  26136  pntrlog2bndlem2  26154  pntrlog2bndlem5  26157  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2  26167  pntlemb  26173  pntlemr  26178  pntlemk  26182  pntlemo  26183  brbtwn2  26691  colinearalglem4  26695  ax5seglem3  26717  axbtwnid  26725  axpaschlem  26726  axeuclidlem  26748  axcontlem7  26756  axcontlem8  26757  elntg2  26771  nvm1  28442  nvpi  28444  nvmtri  28448  ipval2  28484  ipasslem1  28608  ipasslem4  28611  bcs2  28959  lnfnaddi  29820  nnmulge  30474  ccfldsrarelvec  31056  sqsscirc1  31151  indsum  31280  indsumin  31281  eulerpartlemgs2  31638  plymulx0  31817  logdivsqrle  31921  subfacp1lem6  32432  subfaclim  32435  cvxpconn  32489  cvxsconn  32490  resconn  32493  sinccvglem  32915  fwddifn0  33625  nn0prpwlem  33670  knoppndvlem9  33859  knoppndvlem14  33864  bj-bary1lem1  34595  mblfinlem3  34946  itg2addnclem3  34960  iblabsnc  34971  iblmulc2nc  34972  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  areacirclem1  34997  bfplem2  35116  bfp  35117  rrntotbnd  35129  fltnlta  39324  3cubeslem2  39331  3cubeslem3r  39333  irrapxlem5  39472  pellexlem2  39476  pellexlem6  39480  pellfundex  39532  jm2.19lem3  39637  jm2.25  39645  jm2.27c  39653  jm3.1lem2  39664  flcidc  39823  int-mul12d  40585  cvgdvgrat  40694  bccn1  40725  binomcxplemnotnn0  40737  fperiodmullem  41619  xralrple2  41671  fmul01lt1lem2  41915  mccllem  41927  reclimc  41983  cosknegpi  42199  dvsinax  42246  dvnxpaek  42276  dvnmul  42277  itgsinexp  42289  stoweidlem14  42348  stoweidlem26  42360  wallispilem4  42402  wallispilem5  42403  wallispi2lem1  42405  wallispi2  42407  stirlinglem1  42408  stirlinglem3  42410  stirlinglem4  42411  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkercncflem2  42438  fourierdlem26  42467  fourierdlem41  42482  fourierdlem42  42483  fourierdlem56  42496  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem64  42504  fourierdlem65  42505  fourierdlem95  42535  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  etransclem23  42591  etransclem35  42603  etransclem46  42614  fmtnorec2lem  43753  fmtnorec3  43759  m1expoddALTV  43862  perfectALTVlem2  43936  ztprmneprm  44444  altgsumbc  44449  divge1b  44616  divgt1b  44617  affineid  44740  1subrec1sub  44741  rrx2vlinest  44777  line2x  44790