Theorem mulridd 11230

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107  1c1 11110   · cmul 11114

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  muladd11  11383  muls1d  11673  divrec  11887  diveq1  11904  conjmul  11930  divelunit  13470  modid  13860  addmodlteq  13910  expadd  14069  leexp2r  14138  nnlesq  14168  sqoddm1div8  14205  faclbnd  14249  faclbnd2  14250  faclbnd4lem3  14254  faclbnd6  14258  facavg  14260  bcn0  14269  bcn1  14272  hashf1lem2  14416  hashfac  14418  reccn2  15540  iseraltlem2  15628  iseraltlem3  15629  hash2iun1dif1  15769  binom11  15777  harmonic  15804  trireciplem  15807  geoserg  15811  pwdif  15813  pwm1geoser  15814  cvgrat  15828  fprodsplit  15909  fprodle  15939  fsumcube  16003  efzval  16044  tanhlt1  16102  tanaddlem  16108  tanadd  16109  cos01gt0  16133  absef  16139  1dvds  16213  bitsfzo  16375  bitsmod  16376  sqgcd  16501  lcm1  16546  coprmdvds  16589  qredeu  16594  phiprmpw  16708  coprimeprodsq  16740  pc2dvds  16811  sumhash  16828  fldivp1  16829  pcfaclem  16830  prmpwdvds  16836  prmreclem1  16848  vdwlem3  16915  vdwlem9  16921  prmop1  16970  sylow2a  19486  odadd  19717  zsssubrg  21002  zringcyg  21038  prmirredlem  21041  mulgrhm2  21047  znrrg  21120  mhppwdeg  21692  icopnfcnv  24457  icopnfhmeo  24458  lebnumii  24481  reparphti  24512  itg2const  25257  itg2monolem3  25269  bddibl  25356  dveflem  25495  mvth  25508  dvlipcn  25510  dvivthlem1  25524  dvfsumle  25537  dvfsumabs  25539  dvfsumlem2  25543  plyconst  25719  plyeq0lem  25723  plyco  25754  0dgrb  25759  coefv0  25761  vieta1  25824  aaliou3lem2  25855  tayl0  25873  taylply2  25879  dvtaylp  25881  taylthlem2  25885  radcnvlem1  25924  abelthlem1  25942  abelthlem2  25943  abelthlem3  25944  abelthlem7  25949  abelthlem8  25950  abelthlem9  25951  efper  25988  tangtx  26014  eflogeq  26109  logdivlti  26127  logcnlem4  26152  advlogexp  26162  cxpmul2  26196  dvcxp2  26246  cxpaddle  26257  cxpeq  26262  loglesqrt  26263  relogbexp  26282  ang180lem5  26315  isosctrlem2  26321  isosctrlem3  26322  heron  26340  2efiatan  26420  dvatan  26437  leibpi  26444  birthdaylem3  26455  jensenlem2  26489  logdiflbnd  26496  harmonicbnd4  26512  lgamgulmlem2  26531  lgamcvg2  26556  ftalem5  26578  basellem2  26583  basellem5  26586  basellem8  26589  0sgm  26645  muinv  26694  chpub  26720  logfaclbnd  26722  logexprlim  26725  dchrsum2  26768  sumdchr2  26770  bposlem1  26784  bposlem2  26785  bposlem5  26788  lgsquad2lem1  26884  lgsquad3  26887  2sqlem6  26923  2sqlem8  26926  chtppilim  26975  vmadivsum  26982  dchrisumlem1  26989  dchrisum0flblem1  27008  rpvmasum2  27012  dchrisum0re  27013  dchrisum0lem2a  27017  dchrisum0lem3  27019  rpvmasum  27026  mudivsum  27030  mulogsumlem  27031  vmalogdivsum2  27038  pntrsumo1  27065  pntrlog2bndlem2  27078  pntrlog2bndlem4  27080  pntrlog2bndlem5  27081  pntibndlem2  27091  pntlemc  27095  pntlemf  27105  ostth2lem2  27134  ostth2lem3  27135  ostth2lem4  27136  ostth2  27137  ostth3  27138  ttgcontlem1  28139  axpaschlem  28195  axcontlem2  28220  axcontlem4  28222  axcontlem8  28226  nmoub3i  30021  ubthlem2  30119  htthlem  30165  nmcexi  31274  nmopcoadji  31349  branmfn  31353  rearchi  32456  ccfldextdgrr  32741  madjusmdetlem4  32805  ccatmulgnn0dir  33548  ofcccat  33549  itgexpif  33613  hashreprin  33627  circlemeth  33647  lpadlem2  33687  subfacval2  34173  cvmliftlem2  34272  snmlff  34315  sinccvglem  34652  bcprod  34703  faclimlem1  34708  faclimlem2  34709  faclim2  34713  gg-reparphti  35167  gg-dvfsumle  35177  gg-dvfsumlem2  35178  knoppndvlem14  35396  knoppndvlem15  35397  knoppndvlem16  35398  knoppndvlem18  35400  poimirlem29  36512  poimirlem30  36513  poimirlem31  36514  poimirlem32  36515  itg2addnclem  36534  areacirclem1  36571  areacirclem4  36574  cntotbnd  36659  lcmineqlem11  40899  lcmineqlem12  40900  aks4d1p1p7  40934  aks4d1p8d2  40945  2ap1caineq  40956  sticksstones10  40966  sticksstones12a  40968  frlmvscadiccat  41082  oddnumth  41209  oexpreposd  41212  expgcd  41225  fltnltalem  41405  3cubeslem2  41413  3cubeslem3r  41415  irrapxlem1  41550  irrapxlem4  41553  pell1qrgaplem  41601  reglogexpbas  41625  rmspecfund  41637  rmxy1  41651  rmxp1  41661  rmyp1  41662  rmxm1  41663  jm2.17a  41689  jm2.18  41717  jm2.23  41725  jm2.25  41728  jm2.16nn0  41733  relexpmulnn  42450  int-mul11d  42924  nzprmdif  43068  expgrowthi  43082  expgrowth  43084  binomcxplemdvbinom  43102  binomcxplemnotnn0  43105  sqrlearg  44256  fmul01  44286  fmul01lt1lem1  44290  0ellimcdiv  44355  dvxpaek  44646  dvnxpaek  44648  itgiccshift  44686  itgperiod  44687  itgsbtaddcnst  44688  stoweidlem11  44717  stoweidlem26  44732  stoweidlem38  44744  wallispilem4  44774  stirlinglem1  44780  stirlinglem3  44782  stirlinglem6  44785  stirlinglem7  44786  stirlinglem8  44787  stirlinglem10  44789  stirlinglem12  44791  dirkertrigeqlem3  44806  dirkertrigeq  44807  dirkercncflem1  44809  dirkercncflem2  44810  fourierdlem28  44841  fourierdlem30  44843  fourierdlem39  44852  fourierdlem47  44859  fourierdlem60  44872  fourierdlem61  44873  fourierdlem73  44885  fourierdlem83  44895  fourierdlem87  44899  etransclem14  44954  etransclem24  44964  etransclem25  44965  etransclem35  44975  smfmullem1  45497  deccarry  46009  fpprwppr  46397  fpprwpprb  46398  pzriprnglem6  46800  pzriprnglem12  46806  logblt1b  47240  nn0sumshdiglem2  47298  itcovalpclem2  47347  itcovalt2lem1  47351  eenglngeehlnmlem1  47413  eenglngeehlnmlem2  47414  line2ylem  47427