Theorem mullidd 11251

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  1c1 11128   · cmul 11132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  adddirp1d  11259  addrid  11413  mulsubfacd  11696  mulcand  11868  receu  11880  divdivdiv  11940  divcan5  11941  subrecd  12068  ltrec  12122  recp1lt1  12138  nndivtr  12285  subhalfhalf  12473  xp1d2m1eqxm1d2  12493  gtndiv  12668  ge2halflem1  13122  lincmb01cmp  13510  iccf1o  13511  ltdifltdiv  13849  modfrac  13899  negmod  13932  addmodid  13935  m1expcl2  14101  expgt1  14116  ltexp2a  14182  leexp2a  14188  binom3  14240  faclbnd  14306  faclbnd4lem4  14312  facavg  14317  bcval5  14334  cshweqrep  14837  01sqrexlem2  15260  absimle  15326  reccn2  15611  iseraltlem2  15697  iseraltlem3  15698  o1fsum  15827  abscvgcvg  15833  ackbijnn  15842  binom1p  15845  binom1dif  15847  incexclem  15850  incexc  15851  climcndslem1  15863  pwdif  15882  geomulcvg  15890  fprodsplit  15980  fallrisefac  16039  bpolysum  16067  bpolydiflem  16068  bpoly4  16073  efcllem  16091  ef01bndlem  16200  efieq1re  16215  eirrlem  16220  iddvds  16287  pwp1fsum  16408  oddpwp1fsum  16409  bitsfzolem  16451  bitsfzo  16452  rpmulgcd  16574  prmind2  16702  isprm5  16724  phiprm  16794  eulerthlem2  16799  fermltl  16801  hashgcdlem  16805  odzdvds  16813  powm2modprm  16821  modprm0  16823  pythagtriplem4  16837  4sqlem18  16980  vdwapun  16992  mulgnnass  19090  odinv  19540  odadd2  19828  pgpfaclem2  20063  abvneg  20784  pzriprnglem6  21445  pzriprnglem12  21451  nrginvrcnlem  24628  nmoid  24679  blcvx  24735  icopnfcnv  24889  reparphti  24945  reparphtiOLD  24946  pcorevlem  24975  ncvsm1  25104  ncvspi  25106  cphipval2  25191  cphipval  25193  itg11  25642  itg2mulc  25698  itg2monolem1  25701  itgcnlem  25741  iblabs  25780  dvexp  25907  dvmptdiv  25928  dvef  25934  lhop1lem  25968  dvcvx  25975  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem4  25986  dvfsum2  25991  plypow  26160  dgrcolem1  26229  vieta1lem2  26269  radcnvlem1  26372  radcnvlem2  26373  dvradcnv  26380  abelthlem6  26396  abelthlem7  26398  abelth2  26402  sinhalfpip  26451  sinhalfpim  26452  coshalfpip  26453  coshalfpim  26454  tangtx  26464  efif1olem4  26504  abslogle  26577  logdivlti  26579  advlog  26613  advlogexp  26614  logtayl  26619  cxpaddlelem  26711  cxpaddle  26712  affineequiv  26783  affineequiv2  26784  chordthmlem5  26796  dcubic2  26804  dcubic  26806  mcubic  26807  binom4  26810  dquartlem1  26811  quart1lem  26815  quart1  26816  quartlem1  26817  quart  26821  efiasin  26848  atantayl  26897  cvxcl  26945  scvxcvx  26946  lgamgulmlem5  26993  lgamcvg2  27015  lgam1  27024  wilthlem1  27028  wilthlem2  27029  basellem9  27049  fsumfldivdiaglem  27149  muinv  27153  chpub  27181  logexprlim  27186  mersenne  27188  perfectlem2  27191  dchrmullid  27213  dchrptlem1  27225  dchrsum2  27229  sumdchr2  27231  bposlem2  27246  bposlem9  27253  lgsval2lem  27268  lgsval4a  27280  lgsneg1  27283  lgsdir2lem4  27289  lgsdir  27293  lgsmulsqcoprm  27304  lgsdirnn0  27305  lgsdinn0  27306  gausslemma2dlem1a  27326  gausslemma2dlem4  27330  gausslemma2dlem7  27334  gausslemma2d  27335  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem4  27339  lgsquad2lem1  27345  2sqlem8  27387  chebbnd1lem3  27432  chpchtlim  27440  rplogsumlem1  27445  rplogsumlem2  27446  rpvmasumlem  27448  dchrmusum2  27455  dchrvmasum2lem  27457  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrisum0flblem1  27469  mulog2sumlem2  27496  vmalogdivsum2  27499  2vmadivsumlem  27501  log2sumbnd  27505  selberglem2  27507  selberg3lem1  27518  selberg4lem1  27521  pntrlog2bndlem2  27539  pntrlog2bndlem5  27542  pntpbnd1  27547  pntpbnd2  27548  pntibndlem2  27552  pntlemb  27558  pntlemr  27563  pntlemk  27567  pntlemo  27568  brbtwn2  28830  colinearalglem4  28834  ax5seglem3  28856  axbtwnid  28864  axpaschlem  28865  axeuclidlem  28887  axcontlem7  28895  axcontlem8  28896  elntg2  28910  nvm1  30592  nvpi  30594  nvmtri  30598  ipval2  30634  ipasslem1  30758  ipasslem4  30761  bcs2  31109  lnfnaddi  31970  nnmulge  32662  quad3d  32673  2exple2exp  32770  indsum  32784  indsumin  32785  ccfldsrarelvec  33658  constrfin  33726  constrremulcl  33747  constrrecl  33749  constrimcl  33750  constrmulcl  33751  constrreinvcl  33752  2sqr3minply  33760  cos9thpiminplylem2  33763  sqsscirc1  33885  eulerpartlemgs2  34358  plymulx0  34525  logdivsqrle  34628  subfacp1lem6  35153  subfaclim  35156  cvxpconn  35210  cvxsconn  35211  resconn  35214  sinccvglem  35640  fwddifn0  36128  nn0prpwlem  36286  knoppndvlem9  36484  knoppndvlem14  36489  bj-bary1lem1  37275  mblfinlem3  37629  itg2addnclem3  37643  iblabsnc  37654  iblmulc2nc  37655  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  areacirclem1  37678  bfplem2  37793  bfp  37794  rrntotbnd  37806  lcmineqlem1  41988  lcmineqlem12  41999  lcmineqlem18  42005  aks4d1p1p7  42033  aks4d1p8  42046  primrootscoprmpow  42058  posbezout  42059  aks6d1c2lem4  42086  fltnlta  42633  3cubeslem2  42655  3cubeslem3r  42657  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  pellfundex  42856  jm2.19lem3  42962  jm2.25  42970  jm2.27c  42978  jm3.1lem2  42989  flcidc  43141  reabssgn  43607  sqrtcval  43612  int-mul12d  44154  cvgdvgrat  44285  bccn1  44316  binomcxplemnotnn0  44328  fperiodmullem  45280  xralrple2  45329  fmul01lt1lem2  45562  mccllem  45574  reclimc  45630  cosknegpi  45846  dvsinax  45890  dvnxpaek  45919  dvnmul  45920  itgsinexp  45932  stoweidlem14  45991  stoweidlem26  46003  wallispilem4  46045  wallispilem5  46046  wallispi2lem1  46048  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkercncflem2  46081  fourierdlem26  46110  fourierdlem41  46125  fourierdlem42  46126  fourierdlem56  46139  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem64  46147  fourierdlem65  46148  fourierdlem95  46178  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  etransclem23  46234  etransclem35  46246  etransclem46  46257  fmtnorec2lem  47504  fmtnorec3  47510  m1expoddALTV  47610  perfectALTVlem2  47684  ztprmneprm  48270  altgsumbc  48275  divge1b  48436  divgt1b  48437  ackval1  48609  affineid  48632  1subrec1sub  48633  rrx2vlinest  48669  line2x  48682