Theorem mullidd 11231

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7402  ℂcc 11105  1c1 11108   · cmul 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-mulcom 11171  ax-mulass 11173  ax-distr 11174  ax-1rid 11177  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405

This theorem is referenced by:  adddirp1d  11239  addrid  11393  mulsubfacd  11674  mulcand  11846  receu  11858  divdivdiv  11914  divcan5  11915  subrec  12042  ltrec  12095  recp1lt1  12111  nndivtr  12258  subhalfhalf  12445  xp1d2m1eqxm1d2  12465  gtndiv  12638  lincmb01cmp  13473  iccf1o  13474  ltdifltdiv  13800  modfrac  13850  negmod  13882  addmodid  13885  m1expcl2  14052  expgt1  14067  ltexp2a  14132  leexp2a  14138  binom3  14188  faclbnd  14251  faclbnd4lem4  14257  facavg  14262  bcval5  14279  cshweqrep  14773  01sqrexlem2  15192  absimle  15258  reccn2  15543  iseraltlem2  15631  iseraltlem3  15632  o1fsum  15761  abscvgcvg  15767  ackbijnn  15776  binom1p  15779  binom1dif  15781  incexclem  15784  incexc  15785  climcndslem1  15797  pwdif  15816  geomulcvg  15824  fprodsplit  15912  fallrisefac  15971  bpolysum  15999  bpolydiflem  16000  bpoly4  16005  efcllem  16023  ef01bndlem  16130  efieq1re  16145  eirrlem  16150  iddvds  16216  pwp1fsum  16337  oddpwp1fsum  16338  bitsfzolem  16378  bitsfzo  16379  rpmulgcd  16501  prmind2  16625  isprm5  16647  phiprm  16715  eulerthlem2  16720  fermltl  16722  hashgcdlem  16726  odzdvds  16733  powm2modprm  16741  modprm0  16743  pythagtriplem4  16757  4sqlem18  16900  vdwapun  16912  mulgnnass  19032  odinv  19477  odadd2  19765  pgpfaclem2  20000  abvneg  20673  pzriprnglem6  21362  pzriprnglem12  21368  nrginvrcnlem  24552  nmoid  24603  blcvx  24658  icopnfcnv  24811  reparphti  24867  reparphtiOLD  24868  pcorevlem  24897  ncvsm1  25026  ncvspi  25028  cphipval2  25113  cphipval  25115  itg11  25564  itg2mulc  25621  itg2monolem1  25624  itgcnlem  25663  iblabs  25702  dvexp  25829  dvmptdiv  25850  dvef  25856  lhop1lem  25890  dvcvx  25897  dvfsumlem1  25904  dvfsumlem2  25905  dvfsumlem2OLD  25906  dvfsumlem4  25908  dvfsum2  25913  plypow  26082  dgrcolem1  26151  vieta1lem2  26188  radcnvlem1  26289  radcnvlem2  26290  dvradcnv  26297  abelthlem6  26313  abelthlem7  26315  abelth2  26319  sinhalfpip  26367  sinhalfpim  26368  coshalfpip  26369  coshalfpim  26370  tangtx  26380  efif1olem4  26419  abslogle  26492  logdivlti  26494  advlog  26528  advlogexp  26529  logtayl  26534  cxpaddlelem  26626  cxpaddle  26627  affineequiv  26695  affineequiv2  26696  chordthmlem5  26708  dcubic2  26716  dcubic  26718  mcubic  26719  binom4  26722  dquartlem1  26723  quart1lem  26727  quart1  26728  quartlem1  26729  quart  26733  efiasin  26760  atantayl  26809  cvxcl  26857  scvxcvx  26858  lgamgulmlem5  26905  lgamcvg2  26927  lgam1  26936  wilthlem1  26940  wilthlem2  26941  basellem9  26961  fsumfldivdiaglem  27061  muinv  27065  chpub  27093  logexprlim  27098  mersenne  27100  perfectlem2  27103  dchrmullid  27125  dchrptlem1  27137  dchrsum2  27141  sumdchr2  27143  bposlem2  27158  bposlem9  27165  lgsval2lem  27180  lgsval4a  27192  lgsneg1  27195  lgsdir2lem4  27201  lgsdir  27205  lgsmulsqcoprm  27216  lgsdirnn0  27217  lgsdinn0  27218  gausslemma2dlem1a  27238  gausslemma2dlem4  27242  gausslemma2dlem7  27246  gausslemma2d  27247  lgseisenlem1  27248  lgseisenlem2  27249  lgseisenlem4  27251  lgsquad2lem1  27257  2sqlem8  27299  chebbnd1lem3  27344  chpchtlim  27352  rplogsumlem1  27357  rplogsumlem2  27358  rpvmasumlem  27360  dchrmusum2  27367  dchrvmasum2lem  27369  dchrvmasumlem2  27371  dchrvmasumlem3  27372  dchrisum0flblem1  27381  mulog2sumlem2  27408  vmalogdivsum2  27411  2vmadivsumlem  27413  log2sumbnd  27417  selberglem2  27419  selberg3lem1  27430  selberg4lem1  27433  pntrlog2bndlem2  27451  pntrlog2bndlem5  27454  pntpbnd1  27459  pntpbnd2  27460  pntibndlem2  27464  pntlemb  27470  pntlemr  27475  pntlemk  27479  pntlemo  27480  brbtwn2  28656  colinearalglem4  28660  ax5seglem3  28682  axbtwnid  28690  axpaschlem  28691  axeuclidlem  28713  axcontlem7  28721  axcontlem8  28722  elntg2  28736  nvm1  30412  nvpi  30414  nvmtri  30418  ipval2  30454  ipasslem1  30578  ipasslem4  30581  bcs2  30929  lnfnaddi  31790  nnmulge  32457  ccfldsrarelvec  33253  sqsscirc1  33407  indsum  33538  indsumin  33539  eulerpartlemgs2  33898  plymulx0  34077  logdivsqrle  34180  subfacp1lem6  34693  subfaclim  34696  cvxpconn  34750  cvxsconn  34751  resconn  34754  sinccvglem  35174  fwddifn0  35658  nn0prpwlem  35707  knoppndvlem9  35896  knoppndvlem14  35901  bj-bary1lem1  36692  mblfinlem3  37030  itg2addnclem3  37044  iblabsnc  37055  iblmulc2nc  37056  ftc1anclem6  37069  ftc1anclem7  37070  ftc1anclem8  37071  areacirclem1  37079  bfplem2  37194  bfp  37195  rrntotbnd  37207  lcmineqlem1  41400  lcmineqlem12  41411  lcmineqlem18  41417  aks4d1p1p7  41445  aks4d1p8  41458  primrootscoprmpow  41469  posbezout  41470  fltnlta  41955  3cubeslem2  41973  3cubeslem3r  41975  irrapxlem5  42114  pellexlem2  42118  pellexlem6  42122  pellfundex  42174  jm2.19lem3  42280  jm2.25  42288  jm2.27c  42296  jm3.1lem2  42307  flcidc  42466  reabssgn  42936  sqrtcval  42941  int-mul12d  43484  cvgdvgrat  43621  bccn1  43652  binomcxplemnotnn0  43664  fperiodmullem  44558  xralrple2  44609  fmul01lt1lem2  44846  mccllem  44858  reclimc  44914  cosknegpi  45130  dvsinax  45174  dvnxpaek  45203  dvnmul  45204  itgsinexp  45216  stoweidlem14  45275  stoweidlem26  45287  wallispilem4  45329  wallispilem5  45330  wallispi2lem1  45332  wallispi2  45334  stirlinglem1  45335  stirlinglem3  45337  stirlinglem4  45338  stirlinglem5  45339  stirlinglem6  45340  stirlinglem7  45341  stirlinglem10  45344  dirkertrigeqlem2  45360  dirkertrigeqlem3  45361  dirkercncflem2  45365  fourierdlem26  45394  fourierdlem41  45409  fourierdlem42  45410  fourierdlem56  45423  fourierdlem57  45424  fourierdlem58  45425  fourierdlem62  45429  fourierdlem64  45431  fourierdlem65  45432  fourierdlem95  45462  sqwvfoura  45489  sqwvfourb  45490  fouriersw  45492  etransclem23  45518  etransclem35  45530  etransclem46  45541  fmtnorec2lem  46755  fmtnorec3  46761  m1expoddALTV  46861  perfectALTVlem2  46935  ztprmneprm  47272  altgsumbc  47277  divge1b  47441  divgt1b  47442  ackval1  47615  affineid  47638  1subrec1sub  47639  rrx2vlinest  47675  line2x  47688