Theorem mulridd 11254

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulridd	⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Proof of Theorem mulridd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulrid 11234	. 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 7417  ℂcc 11126  1c1 11129   · cmul 11133

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 2734  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-mulcom 11192  ax-mulass 11194  ax-distr 11195  ax-1rid 11198  ax-cnre 11201

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 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420

This theorem is used by:  muladd11  11408  muls1d  11702  divrec  11916  diveq1  11929  conjmul  11960  divelunit  13551  modid  13961  addmodlteq  14014  expadd  14172  leexp2r  14242  nnlesq  14273  sqoddm1div8  14311  faclbnd  14358  faclbnd2  14359  faclbnd4lem3  14363  faclbnd6  14367  facavg  14369  bcn0  14378  bcn1  14381  hashf1lem2  14525  hashfac  14527  reccn2  15688  iseraltlem2  15774  iseraltlem3  15775  fsumconst1  15881  hash2iun1dif1  15915  indsumhash  15920  binom11  15925  harmonic  15952  trireciplem  15955  geoserg  15959  pwdif  15961  pwm1geoser  15962  cvgrat  15976  fprodsplit  16059  fprodle  16089  fsumcube  16152  efzval  16196  tanhlt1  16254  tanaddlem  16260  tanadd  16261  cos01gt0  16285  absef  16291  1dvds  16366  bitsfzo  16531  bitsmod  16532  sqgcd  16658  expgcd  16659  lcm1  16706  coprmdvds  16749  qredeu  16754  phiprmpw  16873  coprimeprodsq  16906  pc2dvds  16977  sumhash  16994  fldivp1  16995  pcfaclem  16996  prmpwdvds  17002  prmreclem1  17014  vdwlem3  17081  vdwlem9  17087  prmop1  17136  sylow2a  19752  odadd  19983  zsssubrg  21644  zringcyg  21688  prmirredlem  21691  mulgrhm2  21697  pzriprnglem6  21705  pzriprnglem12  21711  znrrg  21784  mhppwdeg  22384  icopnfcnv  25176  icopnfhmeo  25177  lebnumii  25200  reparphti  25231  itg2const  25974  itg2monolem3  25986  bddibl  26074  dveflem  26213  mvth  26226  dvlipcn  26228  dvivthlem1  26242  dvfsumle  26255  dvfsumabs  26257  dvfsumlem2  26261  plyconst  26438  plyeq0lem  26443  plyco  26474  0dgrb  26479  coefv0  26481  vieta1  26551  aaliou3lem2  26586  tayl0  26605  taylply2  26611  dvtaylp  26613  taylthlem2  26617  radcnvlem1  26656  abelthlem1  26674  abelthlem2  26675  abelthlem3  26676  abelthlem7  26681  abelthlem8  26682  abelthlem9  26683  efper  26724  tangtx  26750  eflogeq  26847  logdivlti  26865  logcnlem4  26890  advlogexp  26900  cxpmul2  26934  dvcxp2  26986  cxpaddle  26997  cxpeq  27002  loglesqrt  27006  relogbexp  27025  ang180lem5  27058  isosctrlem2  27064  isosctrlem3  27065  heron  27083  2efiatan  27163  dvatan  27180  leibpi  27187  birthdaylem3  27198  jensenlem2  27232  logdiflbnd  27239  harmonicbnd4  27255  lgamgulmlem2  27274  lgamcvg2  27299  ftalem5  27321  basellem2  27326  basellem5  27329  basellem8  27332  0sgm  27388  muinv  27437  chpub  27464  logfaclbnd  27466  logexprlim  27469  dchrsum2  27512  sumdchr2  27514  bposlem1  27528  bposlem2  27529  bposlem5  27532  lgsquad2lem1  27628  lgsquad3  27631  2sqlem6  27667  2sqlem8  27670  chtppilim  27719  vmadivsum  27726  dchrisumlem1  27733  dchrisum0flblem1  27752  rpvmasum2  27756  dchrisum0re  27757  dchrisum0lem2a  27761  dchrisum0lem3  27763  rpvmasum  27770  mudivsum  27774  mulogsumlem  27775  vmalogdivsum2  27782  pntrsumo1  27809  pntrlog2bndlem2  27822  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntibndlem2  27835  pntlemc  27839  pntlemf  27849  ostth2lem2  27878  ostth2lem3  27879  ostth2lem4  27880  ostth2  27881  ostth3  27882  ttgcontlem1  29349  axpaschlem  29405  axcontlem2  29430  axcontlem4  29432  axcontlem8  29436  nmoub3i  31262  ubthlem2  31360  htthlem  31406  nmcexi  32515  nmopcoadji  32590  branmfn  32594  gsumind  33793  rearchi  33794  vietadeg1  34096  ccfldextdgrr  34190  nn0constr  34279  constrrecl  34287  constrimcl  34288  constrreinvcl  34290  constrinvcl  34291  constrresqrtcl  34295  constrabscl  34296  cos9thpiminplylem1  34300  madjusmdetlem4  34348  ccatmulgnn0dir  35061  ofcccat  35062  itgexpif  35122  hashreprin  35136  circlemeth  35156  lpadlem2  35199  subfacval2  35774  cvmliftlem2  35873  snmlff  35916  sinccvglem  36259  bcprod  36325  faclimlem1  36330  faclimlem2  36331  faclim2  36335  knoppndvlem14  37230  knoppndvlem15  37231  knoppndvlem16  37232  knoppndvlem18  37234  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  itg2addnclem  38428  areacirclem1  38465  areacirclem4  38468  cntotbnd  38554  lcmineqlem11  42913  lcmineqlem12  42914  aks4d1p1p7  42948  aks4d1p8d2  42959  hashscontpow1  42995  2ap1caineq  43019  sticksstones10  43029  sticksstones12a  43031  aks6d1c6lem1  43044  aks6d1c7lem1  43054  aks6d1c7  43058  oddnumth  43194  oexpreposd  43205  readvrec  43245  frlmvscadiccat  43402  fltnltalem  43516  3cubeslem2  43538  3cubeslem3r  43540  irrapxlem1  43671  irrapxlem4  43674  pell1qrgaplem  43722  reglogexpbas  43746  rmspecfund  43758  rmxy1  43771  rmxp1  43781  rmyp1  43782  rmxm1  43783  jm2.17a  43809  jm2.18  43837  jm2.23  43845  jm2.25  43848  jm2.16nn0  43853  relexpmulnn  44557  int-mul11d  45030  nzprmdif  45151  expgrowthi  45165  expgrowth  45167  binomcxplemdvbinom  45185  binomcxplemnotnn0  45188  sqrlearg  46391  fmul01  46418  fmul01lt1lem1  46422  0ellimcdiv  46485  dvxpaek  46776  dvnxpaek  46778  itgiccshift  46816  itgperiod  46817  itgsbtaddcnst  46818  stoweidlem11  46847  stoweidlem26  46862  stoweidlem38  46874  wallispilem4  46904  stirlinglem1  46910  stirlinglem3  46912  stirlinglem6  46915  stirlinglem7  46916  stirlinglem8  46917  stirlinglem10  46919  stirlinglem12  46921  dirkertrigeqlem3  46936  dirkertrigeq  46937  dirkercncflem1  46939  dirkercncflem2  46940  fourierdlem28  46971  fourierdlem30  46973  fourierdlem39  46982  fourierdlem47  46989  fourierdlem60  47002  fourierdlem61  47003  fourierdlem73  47015  fourierdlem83  47025  fourierdlem87  47029  etransclem14  47084  etransclem24  47094  etransclem25  47095  etransclem35  47105  smfmullem1  47627  sin3t  47743  cos3t  47744  sin5tlem1  47745  deccarry  48207  fpprwppr  48663  fpprwpprb  48664  logblt1b  49502  nn0sumshdiglem2  49560  itcovalpclem2  49609  itcovalt2lem1  49613  eenglngeehlnmlem1  49675  eenglngeehlnmlem2  49676  line2ylem  49689