Theorem mulridd 11329

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  1c1 11204   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-mulcl 11265  ax-mulcom 11267  ax-mulass 11269  ax-distr 11270  ax-1rid 11273  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  muladd11  11483  muls1d  11779  divrec  11993  diveq1  12006  conjmul  12037  divelunit  13628  modid  14039  addmodlteq  14092  expadd  14250  leexp2r  14320  nnlesq  14352  sqoddm1div8  14390  faclbnd  14437  faclbnd2  14438  faclbnd4lem3  14442  faclbnd6  14446  facavg  14448  bcn0  14457  bcn1  14460  hashf1lem2  14604  hashfac  14606  reccn2  15769  iseraltlem2  15855  iseraltlem3  15856  fsumconst1  15962  hash2iun1dif1  15996  indsumhash  16001  binom11  16006  harmonic  16033  trireciplem  16036  geoserg  16040  pwdif  16042  pwm1geoser  16043  cvgrat  16057  fprodsplit  16138  fprodle  16168  fsumcube  16231  efzval  16275  tanhlt1  16333  tanaddlem  16339  tanadd  16340  cos01gt0  16364  absef  16370  1dvds  16445  bitsfzo  16610  bitsmod  16611  sqgcd  16741  expgcd  16742  lcm1  16790  coprmdvds  16833  qredeu  16838  phiprmpw  16958  coprimeprodsq  16991  pc2dvds  17062  sumhash  17079  fldivp1  17080  pcfaclem  17081  prmpwdvds  17087  prmreclem1  17099  vdwlem3  17166  vdwlem9  17172  prmop1  17221  sylow2a  19838  odadd  20069  zsssubrg  21736  zringcyg  21780  prmirredlem  21783  mulgrhm2  21789  pzriprnglem6  21797  pzriprnglem12  21803  znrrg  21876  mhppwdeg  22476  icopnfcnv  25268  icopnfhmeo  25269  lebnumii  25292  reparphti  25323  itg2const  26066  itg2monolem3  26078  bddibl  26165  dveflem  26304  mvth  26317  dvlipcn  26319  dvivthlem1  26333  dvfsumle  26346  dvfsumabs  26348  dvfsumlem2  26352  plyconst  26529  plyeq0lem  26534  plyco  26565  0dgrb  26570  coefv0  26572  vieta1  26640  aaliou3lem2  26675  tayl0  26694  taylply2  26700  dvtaylp  26702  taylthlem2  26706  radcnvlem1  26745  abelthlem1  26763  abelthlem2  26764  abelthlem3  26765  abelthlem7  26770  abelthlem8  26771  abelthlem9  26772  efper  26813  tangtx  26839  eflogeq  26935  logdivlti  26953  logcnlem4  26978  advlogexp  26988  cxpmul2  27022  dvcxp2  27074  cxpaddle  27085  cxpeq  27090  loglesqrt  27094  relogbexp  27113  ang180lem5  27146  isosctrlem2  27152  isosctrlem3  27153  heron  27171  2efiatan  27251  dvatan  27268  leibpi  27275  birthdaylem3  27286  jensenlem2  27320  logdiflbnd  27327  harmonicbnd4  27343  lgamgulmlem2  27362  lgamcvg2  27387  ftalem5  27409  basellem2  27414  basellem5  27417  basellem8  27420  0sgm  27476  muinv  27525  chpub  27552  logfaclbnd  27554  logexprlim  27557  dchrsum2  27600  sumdchr2  27602  bposlem1  27616  bposlem2  27617  bposlem5  27620  lgsquad2lem1  27716  lgsquad3  27719  2sqlem6  27755  2sqlem8  27758  chtppilim  27807  vmadivsum  27814  dchrisumlem1  27821  dchrisum0flblem1  27840  rpvmasum2  27844  dchrisum0re  27845  dchrisum0lem2a  27849  dchrisum0lem3  27851  rpvmasum  27858  mudivsum  27862  mulogsumlem  27863  vmalogdivsum2  27870  pntrsumo1  27897  pntrlog2bndlem2  27910  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  pntibndlem2  27923  pntlemc  27927  pntlemf  27937  ostth2lem2  27966  ostth2lem3  27967  ostth2lem4  27968  ostth2  27969  ostth3  27970  ttgcontlem1  29467  axpaschlem  29523  axcontlem2  29548  axcontlem4  29550  axcontlem8  29554  nmoub3i  31380  ubthlem2  31478  htthlem  31524  nmcexi  32633  nmopcoadji  32708  branmfn  32712  gsumind  33952  rearchi  33953  vietadeg1  34256  ccfldextdgrr  34350  nn0constr  34439  constrrecl  34447  constrimcl  34448  constrreinvcl  34450  constrinvcl  34451  constrresqrtcl  34455  constrabscl  34456  cos9thpiminplylem1  34460  madjusmdetlem4  34508  ccatmulgnn0dir  35220  ofcccat  35221  itgexpif  35281  hashreprin  35295  circlemeth  35315  lpadlem2  35358  subfacval2  36038  cvmliftlem2  36137  snmlff  36180  sinccvglem  36523  bcprod  36595  faclimlem1  36600  faclimlem2  36601  faclim2  36605  knoppndvlem14  37483  knoppndvlem15  37484  knoppndvlem16  37485  knoppndvlem18  37487  poimirlem29  38660  poimirlem30  38661  poimirlem31  38662  poimirlem32  38663  itg2addnclem  38682  areacirclem1  38719  areacirclem4  38722  cntotbnd  38823  lcmineqlem11  43182  lcmineqlem12  43183  aks4d1p1p7  43217  aks4d1p8d2  43228  hashscontpow1  43264  2ap1caineq  43288  sticksstones10  43298  sticksstones12a  43300  aks6d1c6lem1  43313  aks6d1c7lem1  43323  aks6d1c7  43327  oddnumth  43461  oexpreposd  43472  readvrec  43506  frlmvscadiccat  43666  fltnltalem  43766  3cubeslem2  43788  3cubeslem3r  43790  irrapxlem1  43922  irrapxlem4  43925  pell1qrgaplem  43973  reglogexpbas  43997  rmspecfund  44009  rmxy1  44022  rmxp1  44032  rmyp1  44033  rmxm1  44034  jm2.17a  44060  jm2.18  44088  jm2.23  44096  jm2.25  44099  jm2.16nn0  44104  relexpmulnn  44802  int-mul11d  45275  nzprmdif  45396  expgrowthi  45410  expgrowth  45412  binomcxplemdvbinom  45430  binomcxplemnotnn0  45433  sqrlearg  46658  fmul01  46685  fmul01lt1lem1  46689  0ellimcdiv  46752  dvxpaek  47043  dvnxpaek  47045  itgiccshift  47083  itgperiod  47084  itgsbtaddcnst  47085  stoweidlem11  47114  stoweidlem26  47129  stoweidlem38  47141  wallispilem4  47171  stirlinglem1  47177  stirlinglem3  47179  stirlinglem6  47182  stirlinglem7  47183  stirlinglem8  47184  stirlinglem10  47186  stirlinglem12  47188  dirkertrigeqlem3  47203  dirkertrigeq  47204  dirkercncflem1  47206  dirkercncflem2  47207  fourierdlem28  47238  fourierdlem30  47240  fourierdlem39  47249  fourierdlem47  47256  fourierdlem60  47269  fourierdlem61  47270  fourierdlem73  47282  fourierdlem83  47292  fourierdlem87  47296  etransclem14  47351  etransclem24  47361  etransclem25  47362  etransclem35  47372  smfmullem1  47894  sin3t  48010  cos3t  48011  sin5tlem1  48012  deccarry  48474  fpprwppr  48930  fpprwpprb  48931  logblt1b  49769  nn0sumshdiglem2  49827  itcovalpclem2  49876  itcovalt2lem1  49880  eenglngeehlnmlem1  49943  eenglngeehlnmlem2  49944  line2ylem  49956