Theorem mullidd 11327

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mullidd	⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Proof of Theorem mullidd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mullid 11307	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198  1c1 11201   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  adddirp1d  11335  addrid  11490  mulsubfacd  11777  mulcand  11949  receu  11961  divdivdiv  12018  divcan5  12019  subrecd  12146  ltrec  12199  recp1lt1  12215  nndivtr  12385  subhalfhalf  12580  xp1d2m1eqxm1d2  12600  gtndiv  12776  ge2halflem1  13237  lincmb01cmp  13626  iccf1o  13627  ltdifltdiv  13974  modfrac  14024  negmod  14059  addmodid  14062  m1expcl2  14228  expgt1  14243  ltexp2a  14309  leexp2a  14315  binom3  14368  faclbnd  14434  faclbnd4lem4  14440  facavg  14445  bcval5  14462  cshweqrep  14972  01sqrexlem2  15410  absimle  15476  reccn2  15764  iseraltlem2  15850  iseraltlem3  15851  o1fsum  15980  abscvgcvg  15986  indsum  15995  ackbijnn  15997  binom1p  16000  binom1dif  16002  incexclem  16005  incexc  16006  climcndslem1  16018  pwdif  16037  geomulcvg  16045  fprodsplit  16133  fallrisefac  16192  bpolysum  16219  bpolydiflem  16220  bpoly4  16225  efcllem  16243  ef01bndlem  16352  efieq1re  16367  eirrlem  16372  iddvds  16439  pwp1fsum  16561  oddpwp1fsum  16562  bitsfzolem  16604  bitsfzo  16605  rpmulgcd  16731  prmind2  16860  isprm5  16883  phiprm  16954  eulerthlem2  16959  fermltl  16961  hashgcdlem  16965  odzdvds  16973  powm2modprm  16981  modprm0  16983  pythagtriplem4  16997  4sqlem18  17140  vdwapun  17152  mulgnnass  19319  odinv  19775  odadd2  20063  pgpfaclem2  20298  abvneg  21083  pzriprnglem6  21792  pzriprnglem12  21798  nrginvrcnlem  25010  nmoid  25061  blcvx  25117  icopnfcnv  25263  reparphti  25318  pcorevlem  25347  ncvsm1  25475  ncvspi  25477  cphipval2  25562  cphipval  25564  itg11  26012  itg2mulc  26068  itg2monolem1  26071  itgcnlem  26110  iblabs  26149  dvexp  26273  dvmptdiv  26294  dvef  26300  lhop1lem  26333  dvcvx  26340  dvfsumlem1  26346  dvfsumlem2  26347  dvfsumlem4  26349  dvfsum2  26354  plypow  26523  dgrcolem1  26592  plyn0mulidp  26602  vieta1lem2  26634  radcnvlem1  26740  radcnvlem2  26741  dvradcnv  26748  abelthlem6  26763  abelthlem7  26765  abelth2  26769  sinhalfpip  26821  sinhalfpim  26822  coshalfpip  26823  coshalfpim  26824  tangtx  26834  efif1olem4  26873  abslogle  26946  logdivlti  26948  advlog  26982  advlogexp  26983  logtayl  26988  cxpaddlelem  27079  cxpaddle  27080  affineequiv  27151  affineequiv2  27152  chordthmlem5  27164  dcubic2  27172  dcubic  27174  mcubic  27175  binom4  27178  dquartlem1  27179  quart1lem  27183  quart1  27184  quartlem1  27185  quart  27189  efiasin  27216  atantayl  27265  cvxcl  27312  scvxcvx  27313  lgamgulmlem5  27360  lgamcvg2  27382  lgam1  27391  wilthlem1  27395  wilthlem2  27396  basellem9  27416  fsumfldivdiaglem  27516  muinv  27520  chpub  27547  logexprlim  27552  mersenne  27554  perfectlem2  27557  dchrmullid  27579  dchrptlem1  27591  dchrsum2  27595  sumdchr2  27597  bposlem2  27612  bposlem9  27619  lgsval2lem  27634  lgsval4a  27646  lgsneg1  27649  lgsdir2lem4  27655  lgsdir  27659  lgsmulsqcoprm  27670  lgsdirnn0  27671  lgsdinn0  27672  gausslemma2dlem1a  27692  gausslemma2dlem4  27696  gausslemma2dlem7  27700  gausslemma2d  27701  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem4  27705  lgsquad2lem1  27711  2sqlem8  27753  chebbnd1lem3  27798  chpchtlim  27806  rplogsumlem1  27811  rplogsumlem2  27812  rpvmasumlem  27814  dchrmusum2  27821  dchrvmasum2lem  27823  dchrvmasumlem2  27825  dchrvmasumlem3  27826  dchrisum0flblem1  27835  mulog2sumlem2  27862  vmalogdivsum2  27865  2vmadivsumlem  27867  log2sumbnd  27871  selberglem2  27873  selberg3lem1  27884  selberg4lem1  27887  pntrlog2bndlem2  27905  pntrlog2bndlem5  27908  pntpbnd1  27913  pntpbnd2  27914  pntibndlem2  27918  pntlemb  27924  pntlemr  27929  pntlemk  27933  pntlemo  27934  brbtwn2  29483  colinearalglem4  29487  ax5seglem3  29509  axbtwnid  29517  axpaschlem  29518  axeuclidlem  29540  axcontlem7  29548  axcontlem8  29549  elntg2  29563  nvm1  31267  nvpi  31269  nvmtri  31273  ipval2  31309  ipasslem1  31433  ipasslem4  31436  bcs2  31784  lnfnaddi  32645  nnmulge  33373  quad3d  33383  2exple2exp  33467  indsumin  33470  ccfldsrarelvec  34345  constrfin  34420  constrremulcl  34441  constrrecl  34443  constrimcl  34444  constrmulcl  34445  constrreinvcl  34446  2sqr3minply  34454  cos9thpiminplylem2  34457  sqsscirc1  34582  eulerpartlemgs2  35054  logdivsqrle  35321  subfacp1lem6  35992  subfaclim  35995  cvxpconn  36049  cvxsconn  36050  resconn  36053  sinccvglem  36479  fwddifn0  36971  nn0prpwlem  37152  knoppndvlem9  37428  knoppndvlem14  37433  bj-bary1lem1  38275  mblfinlem3  38620  itg2addnclem3  38634  iblabsnc  38645  iblmulc2nc  38646  ftc1anclem6  38659  ftc1anclem7  38660  ftc1anclem8  38661  areacirclem1  38669  bfplem2  38800  bfp  38801  rrntotbnd  38813  lcmineqlem1  43122  lcmineqlem12  43133  lcmineqlem18  43139  aks4d1p1p7  43167  aks4d1p8  43180  primrootscoprmpow  43192  posbezout  43193  aks6d1c2lem4  43220  3rdpwhole  43392  fltnlta  43717  3cubeslem2  43738  3cubeslem3r  43740  irrapxlem5  43876  pellexlem2  43880  pellexlem6  43884  pellfundex  43936  jm2.19lem3  44041  jm2.25  44049  jm2.27c  44057  jm3.1lem2  44068  flcidc  44215  reabssgn  44679  sqrtcval  44684  int-mul12d  45226  cvgdvgrat  45340  bccn1  45371  binomcxplemnotnn0  45383  fperiodmullem  46362  xralrple2  46409  fmul01lt1lem2  46640  mccllem  46652  reclimc  46706  cosknegpi  46922  dvsinax  46966  dvnxpaek  46995  dvnmul  46996  itgsinexp  47008  stoweidlem14  47067  stoweidlem26  47079  wallispilem4  47121  wallispilem5  47122  wallispi2lem1  47124  wallispi2  47126  stirlinglem1  47127  stirlinglem3  47129  stirlinglem4  47130  stirlinglem5  47131  stirlinglem6  47132  stirlinglem7  47133  stirlinglem10  47136  dirkertrigeqlem2  47152  dirkertrigeqlem3  47153  dirkercncflem2  47157  fourierdlem26  47186  fourierdlem41  47201  fourierdlem42  47202  fourierdlem56  47215  fourierdlem57  47216  fourierdlem58  47217  fourierdlem62  47221  fourierdlem64  47223  fourierdlem65  47224  fourierdlem95  47254  sqwvfoura  47281  sqwvfourb  47282  fouriersw  47284  etransclem23  47310  etransclem35  47322  etransclem46  47333  sin5tlem1  47962  sin5tlem2  47963  fmtnorec2lem  48670  fmtnorec3  48676  m1expoddALTV  48789  perfectALTVlem2  48863  ztprmneprm  49502  altgsumbc  49507  divge1b  49667  divgt1b  49668  ackval1  49836  affineid  49859  1subrec1sub  49860  rrx2vlinest  49896  line2x  49909  dvsec  50899  dvcsc  50900