Theorem mulid2d 10395

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 10375	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2106  (class class class)co 6922  ℂcc 10270  1c1 10273   · cmul 10277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-mulcl 10334  ax-mulcom 10336  ax-mulass 10338  ax-distr 10339  ax-1rid 10342  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925

This theorem is referenced by:  adddirp1d  10403  addid1  10556  mulsubfacd  10836  mulcand  11008  receu  11020  divdivdiv  11076  divcan5  11077  subrec  11204  ltrec  11259  recp1lt1  11275  nndivtr  11422  subhalfhalf  11616  xp1d2m1eqxm1d2  11636  gtndiv  11806  lincmb01cmp  12632  iccf1o  12633  ltdifltdiv  12954  modfrac  13002  negmod  13034  addmodid  13037  m1expcl2  13200  expgt1  13216  ltexp2a  13230  leexp2a  13234  binom3  13304  faclbnd  13395  faclbnd4lem4  13401  facavg  13406  bcval5  13423  cshweqrep  13972  sqrlem2  14391  absimle  14456  reccn2  14735  iseraltlem2  14821  iseraltlem3  14822  o1fsum  14949  abscvgcvg  14955  ackbijnn  14964  binom1p  14967  binom1dif  14969  incexclem  14972  incexc  14973  climcndslem1  14985  geomulcvg  15011  fprodsplit  15099  fallrisefac  15158  bpolysum  15186  bpolydiflem  15187  bpoly4  15192  efcllem  15210  ef01bndlem  15316  efieq1re  15331  eirrlem  15336  iddvds  15402  pwp1fsum  15521  oddpwp1fsum  15522  bitsfzolem  15562  bitsfzo  15563  rpmulgcd  15681  prmind2  15803  isprm5  15823  phiprm  15886  eulerthlem2  15891  fermltl  15893  hashgcdlem  15897  odzdvds  15904  powm2modprm  15912  modprm0  15914  pythagtriplem4  15928  pcexp  15968  4sqlem18  16070  vdwapun  16082  mulgnnass  17961  odinv  18362  odadd2  18638  pgpfaclem2  18868  abvneg  19226  nrginvrcnlem  22903  nmoid  22954  blcvx  23009  icopnfcnv  23149  reparphti  23204  pcorevlem  23233  ncvsm1  23361  ncvspi  23363  cphipval2  23447  cphipval  23449  itg11  23895  itg2mulc  23951  itg2monolem1  23954  itgcnlem  23993  iblabs  24032  dvexp  24153  dvmptdiv  24174  dvef  24180  lhop1lem  24213  dvcvx  24220  dvfsumlem1  24226  dvfsumlem2  24227  dvfsumlem4  24229  dvfsum2  24234  plypow  24398  dgrcolem1  24466  vieta1lem2  24503  radcnvlem1  24604  radcnvlem2  24605  dvradcnv  24612  abelthlem2  24623  abelthlem6  24627  abelthlem7  24629  abelth2  24633  sinhalfpip  24682  sinhalfpim  24683  coshalfpip  24684  coshalfpim  24685  tangtx  24695  efif1olem4  24729  abslogle  24801  logdivlti  24803  advlog  24837  advlogexp  24838  logtayl  24843  cxpaddlelem  24932  cxpaddle  24933  affineequiv  25001  affineequiv2  25002  chordthmlem5  25014  dcubic2  25022  dcubic  25024  mcubic  25025  binom4  25028  dquartlem1  25029  quart1lem  25033  quart1  25034  quartlem1  25035  quart  25039  efiasin  25066  atantayl  25115  cvxcl  25163  scvxcvx  25164  lgamgulmlem5  25211  lgamcvg2  25233  lgam1  25242  wilthlem1  25246  wilthlem2  25247  basellem9  25267  fsumfldivdiaglem  25367  muinv  25371  chpub  25397  logexprlim  25402  mersenne  25404  perfectlem2  25407  dchrmulid2  25429  dchrptlem1  25441  dchrsum2  25445  sumdchr2  25447  bposlem2  25462  bposlem9  25469  lgsval2lem  25484  lgsval4a  25496  lgsneg1  25499  lgsdir2lem4  25505  lgsdir  25509  lgsmulsqcoprm  25520  lgsdirnn0  25521  lgsdinn0  25522  gausslemma2dlem1a  25542  gausslemma2dlem4  25546  gausslemma2dlem7  25550  gausslemma2d  25551  lgseisenlem1  25552  lgseisenlem2  25553  lgseisenlem4  25555  lgsquad2lem1  25561  2sqlem8  25603  chebbnd1lem3  25612  chpchtlim  25620  rplogsumlem1  25625  rplogsumlem2  25626  rpvmasumlem  25628  dchrmusum2  25635  dchrvmasum2lem  25637  dchrvmasumlem2  25639  dchrvmasumlem3  25640  dchrisum0flblem1  25649  mulog2sumlem2  25676  vmalogdivsum2  25679  2vmadivsumlem  25681  log2sumbnd  25685  selberglem2  25687  chpdifbndlem1  25694  selberg3lem1  25698  selberg4lem1  25701  pntrlog2bndlem2  25719  pntrlog2bndlem5  25722  pntpbnd1  25727  pntpbnd2  25728  pntibndlem2  25732  pntlemb  25738  pntlemr  25743  pntlemk  25747  pntlemo  25748  brbtwn2  26254  colinearalglem4  26258  ax5seglem3  26280  axbtwnid  26288  axpaschlem  26289  axeuclidlem  26311  axcontlem7  26319  axcontlem8  26320  elntg2  26334  nvm1  28106  nvpi  28108  nvmtri  28112  ipval2  28148  ipasslem1  28272  ipasslem4  28275  bcs2  28625  lnfnaddi  29488  nnmulge  30094  sqsscirc1  30566  indsum  30695  indsumin  30696  eulerpartlemgs2  31054  plymulx0  31238  logdivsqrle  31344  subfacp1lem6  31780  subfaclim  31783  cvxpconn  31837  cvxsconn  31838  resconn  31841  sinccvglem  32177  fwddifn0  32874  nn0prpwlem  32919  knoppndvlem9  33107  knoppndvlem14  33112  bj-bary1lem1  33773  mblfinlem3  34068  itg2addnclem3  34082  iblabsnc  34093  iblmulc2nc  34094  ftc1anclem6  34109  ftc1anclem7  34110  ftc1anclem8  34111  areacirclem1  34119  bfplem2  34240  bfp  34241  rrntotbnd  34253  irrapxlem5  38342  pellexlem2  38346  pellexlem6  38350  pellfundex  38402  jm2.19lem3  38509  jm2.25  38517  jm2.27c  38525  jm3.1lem2  38536  flcidc  38695  int-mul12d  39434  cvgdvgrat  39460  bccn1  39491  binomcxplemnotnn0  39503  fperiodmullem  40418  xralrple2  40470  fmul01lt1lem2  40717  mccllem  40729  reclimc  40785  cosknegpi  41000  dvsinax  41047  dvnxpaek  41077  dvnmul  41078  itgsinexp  41090  stoweidlem14  41150  stoweidlem26  41162  wallispilem4  41204  wallispilem5  41205  wallispi2lem1  41207  wallispi2  41209  stirlinglem1  41210  stirlinglem3  41212  stirlinglem4  41213  stirlinglem5  41214  stirlinglem6  41215  stirlinglem7  41216  stirlinglem10  41219  dirkertrigeqlem2  41235  dirkertrigeqlem3  41236  dirkercncflem2  41240  fourierdlem26  41269  fourierdlem41  41284  fourierdlem42  41285  fourierdlem56  41298  fourierdlem57  41299  fourierdlem58  41300  fourierdlem62  41304  fourierdlem64  41306  fourierdlem65  41307  fourierdlem95  41337  sqwvfoura  41364  sqwvfourb  41365  fouriersw  41367  etransclem23  41393  etransclem35  41405  etransclem46  41416  fmtnorec2lem  42467  fmtnorec3  42473  pwdif  42514  m1expoddALTV  42578  perfectALTVlem2  42648  ztprmneprm  43132  altgsumbc  43137  divge1b  43309  divgt1b  43310  affineid  43432  1subrec1sub  43433  rrx2vlinest  43469  line2x  43482