Theorem mulridd 11326

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 11306	. 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 7420  ℂcc 11198  1c1 11201   · cmul 11205

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 2733  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  muladd11  11480  muls1d  11776  divrec  11990  diveq1  12003  conjmul  12034  divelunit  13625  modid  14036  addmodlteq  14089  expadd  14247  leexp2r  14317  nnlesq  14349  sqoddm1div8  14387  faclbnd  14434  faclbnd2  14435  faclbnd4lem3  14439  faclbnd6  14443  facavg  14445  bcn0  14454  bcn1  14457  hashf1lem2  14601  hashfac  14603  reccn2  15764  iseraltlem2  15850  iseraltlem3  15851  fsumconst1  15957  hash2iun1dif1  15991  indsumhash  15996  binom11  16001  harmonic  16028  trireciplem  16031  geoserg  16035  pwdif  16037  pwm1geoser  16038  cvgrat  16052  fprodsplit  16133  fprodle  16163  fsumcube  16226  efzval  16270  tanhlt1  16328  tanaddlem  16334  tanadd  16335  cos01gt0  16359  absef  16365  1dvds  16440  bitsfzo  16605  bitsmod  16606  sqgcd  16736  expgcd  16737  lcm1  16785  coprmdvds  16828  qredeu  16833  phiprmpw  16953  coprimeprodsq  16986  pc2dvds  17057  sumhash  17074  fldivp1  17075  pcfaclem  17076  prmpwdvds  17082  prmreclem1  17094  vdwlem3  17161  vdwlem9  17167  prmop1  17216  sylow2a  19833  odadd  20064  zsssubrg  21731  zringcyg  21775  prmirredlem  21778  mulgrhm2  21784  pzriprnglem6  21792  pzriprnglem12  21798  znrrg  21871  mhppwdeg  22471  icopnfcnv  25263  icopnfhmeo  25264  lebnumii  25287  reparphti  25318  itg2const  26061  itg2monolem3  26073  bddibl  26160  dveflem  26299  mvth  26312  dvlipcn  26314  dvivthlem1  26328  dvfsumle  26341  dvfsumabs  26343  dvfsumlem2  26347  plyconst  26524  plyeq0lem  26529  plyco  26560  0dgrb  26565  coefv0  26567  vieta1  26635  aaliou3lem2  26670  tayl0  26689  taylply2  26695  dvtaylp  26697  taylthlem2  26701  radcnvlem1  26740  abelthlem1  26758  abelthlem2  26759  abelthlem3  26760  abelthlem7  26765  abelthlem8  26766  abelthlem9  26767  efper  26808  tangtx  26834  eflogeq  26930  logdivlti  26948  logcnlem4  26973  advlogexp  26983  cxpmul2  27017  dvcxp2  27069  cxpaddle  27080  cxpeq  27085  loglesqrt  27089  relogbexp  27108  ang180lem5  27141  isosctrlem2  27147  isosctrlem3  27148  heron  27166  2efiatan  27246  dvatan  27263  leibpi  27270  birthdaylem3  27281  jensenlem2  27315  logdiflbnd  27322  harmonicbnd4  27338  lgamgulmlem2  27357  lgamcvg2  27382  ftalem5  27404  basellem2  27409  basellem5  27412  basellem8  27415  0sgm  27471  muinv  27520  chpub  27547  logfaclbnd  27549  logexprlim  27552  dchrsum2  27595  sumdchr2  27597  bposlem1  27611  bposlem2  27612  bposlem5  27615  lgsquad2lem1  27711  lgsquad3  27714  2sqlem6  27750  2sqlem8  27753  chtppilim  27802  vmadivsum  27809  dchrisumlem1  27816  dchrisum0flblem1  27835  rpvmasum2  27839  dchrisum0re  27840  dchrisum0lem2a  27844  dchrisum0lem3  27846  rpvmasum  27853  mudivsum  27857  mulogsumlem  27858  vmalogdivsum2  27865  pntrsumo1  27892  pntrlog2bndlem2  27905  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntibndlem2  27918  pntlemc  27922  pntlemf  27932  ostth2lem2  27961  ostth2lem3  27962  ostth2lem4  27963  ostth2  27964  ostth3  27965  ttgcontlem1  29462  axpaschlem  29518  axcontlem2  29543  axcontlem4  29545  axcontlem8  29549  nmoub3i  31375  ubthlem2  31473  htthlem  31519  nmcexi  32628  nmopcoadji  32703  branmfn  32707  gsumind  33906  rearchi  33907  vietadeg1  34210  ccfldextdgrr  34304  nn0constr  34393  constrrecl  34401  constrimcl  34402  constrreinvcl  34404  constrinvcl  34405  constrresqrtcl  34409  constrabscl  34410  cos9thpiminplylem1  34414  madjusmdetlem4  34462  ccatmulgnn0dir  35174  ofcccat  35175  itgexpif  35235  hashreprin  35249  circlemeth  35269  lpadlem2  35312  subfacval2  35952  cvmliftlem2  36051  snmlff  36094  sinccvglem  36437  bcprod  36503  faclimlem1  36508  faclimlem2  36509  faclim2  36513  knoppndvlem14  37391  knoppndvlem15  37392  knoppndvlem16  37393  knoppndvlem18  37395  poimirlem29  38567  poimirlem30  38568  poimirlem31  38569  poimirlem32  38570  itg2addnclem  38589  areacirclem1  38626  areacirclem4  38629  cntotbnd  38730  lcmineqlem11  43089  lcmineqlem12  43090  aks4d1p1p7  43124  aks4d1p8d2  43135  hashscontpow1  43171  2ap1caineq  43195  sticksstones10  43205  sticksstones12a  43207  aks6d1c6lem1  43220  aks6d1c7lem1  43230  aks6d1c7  43234  oddnumth  43368  oexpreposd  43379  readvrec  43413  frlmvscadiccat  43573  fltnltalem  43673  3cubeslem2  43695  3cubeslem3r  43697  irrapxlem1  43828  irrapxlem4  43831  pell1qrgaplem  43879  reglogexpbas  43903  rmspecfund  43915  rmxy1  43928  rmxp1  43938  rmyp1  43939  rmxm1  43940  jm2.17a  43966  jm2.18  43994  jm2.23  44002  jm2.25  44005  jm2.16nn0  44010  relexpmulnn  44708  int-mul11d  45181  nzprmdif  45302  expgrowthi  45316  expgrowth  45318  binomcxplemdvbinom  45336  binomcxplemnotnn0  45339  sqrlearg  46564  fmul01  46591  fmul01lt1lem1  46595  0ellimcdiv  46658  dvxpaek  46949  dvnxpaek  46951  itgiccshift  46989  itgperiod  46990  itgsbtaddcnst  46991  stoweidlem11  47020  stoweidlem26  47035  stoweidlem38  47047  wallispilem4  47077  stirlinglem1  47083  stirlinglem3  47085  stirlinglem6  47088  stirlinglem7  47089  stirlinglem8  47090  stirlinglem10  47092  stirlinglem12  47094  dirkertrigeqlem3  47109  dirkertrigeq  47110  dirkercncflem1  47112  dirkercncflem2  47113  fourierdlem28  47144  fourierdlem30  47146  fourierdlem39  47155  fourierdlem47  47162  fourierdlem60  47175  fourierdlem61  47176  fourierdlem73  47188  fourierdlem83  47198  fourierdlem87  47202  etransclem14  47257  etransclem24  47267  etransclem25  47268  etransclem35  47278  smfmullem1  47800  sin3t  47916  cos3t  47917  sin5tlem1  47918  deccarry  48380  fpprwppr  48836  fpprwpprb  48837  logblt1b  49675  nn0sumshdiglem2  49733  itcovalpclem2  49782  itcovalt2lem1  49786  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  line2ylem  49862