Theorem mulridd 11196

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  1c1 11071   · cmul 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-mulcl 11132  ax-mulcom 11134  ax-mulass 11136  ax-distr 11137  ax-1rid 11140  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395

This theorem is referenced by:  muladd11  11350  muls1d  11644  divrec  11858  diveq1  11872  conjmul  11905  divelunit  13495  modid  13903  addmodlteq  13956  expadd  14114  leexp2r  14184  nnlesq  14215  sqoddm1div8  14253  faclbnd  14300  faclbnd2  14301  faclbnd4lem3  14305  faclbnd6  14309  facavg  14311  bcn0  14320  bcn1  14323  hashf1lem2  14466  hashfac  14468  reccn2  15607  iseraltlem2  15693  iseraltlem3  15694  fsumconst1  15801  hash2iun1dif1  15835  indsumhash  15840  binom11  15845  harmonic  15872  trireciplem  15875  geoserg  15879  pwdif  15881  pwm1geoser  15882  cvgrat  15896  fprodsplit  15979  fprodle  16009  fsumcube  16073  efzval  16117  tanhlt1  16175  tanaddlem  16181  tanadd  16182  cos01gt0  16206  absef  16212  1dvds  16287  bitsfzo  16452  bitsmod  16453  sqgcd  16579  expgcd  16580  lcm1  16627  coprmdvds  16670  qredeu  16675  phiprmpw  16794  coprimeprodsq  16827  pc2dvds  16898  sumhash  16915  fldivp1  16916  pcfaclem  16917  prmpwdvds  16923  prmreclem1  16935  vdwlem3  17002  vdwlem9  17008  prmop1  17057  sylow2a  19642  odadd  19873  zsssubrg  21457  zringcyg  21501  prmirredlem  21504  mulgrhm2  21510  pzriprnglem6  21518  pzriprnglem12  21524  znrrg  21597  mhppwdeg  22195  icopnfcnv  24984  icopnfhmeo  24985  lebnumii  25008  reparphti  25039  itg2const  25782  itg2monolem3  25794  bddibl  25882  dveflem  26021  mvth  26034  dvlipcn  26036  dvivthlem1  26050  dvfsumle  26063  dvfsumabs  26065  dvfsumlem2  26069  plyconst  26246  plyeq0lem  26250  plyco  26281  0dgrb  26286  coefv0  26288  vieta1  26353  aaliou3lem2  26384  tayl0  26402  taylply2  26408  dvtaylp  26410  taylthlem2  26414  radcnvlem1  26453  abelthlem1  26471  abelthlem2  26472  abelthlem3  26473  abelthlem7  26478  abelthlem8  26479  abelthlem9  26480  efper  26521  tangtx  26547  eflogeq  26644  logdivlti  26662  logcnlem4  26687  advlogexp  26697  cxpmul2  26731  dvcxp2  26783  cxpaddle  26794  cxpeq  26799  loglesqrt  26803  relogbexp  26822  ang180lem5  26855  isosctrlem2  26861  isosctrlem3  26862  heron  26880  2efiatan  26960  dvatan  26977  leibpi  26984  birthdaylem3  26995  jensenlem2  27029  logdiflbnd  27036  harmonicbnd4  27052  lgamgulmlem2  27071  lgamcvg2  27096  ftalem5  27118  basellem2  27123  basellem5  27126  basellem8  27129  0sgm  27185  muinv  27234  chpub  27261  logfaclbnd  27263  logexprlim  27266  dchrsum2  27309  sumdchr2  27311  bposlem1  27325  bposlem2  27326  bposlem5  27329  lgsquad2lem1  27425  lgsquad3  27428  2sqlem6  27464  2sqlem8  27467  chtppilim  27516  vmadivsum  27523  dchrisumlem1  27530  dchrisum0flblem1  27549  rpvmasum2  27553  dchrisum0re  27554  dchrisum0lem2a  27558  dchrisum0lem3  27560  rpvmasum  27567  mudivsum  27571  mulogsumlem  27572  vmalogdivsum2  27579  pntrsumo1  27606  pntrlog2bndlem2  27619  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  pntibndlem2  27632  pntlemc  27636  pntlemf  27646  ostth2lem2  27675  ostth2lem3  27676  ostth2lem4  27677  ostth2  27678  ostth3  27679  ttgcontlem1  29031  axpaschlem  29087  axcontlem2  29112  axcontlem4  29114  axcontlem8  29118  nmoub3i  30922  ubthlem2  31020  htthlem  31066  nmcexi  32175  nmopcoadji  32250  branmfn  32254  gsumind  33492  rearchi  33493  vietadeg1  33836  ccfldextdgrr  33930  nn0constr  34019  constrrecl  34027  constrimcl  34028  constrreinvcl  34030  constrinvcl  34031  constrresqrtcl  34035  constrabscl  34036  cos9thpiminplylem1  34040  madjusmdetlem4  34088  ccatmulgnn0dir  34800  ofcccat  34801  itgexpif  34864  hashreprin  34878  circlemeth  34898  lpadlem2  34941  subfacval2  35501  cvmliftlem2  35600  snmlff  35643  sinccvglem  35986  bcprod  36052  faclimlem1  36057  faclimlem2  36058  faclim2  36062  knoppndvlem14  36927  knoppndvlem15  36928  knoppndvlem16  36929  knoppndvlem18  36931  poimirlem29  38112  poimirlem30  38113  poimirlem31  38114  poimirlem32  38115  itg2addnclem  38134  areacirclem1  38171  areacirclem4  38174  cntotbnd  38259  lcmineqlem11  42620  lcmineqlem12  42621  aks4d1p1p7  42655  aks4d1p8d2  42666  hashscontpow1  42702  2ap1caineq  42726  sticksstones10  42736  sticksstones12a  42738  aks6d1c6lem1  42751  aks6d1c7lem1  42761  aks6d1c7  42765  oddnumth  42884  oexpreposd  42895  readvrec  42935  frlmvscadiccat  43092  fltnltalem  43208  3cubeslem2  43230  3cubeslem3r  43232  irrapxlem1  43363  irrapxlem4  43366  pell1qrgaplem  43414  reglogexpbas  43438  rmspecfund  43450  rmxy1  43463  rmxp1  43473  rmyp1  43474  rmxm1  43475  jm2.17a  43501  jm2.18  43529  jm2.23  43537  jm2.25  43540  jm2.16nn0  43545  relexpmulnn  44249  int-mul11d  44722  nzprmdif  44859  expgrowthi  44873  expgrowth  44875  binomcxplemdvbinom  44893  binomcxplemnotnn0  44896  sqrlearg  46093  fmul01  46120  fmul01lt1lem1  46124  0ellimcdiv  46187  dvxpaek  46478  dvnxpaek  46480  itgiccshift  46518  itgperiod  46519  itgsbtaddcnst  46520  stoweidlem11  46549  stoweidlem26  46564  stoweidlem38  46576  wallispilem4  46606  stirlinglem1  46612  stirlinglem3  46614  stirlinglem6  46617  stirlinglem7  46618  stirlinglem8  46619  stirlinglem10  46621  stirlinglem12  46623  dirkertrigeqlem3  46638  dirkertrigeq  46639  dirkercncflem1  46641  dirkercncflem2  46642  fourierdlem28  46673  fourierdlem30  46675  fourierdlem39  46684  fourierdlem47  46691  fourierdlem60  46704  fourierdlem61  46705  fourierdlem73  46717  fourierdlem83  46727  fourierdlem87  46731  etransclem14  46786  etransclem24  46796  etransclem25  46797  etransclem35  46807  smfmullem1  47329  sin3t  47429  cos3t  47430  sin5tlem1  47431  deccarry  47869  fpprwppr  48325  fpprwpprb  48326  logblt1b  49150  nn0sumshdiglem2  49208  itcovalpclem2  49257  itcovalt2lem1  49261  eenglngeehlnmlem1  49323  eenglngeehlnmlem2  49324  line2ylem  49337