Theorem mulridd 11250

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  1c1 11128   · cmul 11132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  muladd11  11403  muls1d  11695  divrec  11910  diveq1  11924  conjmul  11956  divelunit  13509  modid  13911  addmodlteq  13962  expadd  14120  leexp2r  14190  nnlesq  14221  sqoddm1div8  14259  faclbnd  14306  faclbnd2  14307  faclbnd4lem3  14311  faclbnd6  14315  facavg  14317  bcn0  14326  bcn1  14329  hashf1lem2  14472  hashfac  14474  reccn2  15611  iseraltlem2  15697  iseraltlem3  15698  hash2iun1dif1  15838  binom11  15846  harmonic  15873  trireciplem  15876  geoserg  15880  pwdif  15882  pwm1geoser  15883  cvgrat  15897  fprodsplit  15980  fprodle  16010  fsumcube  16074  efzval  16118  tanhlt1  16176  tanaddlem  16182  tanadd  16183  cos01gt0  16207  absef  16213  1dvds  16288  bitsfzo  16452  bitsmod  16453  sqgcd  16579  expgcd  16580  lcm1  16627  coprmdvds  16670  qredeu  16675  phiprmpw  16793  coprimeprodsq  16826  pc2dvds  16897  sumhash  16914  fldivp1  16915  pcfaclem  16916  prmpwdvds  16922  prmreclem1  16934  vdwlem3  17001  vdwlem9  17007  prmop1  17056  sylow2a  19598  odadd  19829  zsssubrg  21391  zringcyg  21428  prmirredlem  21431  mulgrhm2  21437  pzriprnglem6  21445  pzriprnglem12  21451  znrrg  21524  mhppwdeg  22086  icopnfcnv  24889  icopnfhmeo  24890  lebnumii  24914  reparphti  24945  reparphtiOLD  24946  itg2const  25691  itg2monolem3  25703  bddibl  25791  dveflem  25933  mvth  25947  dvlipcn  25949  dvivthlem1  25963  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  plyconst  26161  plyeq0lem  26165  plyco  26196  0dgrb  26201  coefv0  26203  vieta1  26270  aaliou3lem2  26301  tayl0  26319  taylply2  26325  taylply2OLD  26326  dvtaylp  26328  taylthlem2  26332  taylthlem2OLD  26333  radcnvlem1  26372  abelthlem1  26391  abelthlem2  26392  abelthlem3  26393  abelthlem7  26398  abelthlem8  26399  abelthlem9  26400  efper  26438  tangtx  26464  eflogeq  26561  logdivlti  26579  logcnlem4  26604  advlogexp  26614  cxpmul2  26648  dvcxp2  26700  cxpaddle  26712  cxpeq  26717  loglesqrt  26721  relogbexp  26740  ang180lem5  26773  isosctrlem2  26779  isosctrlem3  26780  heron  26798  2efiatan  26878  dvatan  26895  leibpi  26902  birthdaylem3  26913  jensenlem2  26948  logdiflbnd  26955  harmonicbnd4  26971  lgamgulmlem2  26990  lgamcvg2  27015  ftalem5  27037  basellem2  27042  basellem5  27045  basellem8  27048  0sgm  27104  muinv  27153  chpub  27181  logfaclbnd  27183  logexprlim  27186  dchrsum2  27229  sumdchr2  27231  bposlem1  27245  bposlem2  27246  bposlem5  27249  lgsquad2lem1  27345  lgsquad3  27348  2sqlem6  27384  2sqlem8  27387  chtppilim  27436  vmadivsum  27443  dchrisumlem1  27450  dchrisum0flblem1  27469  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem2a  27478  dchrisum0lem3  27480  rpvmasum  27487  mudivsum  27491  mulogsumlem  27492  vmalogdivsum2  27499  pntrsumo1  27526  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntibndlem2  27552  pntlemc  27556  pntlemf  27566  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth2  27598  ostth3  27599  ttgcontlem1  28810  axpaschlem  28865  axcontlem2  28890  axcontlem4  28892  axcontlem8  28896  nmoub3i  30700  ubthlem2  30798  htthlem  30844  nmcexi  31953  nmopcoadji  32028  branmfn  32032  rearchi  33307  ccfldextdgrr  33659  nn0constr  33741  constrrecl  33749  constrimcl  33750  constrreinvcl  33752  constrinvcl  33753  constrresqrtcl  33757  constrabscl  33758  cos9thpiminplylem1  33762  madjusmdetlem4  33807  ccatmulgnn0dir  34520  ofcccat  34521  itgexpif  34584  hashreprin  34598  circlemeth  34618  lpadlem2  34658  subfacval2  35155  cvmliftlem2  35254  snmlff  35297  sinccvglem  35640  bcprod  35701  faclimlem1  35706  faclimlem2  35707  faclim2  35711  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem16  36491  knoppndvlem18  36493  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  itg2addnclem  37641  areacirclem1  37678  areacirclem4  37681  cntotbnd  37766  lcmineqlem11  41998  lcmineqlem12  41999  aks4d1p1p7  42033  aks4d1p8d2  42044  hashscontpow1  42080  2ap1caineq  42104  sticksstones10  42114  sticksstones12a  42116  aks6d1c6lem1  42129  aks6d1c7lem1  42139  aks6d1c7  42143  oddnumth  42307  oexpreposd  42318  readvrec  42352  frlmvscadiccat  42476  fltnltalem  42632  3cubeslem2  42655  3cubeslem3r  42657  irrapxlem1  42792  irrapxlem4  42795  pell1qrgaplem  42843  reglogexpbas  42867  rmspecfund  42879  rmxy1  42893  rmxp1  42903  rmyp1  42904  rmxm1  42905  jm2.17a  42931  jm2.18  42959  jm2.23  42967  jm2.25  42970  jm2.16nn0  42975  relexpmulnn  43680  int-mul11d  44153  nzprmdif  44291  expgrowthi  44305  expgrowth  44307  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  sqrlearg  45530  fmul01  45557  fmul01lt1lem1  45561  0ellimcdiv  45626  dvxpaek  45917  dvnxpaek  45919  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stoweidlem11  45988  stoweidlem26  46003  stoweidlem38  46015  wallispilem4  46045  stirlinglem1  46051  stirlinglem3  46053  stirlinglem6  46056  stirlinglem7  46057  stirlinglem8  46058  stirlinglem10  46060  stirlinglem12  46062  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem1  46080  dirkercncflem2  46081  fourierdlem28  46112  fourierdlem30  46114  fourierdlem39  46123  fourierdlem47  46130  fourierdlem60  46143  fourierdlem61  46144  fourierdlem73  46156  fourierdlem83  46166  fourierdlem87  46170  etransclem14  46225  etransclem24  46235  etransclem25  46236  etransclem35  46246  smfmullem1  46768  deccarry  47288  fpprwppr  47701  fpprwpprb  47702  logblt1b  48492  nn0sumshdiglem2  48550  itcovalpclem2  48599  itcovalt2lem1  48603  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  line2ylem  48679