Theorem mullidd 11226

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097  1c1 11100   · cmul 11104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-mulcl 11161  ax-mulcom 11163  ax-mulass 11165  ax-distr 11166  ax-1rid 11169  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  adddirp1d  11234  addrid  11389  mulsubfacd  11674  mulcand  11846  receu  11858  divdivdiv  11915  divcan5  11916  subrecd  12043  ltrec  12096  recp1lt1  12112  nndivtr  12282  subhalfhalf  12477  xp1d2m1eqxm1d2  12497  gtndiv  12672  ge2halflem1  13132  lincmb01cmp  13521  iccf1o  13522  ltdifltdiv  13866  modfrac  13916  negmod  13951  addmodid  13954  m1expcl2  14120  expgt1  14135  ltexp2a  14201  leexp2a  14207  binom3  14259  faclbnd  14325  faclbnd4lem4  14331  facavg  14336  bcval5  14353  cshweqrep  14857  01sqrexlem2  15293  absimle  15359  reccn2  15647  iseraltlem2  15733  iseraltlem3  15734  o1fsum  15864  abscvgcvg  15870  indsum  15879  ackbijnn  15881  binom1p  15884  binom1dif  15886  incexclem  15889  incexc  15890  climcndslem1  15902  pwdif  15921  geomulcvg  15929  fprodsplit  16019  fallrisefac  16078  bpolysum  16106  bpolydiflem  16107  bpoly4  16112  efcllem  16130  ef01bndlem  16239  efieq1re  16254  eirrlem  16259  iddvds  16326  pwp1fsum  16448  oddpwp1fsum  16449  bitsfzolem  16491  bitsfzo  16492  rpmulgcd  16614  prmind2  16742  isprm5  16765  phiprm  16835  eulerthlem2  16840  fermltl  16842  hashgcdlem  16846  odzdvds  16854  powm2modprm  16862  modprm0  16864  pythagtriplem4  16878  4sqlem18  17021  vdwapun  17033  mulgnnass  19174  odinv  19630  odadd2  19918  pgpfaclem2  20153  abvneg  20908  pzriprnglem6  21615  pzriprnglem12  21621  nrginvrcnlem  24827  nmoid  24878  blcvx  24934  icopnfcnv  25080  reparphti  25135  pcorevlem  25164  ncvsm1  25292  ncvspi  25294  cphipval2  25379  cphipval  25381  itg11  25829  itg2mulc  25885  itg2monolem1  25888  itgcnlem  25928  iblabs  25967  dvexp  26091  dvmptdiv  26112  dvef  26118  lhop1lem  26151  dvcvx  26158  dvfsumlem1  26164  dvfsumlem2  26165  dvfsumlem4  26167  dvfsum2  26172  plypow  26341  dgrcolem1  26409  plyn0mulidp  26421  vieta1lem2  26451  radcnvlem1  26552  radcnvlem2  26553  dvradcnv  26560  abelthlem6  26575  abelthlem7  26577  abelth2  26581  sinhalfpip  26633  sinhalfpim  26634  coshalfpip  26635  coshalfpim  26636  tangtx  26646  efif1olem4  26686  abslogle  26759  logdivlti  26761  advlog  26795  advlogexp  26796  logtayl  26801  cxpaddlelem  26892  cxpaddle  26893  affineequiv  26964  affineequiv2  26965  chordthmlem5  26977  dcubic2  26985  dcubic  26987  mcubic  26988  binom4  26991  dquartlem1  26992  quart1lem  26996  quart1  26997  quartlem1  26998  quart  27002  efiasin  27029  atantayl  27078  cvxcl  27125  scvxcvx  27126  lgamgulmlem5  27173  lgamcvg2  27195  lgam1  27204  wilthlem1  27208  wilthlem2  27209  basellem9  27229  fsumfldivdiaglem  27329  muinv  27333  chpub  27360  logexprlim  27365  mersenne  27367  perfectlem2  27370  dchrmullid  27392  dchrptlem1  27404  dchrsum2  27408  sumdchr2  27410  bposlem2  27425  bposlem9  27432  lgsval2lem  27447  lgsval4a  27459  lgsneg1  27462  lgsdir2lem4  27468  lgsdir  27472  lgsmulsqcoprm  27483  lgsdirnn0  27484  lgsdinn0  27485  gausslemma2dlem1a  27505  gausslemma2dlem4  27509  gausslemma2dlem7  27513  gausslemma2d  27514  lgseisenlem1  27515  lgseisenlem2  27516  lgseisenlem4  27518  lgsquad2lem1  27524  2sqlem8  27566  chebbnd1lem3  27611  chpchtlim  27619  rplogsumlem1  27624  rplogsumlem2  27625  rpvmasumlem  27627  dchrmusum2  27634  dchrvmasum2lem  27636  dchrvmasumlem2  27638  dchrvmasumlem3  27639  dchrisum0flblem1  27648  mulog2sumlem2  27675  vmalogdivsum2  27678  2vmadivsumlem  27680  log2sumbnd  27684  selberglem2  27686  selberg3lem1  27697  selberg4lem1  27700  pntrlog2bndlem2  27718  pntrlog2bndlem5  27721  pntpbnd1  27726  pntpbnd2  27727  pntibndlem2  27731  pntlemb  27737  pntlemr  27742  pntlemk  27746  pntlemo  27747  brbtwn2  29221  colinearalglem4  29225  ax5seglem3  29247  axbtwnid  29255  axpaschlem  29256  axeuclidlem  29278  axcontlem7  29286  axcontlem8  29287  elntg2  29301  nvm1  30983  nvpi  30985  nvmtri  30989  ipval2  31025  ipasslem1  31149  ipasslem4  31152  bcs2  31500  lnfnaddi  32361  nnmulge  33050  quad3d  33060  2exple2exp  33144  indsumin  33147  ccfldsrarelvec  34027  constrfin  34102  constrremulcl  34123  constrrecl  34125  constrimcl  34126  constrmulcl  34127  constrreinvcl  34128  2sqr3minply  34136  cos9thpiminplylem2  34139  sqsscirc1  34264  eulerpartlemgs2  34736  logdivsqrle  35003  subfacp1lem6  35631  subfaclim  35634  cvxpconn  35688  cvxsconn  35689  resconn  35692  sinccvglem  36118  fwddifn0  36610  nn0prpwlem  36777  knoppndvlem9  37053  knoppndvlem14  37058  bj-bary1lem1  37899  mblfinlem3  38254  itg2addnclem3  38268  iblabsnc  38279  iblmulc2nc  38280  ftc1anclem6  38293  ftc1anclem7  38294  ftc1anclem8  38295  areacirclem1  38303  bfplem2  38418  bfp  38419  rrntotbnd  38431  lcmineqlem1  42742  lcmineqlem12  42753  lcmineqlem18  42759  aks4d1p1p7  42787  aks4d1p8  42800  primrootscoprmpow  42812  posbezout  42813  aks6d1c2lem4  42840  3rdpwhole  42999  fltnlta  43343  3cubeslem2  43364  3cubeslem3r  43366  irrapxlem5  43501  pellexlem2  43505  pellexlem6  43509  pellfundex  43561  jm2.19lem3  43666  jm2.25  43674  jm2.27c  43682  jm3.1lem2  43693  flcidc  43845  reabssgn  44310  sqrtcval  44315  int-mul12d  44857  cvgdvgrat  44971  bccn1  45002  binomcxplemnotnn0  45014  fperiodmullem  45970  xralrple2  46018  fmul01lt1lem2  46249  mccllem  46261  reclimc  46315  cosknegpi  46531  dvsinax  46575  dvnxpaek  46604  dvnmul  46605  itgsinexp  46617  stoweidlem14  46676  stoweidlem26  46688  wallispilem4  46730  wallispilem5  46731  wallispi2lem1  46733  wallispi2  46735  stirlinglem1  46736  stirlinglem3  46738  stirlinglem4  46739  stirlinglem5  46740  stirlinglem6  46741  stirlinglem7  46742  stirlinglem10  46745  dirkertrigeqlem2  46761  dirkertrigeqlem3  46762  dirkercncflem2  46766  fourierdlem26  46795  fourierdlem41  46810  fourierdlem42  46811  fourierdlem56  46824  fourierdlem57  46825  fourierdlem58  46826  fourierdlem62  46830  fourierdlem64  46832  fourierdlem65  46833  fourierdlem95  46863  sqwvfoura  46890  sqwvfourb  46891  fouriersw  46893  etransclem23  46919  etransclem35  46931  etransclem46  46942  sin5tlem1  47555  sin5tlem2  47556  fmtnorec2lem  48239  fmtnorec3  48245  m1expoddALTV  48358  perfectALTVlem2  48432  ztprmneprm  49072  altgsumbc  49077  divge1b  49237  divgt1b  49238  ackval1  49406  affineid  49429  1subrec1sub  49430  rrx2vlinest  49466  line2x  49479