Theorem mullidd 11228

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7401  ℂcc 11103  1c1 11106   · cmul 11110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-mulcl 11167  ax-mulcom 11169  ax-mulass 11171  ax-distr 11172  ax-1rid 11175  ax-cnre 11178

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404

This theorem is referenced by:  adddirp1d  11236  addrid  11390  mulsubfacd  11671  mulcand  11843  receu  11855  divdivdiv  11911  divcan5  11912  subrec  12039  ltrec  12092  recp1lt1  12108  nndivtr  12255  subhalfhalf  12442  xp1d2m1eqxm1d2  12462  gtndiv  12635  lincmb01cmp  13468  iccf1o  13469  ltdifltdiv  13795  modfrac  13845  negmod  13877  addmodid  13880  m1expcl2  14047  expgt1  14062  ltexp2a  14127  leexp2a  14133  binom3  14183  faclbnd  14246  faclbnd4lem4  14252  facavg  14257  bcval5  14274  cshweqrep  14767  01sqrexlem2  15186  absimle  15252  reccn2  15537  iseraltlem2  15625  iseraltlem3  15626  o1fsum  15755  abscvgcvg  15761  ackbijnn  15770  binom1p  15773  binom1dif  15775  incexclem  15778  incexc  15779  climcndslem1  15791  pwdif  15810  geomulcvg  15818  fprodsplit  15906  fallrisefac  15965  bpolysum  15993  bpolydiflem  15994  bpoly4  15999  efcllem  16017  ef01bndlem  16123  efieq1re  16138  eirrlem  16143  iddvds  16209  pwp1fsum  16330  oddpwp1fsum  16331  bitsfzolem  16371  bitsfzo  16372  rpmulgcd  16494  prmind2  16618  isprm5  16640  phiprm  16708  eulerthlem2  16713  fermltl  16715  hashgcdlem  16719  odzdvds  16726  powm2modprm  16734  modprm0  16736  pythagtriplem4  16750  4sqlem18  16893  vdwapun  16905  mulgnnass  19025  odinv  19470  odadd2  19758  pgpfaclem2  19993  abvneg  20666  pzriprnglem6  21340  pzriprnglem12  21346  nrginvrcnlem  24529  nmoid  24580  blcvx  24635  icopnfcnv  24788  reparphti  24844  reparphtiOLD  24845  pcorevlem  24874  ncvsm1  25003  ncvspi  25005  cphipval2  25090  cphipval  25092  itg11  25541  itg2mulc  25598  itg2monolem1  25601  itgcnlem  25640  iblabs  25679  dvexp  25806  dvmptdiv  25827  dvef  25833  lhop1lem  25867  dvcvx  25874  dvfsumlem1  25881  dvfsumlem2  25882  dvfsumlem2OLD  25883  dvfsumlem4  25885  dvfsum2  25890  plypow  26058  dgrcolem1  26127  vieta1lem2  26164  radcnvlem1  26265  radcnvlem2  26266  dvradcnv  26273  abelthlem6  26289  abelthlem7  26291  abelth2  26295  sinhalfpip  26343  sinhalfpim  26344  coshalfpip  26345  coshalfpim  26346  tangtx  26356  efif1olem4  26395  abslogle  26467  logdivlti  26469  advlog  26503  advlogexp  26504  logtayl  26509  cxpaddlelem  26601  cxpaddle  26602  affineequiv  26670  affineequiv2  26671  chordthmlem5  26683  dcubic2  26691  dcubic  26693  mcubic  26694  binom4  26697  dquartlem1  26698  quart1lem  26702  quart1  26703  quartlem1  26704  quart  26708  efiasin  26735  atantayl  26784  cvxcl  26832  scvxcvx  26833  lgamgulmlem5  26880  lgamcvg2  26902  lgam1  26911  wilthlem1  26915  wilthlem2  26916  basellem9  26936  fsumfldivdiaglem  27036  muinv  27040  chpub  27068  logexprlim  27073  mersenne  27075  perfectlem2  27078  dchrmullid  27100  dchrptlem1  27112  dchrsum2  27116  sumdchr2  27118  bposlem2  27133  bposlem9  27140  lgsval2lem  27155  lgsval4a  27167  lgsneg1  27170  lgsdir2lem4  27176  lgsdir  27180  lgsmulsqcoprm  27191  lgsdirnn0  27192  lgsdinn0  27193  gausslemma2dlem1a  27213  gausslemma2dlem4  27217  gausslemma2dlem7  27221  gausslemma2d  27222  lgseisenlem1  27223  lgseisenlem2  27224  lgseisenlem4  27226  lgsquad2lem1  27232  2sqlem8  27274  chebbnd1lem3  27319  chpchtlim  27327  rplogsumlem1  27332  rplogsumlem2  27333  rpvmasumlem  27335  dchrmusum2  27342  dchrvmasum2lem  27344  dchrvmasumlem2  27346  dchrvmasumlem3  27347  dchrisum0flblem1  27356  mulog2sumlem2  27383  vmalogdivsum2  27386  2vmadivsumlem  27388  log2sumbnd  27392  selberglem2  27394  selberg3lem1  27405  selberg4lem1  27408  pntrlog2bndlem2  27426  pntrlog2bndlem5  27429  pntpbnd1  27434  pntpbnd2  27435  pntibndlem2  27439  pntlemb  27445  pntlemr  27450  pntlemk  27454  pntlemo  27455  brbtwn2  28598  colinearalglem4  28602  ax5seglem3  28624  axbtwnid  28632  axpaschlem  28633  axeuclidlem  28655  axcontlem7  28663  axcontlem8  28664  elntg2  28678  nvm1  30353  nvpi  30355  nvmtri  30359  ipval2  30395  ipasslem1  30519  ipasslem4  30522  bcs2  30870  lnfnaddi  31731  nnmulge  32398  ccfldsrarelvec  33191  sqsscirc1  33343  indsum  33474  indsumin  33475  eulerpartlemgs2  33834  plymulx0  34013  logdivsqrle  34117  subfacp1lem6  34631  subfaclim  34634  cvxpconn  34688  cvxsconn  34689  resconn  34692  sinccvglem  35112  fwddifn0  35597  nn0prpwlem  35663  knoppndvlem9  35852  knoppndvlem14  35857  bj-bary1lem1  36648  mblfinlem3  36983  itg2addnclem3  36997  iblabsnc  37008  iblmulc2nc  37009  ftc1anclem6  37022  ftc1anclem7  37023  ftc1anclem8  37024  areacirclem1  37032  bfplem2  37147  bfp  37148  rrntotbnd  37160  lcmineqlem1  41353  lcmineqlem12  41364  lcmineqlem18  41370  aks4d1p1p7  41398  aks4d1p8  41411  fltnlta  41860  3cubeslem2  41878  3cubeslem3r  41880  irrapxlem5  42019  pellexlem2  42023  pellexlem6  42027  pellfundex  42079  jm2.19lem3  42185  jm2.25  42193  jm2.27c  42201  jm3.1lem2  42212  flcidc  42371  reabssgn  42842  sqrtcval  42847  int-mul12d  43390  cvgdvgrat  43527  bccn1  43558  binomcxplemnotnn0  43570  fperiodmullem  44464  xralrple2  44515  fmul01lt1lem2  44752  mccllem  44764  reclimc  44820  cosknegpi  45036  dvsinax  45080  dvnxpaek  45109  dvnmul  45110  itgsinexp  45122  stoweidlem14  45181  stoweidlem26  45193  wallispilem4  45235  wallispilem5  45236  wallispi2lem1  45238  wallispi2  45240  stirlinglem1  45241  stirlinglem3  45243  stirlinglem4  45244  stirlinglem5  45245  stirlinglem6  45246  stirlinglem7  45247  stirlinglem10  45250  dirkertrigeqlem2  45266  dirkertrigeqlem3  45267  dirkercncflem2  45271  fourierdlem26  45300  fourierdlem41  45315  fourierdlem42  45316  fourierdlem56  45329  fourierdlem57  45330  fourierdlem58  45331  fourierdlem62  45335  fourierdlem64  45337  fourierdlem65  45338  fourierdlem95  45368  sqwvfoura  45395  sqwvfourb  45396  fouriersw  45398  etransclem23  45424  etransclem35  45436  etransclem46  45447  fmtnorec2lem  46661  fmtnorec3  46667  m1expoddALTV  46767  perfectALTVlem2  46841  ztprmneprm  47178  altgsumbc  47183  divge1b  47347  divgt1b  47348  ackval1  47521  affineid  47544  1subrec1sub  47545  rrx2vlinest  47581  line2x  47594