Theorem mullidd 11298

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7408  ℂcc 11169  1c1 11172   · cmul 11176

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-mulcl 11233  ax-mulcom 11235  ax-mulass 11237  ax-distr 11238  ax-1rid 11241  ax-cnre 11244

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411

This theorem is used by:  adddirp1d  11306  addrid  11461  mulsubfacd  11746  mulcand  11918  receu  11930  divdivdiv  11987  divcan5  11988  subrecd  12115  ltrec  12168  recp1lt1  12184  nndivtr  12354  subhalfhalf  12549  xp1d2m1eqxm1d2  12569  gtndiv  12745  ge2halflem1  13206  lincmb01cmp  13595  iccf1o  13596  ltdifltdiv  13942  modfrac  13992  negmod  14027  addmodid  14030  m1expcl2  14196  expgt1  14211  ltexp2a  14277  leexp2a  14283  binom3  14335  faclbnd  14401  faclbnd4lem4  14407  facavg  14412  bcval5  14429  cshweqrep  14939  01sqrexlem2  15377  absimle  15443  reccn2  15731  iseraltlem2  15817  iseraltlem3  15818  o1fsum  15947  abscvgcvg  15953  indsum  15962  ackbijnn  15964  binom1p  15967  binom1dif  15969  incexclem  15972  incexc  15973  climcndslem1  15985  pwdif  16004  geomulcvg  16012  fprodsplit  16100  fallrisefac  16159  bpolysum  16186  bpolydiflem  16187  bpoly4  16192  efcllem  16210  ef01bndlem  16319  efieq1re  16334  eirrlem  16339  iddvds  16406  pwp1fsum  16528  oddpwp1fsum  16529  bitsfzolem  16571  bitsfzo  16572  rpmulgcd  16694  prmind2  16822  isprm5  16845  phiprm  16915  eulerthlem2  16920  fermltl  16922  hashgcdlem  16926  odzdvds  16934  powm2modprm  16942  modprm0  16944  pythagtriplem4  16958  4sqlem18  17101  vdwapun  17113  mulgnnass  19280  odinv  19736  odadd2  20024  pgpfaclem2  20259  abvneg  21044  pzriprnglem6  21753  pzriprnglem12  21759  nrginvrcnlem  24971  nmoid  25022  blcvx  25078  icopnfcnv  25224  reparphti  25279  pcorevlem  25308  ncvsm1  25436  ncvspi  25438  cphipval2  25523  cphipval  25525  itg11  25973  itg2mulc  26029  itg2monolem1  26032  itgcnlem  26071  iblabs  26110  dvexp  26234  dvmptdiv  26255  dvef  26261  lhop1lem  26294  dvcvx  26301  dvfsumlem1  26307  dvfsumlem2  26308  dvfsumlem4  26310  dvfsum2  26315  plypow  26484  dgrcolem1  26553  plyn0mulidp  26565  vieta1lem2  26597  radcnvlem1  26703  radcnvlem2  26704  dvradcnv  26711  abelthlem6  26726  abelthlem7  26728  abelth2  26732  sinhalfpip  26784  sinhalfpim  26785  coshalfpip  26786  coshalfpim  26787  tangtx  26797  efif1olem4  26836  abslogle  26909  logdivlti  26911  advlog  26945  advlogexp  26946  logtayl  26951  cxpaddlelem  27042  cxpaddle  27043  affineequiv  27114  affineequiv2  27115  chordthmlem5  27127  dcubic2  27135  dcubic  27137  mcubic  27138  binom4  27141  dquartlem1  27142  quart1lem  27146  quart1  27147  quartlem1  27148  quart  27152  efiasin  27179  atantayl  27228  cvxcl  27275  scvxcvx  27276  lgamgulmlem5  27323  lgamcvg2  27345  lgam1  27354  wilthlem1  27358  wilthlem2  27359  basellem9  27379  fsumfldivdiaglem  27479  muinv  27483  chpub  27510  logexprlim  27515  mersenne  27517  perfectlem2  27520  dchrmullid  27542  dchrptlem1  27554  dchrsum2  27558  sumdchr2  27560  bposlem2  27575  bposlem9  27582  lgsval2lem  27597  lgsval4a  27609  lgsneg1  27612  lgsdir2lem4  27618  lgsdir  27622  lgsmulsqcoprm  27633  lgsdirnn0  27634  lgsdinn0  27635  gausslemma2dlem1a  27655  gausslemma2dlem4  27659  gausslemma2dlem7  27663  gausslemma2d  27664  lgseisenlem1  27665  lgseisenlem2  27666  lgseisenlem4  27668  lgsquad2lem1  27674  2sqlem8  27716  chebbnd1lem3  27761  chpchtlim  27769  rplogsumlem1  27774  rplogsumlem2  27775  rpvmasumlem  27777  dchrmusum2  27784  dchrvmasum2lem  27786  dchrvmasumlem2  27788  dchrvmasumlem3  27789  dchrisum0flblem1  27798  mulog2sumlem2  27825  vmalogdivsum2  27828  2vmadivsumlem  27830  log2sumbnd  27834  selberglem2  27836  selberg3lem1  27847  selberg4lem1  27850  pntrlog2bndlem2  27868  pntrlog2bndlem5  27871  pntpbnd1  27876  pntpbnd2  27877  pntibndlem2  27881  pntlemb  27887  pntlemr  27892  pntlemk  27896  pntlemo  27897  brbtwn2  29416  colinearalglem4  29420  ax5seglem3  29442  axbtwnid  29450  axpaschlem  29451  axeuclidlem  29473  axcontlem7  29481  axcontlem8  29482  elntg2  29496  nvm1  31200  nvpi  31202  nvmtri  31206  ipval2  31242  ipasslem1  31366  ipasslem4  31369  bcs2  31717  lnfnaddi  32578  nnmulge  33264  quad3d  33274  2exple2exp  33358  indsumin  33361  ccfldsrarelvec  34236  constrfin  34311  constrremulcl  34332  constrrecl  34334  constrimcl  34335  constrmulcl  34336  constrreinvcl  34337  2sqr3minply  34345  cos9thpiminplylem2  34348  sqsscirc1  34473  eulerpartlemgs2  34946  logdivsqrle  35213  subfacp1lem6  35871  subfaclim  35874  cvxpconn  35928  cvxsconn  35929  resconn  35932  sinccvglem  36358  fwddifn0  36851  nn0prpwlem  37032  knoppndvlem9  37308  knoppndvlem14  37313  bj-bary1lem1  38152  mblfinlem3  38497  itg2addnclem3  38511  iblabsnc  38522  iblmulc2nc  38523  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anclem8  38538  areacirclem1  38546  bfplem2  38677  bfp  38678  rrntotbnd  38690  lcmineqlem1  42999  lcmineqlem12  43010  lcmineqlem18  43016  aks4d1p1p7  43044  aks4d1p8  43057  primrootscoprmpow  43069  posbezout  43070  aks6d1c2lem4  43097  3rdpwhole  43271  fltnlta  43613  3cubeslem2  43634  3cubeslem3r  43636  irrapxlem5  43771  pellexlem2  43775  pellexlem6  43779  pellfundex  43831  jm2.19lem3  43936  jm2.25  43944  jm2.27c  43952  jm3.1lem2  43963  flcidc  44115  reabssgn  44580  sqrtcval  44585  int-mul12d  45127  cvgdvgrat  45241  bccn1  45272  binomcxplemnotnn0  45284  fperiodmullem  46240  xralrple2  46288  fmul01lt1lem2  46519  mccllem  46531  reclimc  46585  cosknegpi  46801  dvsinax  46845  dvnxpaek  46874  dvnmul  46875  itgsinexp  46887  stoweidlem14  46946  stoweidlem26  46958  wallispilem4  47000  wallispilem5  47001  wallispi2lem1  47003  wallispi2  47005  stirlinglem1  47006  stirlinglem3  47008  stirlinglem4  47009  stirlinglem5  47010  stirlinglem6  47011  stirlinglem7  47012  stirlinglem10  47015  dirkertrigeqlem2  47031  dirkertrigeqlem3  47032  dirkercncflem2  47036  fourierdlem26  47065  fourierdlem41  47080  fourierdlem42  47081  fourierdlem56  47094  fourierdlem57  47095  fourierdlem58  47096  fourierdlem62  47100  fourierdlem64  47102  fourierdlem65  47103  fourierdlem95  47133  sqwvfoura  47160  sqwvfourb  47161  fouriersw  47163  etransclem23  47189  etransclem35  47201  etransclem46  47212  sin5tlem1  47841  sin5tlem2  47842  fmtnorec2lem  48549  fmtnorec3  48555  m1expoddALTV  48668  perfectALTVlem2  48742  ztprmneprm  49381  altgsumbc  49386  divge1b  49546  divgt1b  49547  ackval1  49715  affineid  49738  1subrec1sub  49739  rrx2vlinest  49775  line2x  49788  dvsec  50778  dvcsc  50779