Theorem mullidd 11122

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996  1c1 10999   · cmul 11003

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-mulcl 11060  ax-mulcom 11062  ax-mulass 11064  ax-distr 11065  ax-1rid 11068  ax-cnre 11071

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344

This theorem is referenced by:  adddirp1d  11130  addrid  11285  mulsubfacd  11570  mulcand  11742  receu  11754  divdivdiv  11814  divcan5  11815  subrecd  11942  ltrec  11996  recp1lt1  12012  nndivtr  12164  subhalfhalf  12347  xp1d2m1eqxm1d2  12367  gtndiv  12542  ge2halflem1  12999  lincmb01cmp  13387  iccf1o  13388  ltdifltdiv  13730  modfrac  13780  negmod  13815  addmodid  13818  m1expcl2  13984  expgt1  13999  ltexp2a  14065  leexp2a  14071  binom3  14123  faclbnd  14189  faclbnd4lem4  14195  facavg  14200  bcval5  14217  cshweqrep  14720  01sqrexlem2  15142  absimle  15208  reccn2  15496  iseraltlem2  15582  iseraltlem3  15583  o1fsum  15712  abscvgcvg  15718  ackbijnn  15727  binom1p  15730  binom1dif  15732  incexclem  15735  incexc  15736  climcndslem1  15748  pwdif  15767  geomulcvg  15775  fprodsplit  15865  fallrisefac  15924  bpolysum  15952  bpolydiflem  15953  bpoly4  15958  efcllem  15976  ef01bndlem  16085  efieq1re  16100  eirrlem  16105  iddvds  16172  pwp1fsum  16294  oddpwp1fsum  16295  bitsfzolem  16337  bitsfzo  16338  rpmulgcd  16460  prmind2  16588  isprm5  16610  phiprm  16680  eulerthlem2  16685  fermltl  16687  hashgcdlem  16691  odzdvds  16699  powm2modprm  16707  modprm0  16709  pythagtriplem4  16723  4sqlem18  16866  vdwapun  16878  mulgnnass  19014  odinv  19466  odadd2  19754  pgpfaclem2  19989  abvneg  20734  pzriprnglem6  21416  pzriprnglem12  21422  nrginvrcnlem  24599  nmoid  24650  blcvx  24706  icopnfcnv  24860  reparphti  24916  reparphtiOLD  24917  pcorevlem  24946  ncvsm1  25074  ncvspi  25076  cphipval2  25161  cphipval  25163  itg11  25612  itg2mulc  25668  itg2monolem1  25671  itgcnlem  25711  iblabs  25750  dvexp  25877  dvmptdiv  25898  dvef  25904  lhop1lem  25938  dvcvx  25945  dvfsumlem1  25952  dvfsumlem2  25953  dvfsumlem2OLD  25954  dvfsumlem4  25956  dvfsum2  25961  plypow  26130  dgrcolem1  26199  vieta1lem2  26239  radcnvlem1  26342  radcnvlem2  26343  dvradcnv  26350  abelthlem6  26366  abelthlem7  26368  abelth2  26372  sinhalfpip  26421  sinhalfpim  26422  coshalfpip  26423  coshalfpim  26424  tangtx  26434  efif1olem4  26474  abslogle  26547  logdivlti  26549  advlog  26583  advlogexp  26584  logtayl  26589  cxpaddlelem  26681  cxpaddle  26682  affineequiv  26753  affineequiv2  26754  chordthmlem5  26766  dcubic2  26774  dcubic  26776  mcubic  26777  binom4  26780  dquartlem1  26781  quart1lem  26785  quart1  26786  quartlem1  26787  quart  26791  efiasin  26818  atantayl  26867  cvxcl  26915  scvxcvx  26916  lgamgulmlem5  26963  lgamcvg2  26985  lgam1  26994  wilthlem1  26998  wilthlem2  26999  basellem9  27019  fsumfldivdiaglem  27119  muinv  27123  chpub  27151  logexprlim  27156  mersenne  27158  perfectlem2  27161  dchrmullid  27183  dchrptlem1  27195  dchrsum2  27199  sumdchr2  27201  bposlem2  27216  bposlem9  27223  lgsval2lem  27238  lgsval4a  27250  lgsneg1  27253  lgsdir2lem4  27259  lgsdir  27263  lgsmulsqcoprm  27274  lgsdirnn0  27275  lgsdinn0  27276  gausslemma2dlem1a  27296  gausslemma2dlem4  27300  gausslemma2dlem7  27304  gausslemma2d  27305  lgseisenlem1  27306  lgseisenlem2  27307  lgseisenlem4  27309  lgsquad2lem1  27315  2sqlem8  27357  chebbnd1lem3  27402  chpchtlim  27410  rplogsumlem1  27415  rplogsumlem2  27416  rpvmasumlem  27418  dchrmusum2  27425  dchrvmasum2lem  27427  dchrvmasumlem2  27429  dchrvmasumlem3  27430  dchrisum0flblem1  27439  mulog2sumlem2  27466  vmalogdivsum2  27469  2vmadivsumlem  27471  log2sumbnd  27475  selberglem2  27477  selberg3lem1  27488  selberg4lem1  27491  pntrlog2bndlem2  27509  pntrlog2bndlem5  27512  pntpbnd1  27517  pntpbnd2  27518  pntibndlem2  27522  pntlemb  27528  pntlemr  27533  pntlemk  27537  pntlemo  27538  brbtwn2  28876  colinearalglem4  28880  ax5seglem3  28902  axbtwnid  28910  axpaschlem  28911  axeuclidlem  28933  axcontlem7  28941  axcontlem8  28942  elntg2  28956  nvm1  30635  nvpi  30637  nvmtri  30641  ipval2  30677  ipasslem1  30801  ipasslem4  30804  bcs2  31152  lnfnaddi  32013  nnmulge  32712  quad3d  32723  2exple2exp  32818  indsum  32832  indsumin  32833  ccfldsrarelvec  33674  constrfin  33749  constrremulcl  33770  constrrecl  33772  constrimcl  33773  constrmulcl  33774  constrreinvcl  33775  2sqr3minply  33783  cos9thpiminplylem2  33786  sqsscirc1  33911  eulerpartlemgs2  34383  plymulx0  34550  logdivsqrle  34653  subfacp1lem6  35197  subfaclim  35200  cvxpconn  35254  cvxsconn  35255  resconn  35258  sinccvglem  35684  fwddifn0  36177  nn0prpwlem  36335  knoppndvlem9  36533  knoppndvlem14  36538  bj-bary1lem1  37324  mblfinlem3  37678  itg2addnclem3  37692  iblabsnc  37703  iblmulc2nc  37704  ftc1anclem6  37717  ftc1anclem7  37718  ftc1anclem8  37719  areacirclem1  37727  bfplem2  37842  bfp  37843  rrntotbnd  37855  lcmineqlem1  42041  lcmineqlem12  42052  lcmineqlem18  42058  aks4d1p1p7  42086  aks4d1p8  42099  primrootscoprmpow  42111  posbezout  42112  aks6d1c2lem4  42139  3rdpwhole  42304  fltnlta  42675  3cubeslem2  42697  3cubeslem3r  42699  irrapxlem5  42838  pellexlem2  42842  pellexlem6  42846  pellfundex  42898  jm2.19lem3  43003  jm2.25  43011  jm2.27c  43019  jm3.1lem2  43030  flcidc  43182  reabssgn  43648  sqrtcval  43653  int-mul12d  44195  cvgdvgrat  44325  bccn1  44356  binomcxplemnotnn0  44368  fperiodmullem  45323  xralrple2  45372  fmul01lt1lem2  45604  mccllem  45616  reclimc  45670  cosknegpi  45886  dvsinax  45930  dvnxpaek  45959  dvnmul  45960  itgsinexp  45972  stoweidlem14  46031  stoweidlem26  46043  wallispilem4  46085  wallispilem5  46086  wallispi2lem1  46088  wallispi2  46090  stirlinglem1  46091  stirlinglem3  46093  stirlinglem4  46094  stirlinglem5  46095  stirlinglem6  46096  stirlinglem7  46097  stirlinglem10  46100  dirkertrigeqlem2  46116  dirkertrigeqlem3  46117  dirkercncflem2  46121  fourierdlem26  46150  fourierdlem41  46165  fourierdlem42  46166  fourierdlem56  46179  fourierdlem57  46180  fourierdlem58  46181  fourierdlem62  46185  fourierdlem64  46187  fourierdlem65  46188  fourierdlem95  46218  sqwvfoura  46245  sqwvfourb  46246  fouriersw  46248  etransclem23  46274  etransclem35  46286  etransclem46  46297  fmtnorec2lem  47552  fmtnorec3  47558  m1expoddALTV  47658  perfectALTVlem2  47732  ztprmneprm  48357  altgsumbc  48362  divge1b  48523  divgt1b  48524  ackval1  48692  affineid  48715  1subrec1sub  48716  rrx2vlinest  48752  line2x  48765