Theorem mullidd 11165

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7369  ℂcc 11038  1c1 11041   · cmul 11045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-mulcl 11102  ax-mulcom 11104  ax-mulass 11106  ax-distr 11107  ax-1rid 11110  ax-cnre 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6456  df-fv 6508  df-ov 7372

This theorem is referenced by:  adddirp1d  11173  addrid  11328  mulsubfacd  11613  mulcand  11785  receu  11797  divdivdiv  11858  divcan5  11859  subrecd  11986  ltrec  12040  recp1lt1  12056  nndivtr  12226  subhalfhalf  12413  xp1d2m1eqxm1d2  12433  gtndiv  12608  ge2halflem1  13061  lincmb01cmp  13450  iccf1o  13451  ltdifltdiv  13795  modfrac  13845  negmod  13880  addmodid  13883  m1expcl2  14049  expgt1  14064  ltexp2a  14130  leexp2a  14136  binom3  14188  faclbnd  14254  faclbnd4lem4  14260  facavg  14265  bcval5  14282  cshweqrep  14785  01sqrexlem2  15207  absimle  15273  reccn2  15561  iseraltlem2  15647  iseraltlem3  15648  o1fsum  15778  abscvgcvg  15784  indsum  15793  ackbijnn  15795  binom1p  15798  binom1dif  15800  incexclem  15803  incexc  15804  climcndslem1  15816  pwdif  15835  geomulcvg  15843  fprodsplit  15933  fallrisefac  15992  bpolysum  16020  bpolydiflem  16021  bpoly4  16026  efcllem  16044  ef01bndlem  16153  efieq1re  16168  eirrlem  16173  iddvds  16240  pwp1fsum  16362  oddpwp1fsum  16363  bitsfzolem  16405  bitsfzo  16406  rpmulgcd  16528  prmind2  16656  isprm5  16679  phiprm  16749  eulerthlem2  16754  fermltl  16756  hashgcdlem  16760  odzdvds  16768  powm2modprm  16776  modprm0  16778  pythagtriplem4  16792  4sqlem18  16935  vdwapun  16947  mulgnnass  19087  odinv  19538  odadd2  19826  pgpfaclem2  20061  abvneg  20805  pzriprnglem6  21468  pzriprnglem12  21474  nrginvrcnlem  24658  nmoid  24709  blcvx  24765  icopnfcnv  24911  reparphti  24966  pcorevlem  24995  ncvsm1  25123  ncvspi  25125  cphipval2  25210  cphipval  25212  itg11  25660  itg2mulc  25716  itg2monolem1  25719  itgcnlem  25759  iblabs  25798  dvexp  25922  dvmptdiv  25943  dvef  25949  lhop1lem  25982  dvcvx  25989  dvfsumlem1  25995  dvfsumlem2  25996  dvfsumlem4  25998  dvfsum2  26003  plypow  26172  dgrcolem1  26240  vieta1lem2  26279  radcnvlem1  26380  radcnvlem2  26381  dvradcnv  26388  abelthlem6  26403  abelthlem7  26405  abelth2  26409  sinhalfpip  26458  sinhalfpim  26459  coshalfpip  26460  coshalfpim  26461  tangtx  26471  efif1olem4  26511  abslogle  26584  logdivlti  26586  advlog  26620  advlogexp  26621  logtayl  26626  cxpaddlelem  26717  cxpaddle  26718  affineequiv  26789  affineequiv2  26790  chordthmlem5  26802  dcubic2  26810  dcubic  26812  mcubic  26813  binom4  26816  dquartlem1  26817  quart1lem  26821  quart1  26822  quartlem1  26823  quart  26827  efiasin  26854  atantayl  26903  cvxcl  26950  scvxcvx  26951  lgamgulmlem5  26998  lgamcvg2  27020  lgam1  27029  wilthlem1  27033  wilthlem2  27034  basellem9  27054  fsumfldivdiaglem  27154  muinv  27158  chpub  27185  logexprlim  27190  mersenne  27192  perfectlem2  27195  dchrmullid  27217  dchrptlem1  27229  dchrsum2  27233  sumdchr2  27235  bposlem2  27250  bposlem9  27257  lgsval2lem  27272  lgsval4a  27284  lgsneg1  27287  lgsdir2lem4  27293  lgsdir  27297  lgsmulsqcoprm  27308  lgsdirnn0  27309  lgsdinn0  27310  gausslemma2dlem1a  27330  gausslemma2dlem4  27334  gausslemma2dlem7  27338  gausslemma2d  27339  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem4  27343  lgsquad2lem1  27349  2sqlem8  27391  chebbnd1lem3  27436  chpchtlim  27444  rplogsumlem1  27449  rplogsumlem2  27450  rpvmasumlem  27452  dchrmusum2  27459  dchrvmasum2lem  27461  dchrvmasumlem2  27463  dchrvmasumlem3  27464  dchrisum0flblem1  27473  mulog2sumlem2  27500  vmalogdivsum2  27503  2vmadivsumlem  27505  log2sumbnd  27509  selberglem2  27511  selberg3lem1  27522  selberg4lem1  27525  pntrlog2bndlem2  27543  pntrlog2bndlem5  27546  pntpbnd1  27551  pntpbnd2  27552  pntibndlem2  27556  pntlemb  27562  pntlemr  27567  pntlemk  27571  pntlemo  27572  brbtwn2  28976  colinearalglem4  28980  ax5seglem3  29002  axbtwnid  29010  axpaschlem  29011  axeuclidlem  29033  axcontlem7  29041  axcontlem8  29042  elntg2  29056  nvm1  30738  nvpi  30740  nvmtri  30744  ipval2  30780  ipasslem1  30904  ipasslem4  30907  bcs2  31255  lnfnaddi  32116  nnmulge  32814  quad3d  32824  2exple2exp  32920  indsumin  32923  ccfldsrarelvec  33817  constrfin  33892  constrremulcl  33913  constrrecl  33915  constrimcl  33916  constrmulcl  33917  constrreinvcl  33918  2sqr3minply  33926  cos9thpiminplylem2  33929  sqsscirc1  34054  eulerpartlemgs2  34526  plymulx0  34693  logdivsqrle  34796  subfacp1lem6  35369  subfaclim  35372  cvxpconn  35426  cvxsconn  35427  resconn  35430  sinccvglem  35856  fwddifn0  36348  nn0prpwlem  36506  knoppndvlem9  36782  knoppndvlem14  36787  bj-bary1lem1  37627  mblfinlem3  37982  itg2addnclem3  37996  iblabsnc  38007  iblmulc2nc  38008  ftc1anclem6  38021  ftc1anclem7  38022  ftc1anclem8  38023  areacirclem1  38031  bfplem2  38146  bfp  38147  rrntotbnd  38159  lcmineqlem1  42470  lcmineqlem12  42481  lcmineqlem18  42487  aks4d1p1p7  42515  aks4d1p8  42528  primrootscoprmpow  42540  posbezout  42541  aks6d1c2lem4  42568  3rdpwhole  42726  fltnlta  43098  3cubeslem2  43119  3cubeslem3r  43121  irrapxlem5  43256  pellexlem2  43260  pellexlem6  43264  pellfundex  43316  jm2.19lem3  43421  jm2.25  43429  jm2.27c  43437  jm3.1lem2  43448  flcidc  43600  reabssgn  44065  sqrtcval  44070  int-mul12d  44612  cvgdvgrat  44742  bccn1  44773  binomcxplemnotnn0  44785  fperiodmullem  45738  xralrple2  45786  fmul01lt1lem2  46017  mccllem  46029  reclimc  46083  cosknegpi  46299  dvsinax  46343  dvnxpaek  46372  dvnmul  46373  itgsinexp  46385  stoweidlem14  46444  stoweidlem26  46456  wallispilem4  46498  wallispilem5  46499  wallispi2lem1  46501  wallispi2  46503  stirlinglem1  46504  stirlinglem3  46506  stirlinglem4  46507  stirlinglem5  46508  stirlinglem6  46509  stirlinglem7  46510  stirlinglem10  46513  dirkertrigeqlem2  46529  dirkertrigeqlem3  46530  dirkercncflem2  46534  fourierdlem26  46563  fourierdlem41  46578  fourierdlem42  46579  fourierdlem56  46592  fourierdlem57  46593  fourierdlem58  46594  fourierdlem62  46598  fourierdlem64  46600  fourierdlem65  46601  fourierdlem95  46631  sqwvfoura  46658  sqwvfourb  46659  fouriersw  46661  etransclem23  46687  etransclem35  46699  etransclem46  46710  sin5tlem1  47323  sin5tlem2  47324  fmtnorec2lem  48007  fmtnorec3  48013  m1expoddALTV  48126  perfectALTVlem2  48200  ztprmneprm  48825  altgsumbc  48830  divge1b  48990  divgt1b  48991  ackval1  49159  affineid  49182  1subrec1sub  49183  rrx2vlinest  49219  line2x  49232