Theorem mulid2d 10661

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537  1c1 10540   · cmul 10544

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 2795  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-mulcom 10603  ax-mulass 10605  ax-distr 10606  ax-1rid 10609  ax-cnre 10612

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161

This theorem is referenced by:  adddirp1d  10669  addid1  10822  mulsubfacd  11103  mulcand  11275  receu  11287  divdivdiv  11343  divcan5  11344  subrec  11471  ltrec  11524  recp1lt1  11540  nndivtr  11687  subhalfhalf  11874  xp1d2m1eqxm1d2  11894  gtndiv  12062  lincmb01cmp  12884  iccf1o  12885  ltdifltdiv  13207  modfrac  13255  negmod  13287  addmodid  13290  m1expcl2  13454  expgt1  13470  ltexp2a  13533  leexp2a  13539  binom3  13588  faclbnd  13653  faclbnd4lem4  13659  facavg  13664  bcval5  13681  cshweqrep  14185  sqrlem2  14605  absimle  14671  reccn2  14955  iseraltlem2  15041  iseraltlem3  15042  o1fsum  15170  abscvgcvg  15176  ackbijnn  15185  binom1p  15188  binom1dif  15190  incexclem  15193  incexc  15194  climcndslem1  15206  pwdif  15225  geomulcvg  15234  fprodsplit  15322  fallrisefac  15381  bpolysum  15409  bpolydiflem  15410  bpoly4  15415  efcllem  15433  ef01bndlem  15539  efieq1re  15554  eirrlem  15559  iddvds  15625  pwp1fsum  15744  oddpwp1fsum  15745  bitsfzolem  15785  bitsfzo  15786  rpmulgcd  15908  prmind2  16031  isprm5  16053  phiprm  16116  eulerthlem2  16121  fermltl  16123  hashgcdlem  16127  odzdvds  16134  powm2modprm  16142  modprm0  16144  pythagtriplem4  16158  4sqlem18  16300  vdwapun  16312  mulgnnass  18264  odinv  18690  odadd2  18971  pgpfaclem2  19206  abvneg  19607  nrginvrcnlem  23302  nmoid  23353  blcvx  23408  icopnfcnv  23548  reparphti  23603  pcorevlem  23632  ncvsm1  23760  ncvspi  23762  cphipval2  23846  cphipval  23848  itg11  24294  itg2mulc  24350  itg2monolem1  24353  itgcnlem  24392  iblabs  24431  dvexp  24552  dvmptdiv  24573  dvef  24579  lhop1lem  24612  dvcvx  24619  dvfsumlem1  24625  dvfsumlem2  24626  dvfsumlem4  24628  dvfsum2  24633  plypow  24797  dgrcolem1  24865  vieta1lem2  24902  radcnvlem1  25003  radcnvlem2  25004  dvradcnv  25011  abelthlem6  25026  abelthlem7  25028  abelth2  25032  sinhalfpip  25080  sinhalfpim  25081  coshalfpip  25082  coshalfpim  25083  tangtx  25093  efif1olem4  25131  abslogle  25203  logdivlti  25205  advlog  25239  advlogexp  25240  logtayl  25245  cxpaddlelem  25334  cxpaddle  25335  affineequiv  25403  affineequiv2  25404  chordthmlem5  25416  dcubic2  25424  dcubic  25426  mcubic  25427  binom4  25430  dquartlem1  25431  quart1lem  25435  quart1  25436  quartlem1  25437  quart  25441  efiasin  25468  atantayl  25517  cvxcl  25564  scvxcvx  25565  lgamgulmlem5  25612  lgamcvg2  25634  lgam1  25643  wilthlem1  25647  wilthlem2  25648  basellem9  25668  fsumfldivdiaglem  25768  muinv  25772  chpub  25798  logexprlim  25803  mersenne  25805  perfectlem2  25808  dchrmulid2  25830  dchrptlem1  25842  dchrsum2  25846  sumdchr2  25848  bposlem2  25863  bposlem9  25870  lgsval2lem  25885  lgsval4a  25897  lgsneg1  25900  lgsdir2lem4  25906  lgsdir  25910  lgsmulsqcoprm  25921  lgsdirnn0  25922  lgsdinn0  25923  gausslemma2dlem1a  25943  gausslemma2dlem4  25947  gausslemma2dlem7  25951  gausslemma2d  25952  lgseisenlem1  25953  lgseisenlem2  25954  lgseisenlem4  25956  lgsquad2lem1  25962  2sqlem8  26004  chebbnd1lem3  26049  chpchtlim  26057  rplogsumlem1  26062  rplogsumlem2  26063  rpvmasumlem  26065  dchrmusum2  26072  dchrvmasum2lem  26074  dchrvmasumlem2  26076  dchrvmasumlem3  26077  dchrisum0flblem1  26086  mulog2sumlem2  26113  vmalogdivsum2  26116  2vmadivsumlem  26118  log2sumbnd  26122  selberglem2  26124  selberg3lem1  26135  selberg4lem1  26138  pntrlog2bndlem2  26156  pntrlog2bndlem5  26159  pntpbnd1  26164  pntpbnd2  26165  pntibndlem2  26169  pntlemb  26175  pntlemr  26180  pntlemk  26184  pntlemo  26185  brbtwn2  26693  colinearalglem4  26697  ax5seglem3  26719  axbtwnid  26727  axpaschlem  26728  axeuclidlem  26750  axcontlem7  26758  axcontlem8  26759  elntg2  26773  nvm1  28444  nvpi  28446  nvmtri  28450  ipval2  28486  ipasslem1  28610  ipasslem4  28613  bcs2  28961  lnfnaddi  29822  nnmulge  30476  ccfldsrarelvec  31058  sqsscirc1  31153  indsum  31282  indsumin  31283  eulerpartlemgs2  31640  plymulx0  31819  logdivsqrle  31923  subfacp1lem6  32434  subfaclim  32437  cvxpconn  32491  cvxsconn  32492  resconn  32495  sinccvglem  32917  fwddifn0  33627  nn0prpwlem  33672  knoppndvlem9  33861  knoppndvlem14  33866  bj-bary1lem1  34594  mblfinlem3  34933  itg2addnclem3  34947  iblabsnc  34958  iblmulc2nc  34959  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anclem8  34976  areacirclem1  34984  bfplem2  35103  bfp  35104  rrntotbnd  35116  fltnlta  39282  3cubeslem2  39289  3cubeslem3r  39291  irrapxlem5  39430  pellexlem2  39434  pellexlem6  39438  pellfundex  39490  jm2.19lem3  39595  jm2.25  39603  jm2.27c  39611  jm3.1lem2  39622  flcidc  39781  int-mul12d  40543  cvgdvgrat  40652  bccn1  40683  binomcxplemnotnn0  40695  fperiodmullem  41577  xralrple2  41629  fmul01lt1lem2  41873  mccllem  41885  reclimc  41941  cosknegpi  42157  dvsinax  42204  dvnxpaek  42234  dvnmul  42235  itgsinexp  42247  stoweidlem14  42306  stoweidlem26  42318  wallispilem4  42360  wallispilem5  42361  wallispi2lem1  42363  wallispi2  42365  stirlinglem1  42366  stirlinglem3  42368  stirlinglem4  42369  stirlinglem5  42370  stirlinglem6  42371  stirlinglem7  42372  stirlinglem10  42375  dirkertrigeqlem2  42391  dirkertrigeqlem3  42392  dirkercncflem2  42396  fourierdlem26  42425  fourierdlem41  42440  fourierdlem42  42441  fourierdlem56  42454  fourierdlem57  42455  fourierdlem58  42456  fourierdlem62  42460  fourierdlem64  42462  fourierdlem65  42463  fourierdlem95  42493  sqwvfoura  42520  sqwvfourb  42521  fouriersw  42523  etransclem23  42549  etransclem35  42561  etransclem46  42572  fmtnorec2lem  43711  fmtnorec3  43717  m1expoddALTV  43820  perfectALTVlem2  43894  ztprmneprm  44402  altgsumbc  44407  divge1b  44574  divgt1b  44575  affineid  44698  1subrec1sub  44699  rrx2vlinest  44735  line2x  44748