Theorem mulridd 11353

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   · cmul 11232

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-mulcom 11291  ax-mulass 11293  ax-distr 11294  ax-1rid 11297  ax-cnre 11300

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  muladd11  11507  muls1d  11803  divrec  12017  diveq1  12030  conjmul  12061  divelunit  13652  modid  14063  addmodlteq  14116  expadd  14274  leexp2r  14344  nnlesq  14376  sqoddm1div8  14414  faclbnd  14461  faclbnd2  14462  faclbnd4lem3  14466  faclbnd6  14470  facavg  14472  bcn0  14481  bcn1  14484  hashf1lem2  14628  hashfac  14630  reccn2  15793  iseraltlem2  15879  iseraltlem3  15880  fsumconst1  15986  hash2iun1dif1  16020  indsumhash  16025  binom11  16030  harmonic  16057  trireciplem  16060  geoserg  16064  pwdif  16066  pwm1geoser  16067  cvgrat  16081  fprodsplit  16162  fprodle  16192  fsumcube  16255  efzval  16299  tanhlt1  16357  tanaddlem  16363  tanadd  16364  cos01gt0  16388  absef  16394  1dvds  16469  bitsfzo  16634  bitsmod  16635  sqgcd  16765  expgcd  16766  lcm1  16814  coprmdvds  16857  qredeu  16862  phiprmpw  16982  coprimeprodsq  17015  pc2dvds  17086  sumhash  17103  fldivp1  17104  pcfaclem  17105  prmpwdvds  17111  prmreclem1  17123  vdwlem3  17190  vdwlem9  17196  prmop1  17245  sylow2a  19863  odadd  20094  zsssubrg  21761  zringcyg  21805  prmirredlem  21808  mulgrhm2  21814  pzriprnglem6  21822  pzriprnglem12  21828  znrrg  21901  mhppwdeg  22501  icopnfcnv  25293  icopnfhmeo  25294  lebnumii  25317  reparphti  25348  itg2const  26091  itg2monolem3  26103  bddibl  26190  dveflem  26329  mvth  26342  dvlipcn  26344  dvivthlem1  26358  dvfsumle  26371  dvfsumabs  26373  dvfsumlem2  26377  plyconst  26554  plyeq0lem  26559  plyco  26590  0dgrb  26595  coefv0  26597  vieta1  26665  aaliou3lem2  26700  tayl0  26719  taylply2  26725  dvtaylp  26727  taylthlem2  26731  radcnvlem1  26770  abelthlem1  26788  abelthlem2  26789  abelthlem3  26790  abelthlem7  26795  abelthlem8  26796  abelthlem9  26797  efper  26838  tangtx  26864  eflogeq  26960  logdivlti  26978  logcnlem4  27003  advlogexp  27013  cxpmul2  27047  dvcxp2  27099  cxpaddle  27110  cxpeq  27115  loglesqrt  27119  relogbexp  27138  ang180lem5  27171  isosctrlem2  27177  isosctrlem3  27178  heron  27196  2efiatan  27276  dvatan  27293  leibpi  27300  birthdaylem3  27311  jensenlem2  27345  logdiflbnd  27352  harmonicbnd4  27368  lgamgulmlem2  27387  lgamcvg2  27412  ftalem5  27434  basellem2  27439  basellem5  27442  basellem8  27445  0sgm  27501  muinv  27550  chpub  27577  logfaclbnd  27579  logexprlim  27582  dchrsum2  27625  sumdchr2  27627  bposlem1  27641  bposlem2  27642  bposlem5  27645  lgsquad2lem1  27741  lgsquad3  27744  2sqlem6  27780  2sqlem8  27783  chtppilim  27832  vmadivsum  27839  dchrisumlem1  27846  dchrisum0flblem1  27865  rpvmasum2  27869  dchrisum0re  27870  dchrisum0lem2a  27874  dchrisum0lem3  27876  rpvmasum  27883  mudivsum  27887  mulogsumlem  27888  vmalogdivsum2  27895  pntrsumo1  27922  pntrlog2bndlem2  27935  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  pntibndlem2  27948  pntlemc  27952  pntlemf  27962  ostth2lem2  27991  ostth2lem3  27992  ostth2lem4  27993  ostth2  27994  ostth3  27995  ttgcontlem1  29492  axpaschlem  29548  axcontlem2  29573  axcontlem4  29575  axcontlem8  29579  nmoub3i  31405  ubthlem2  31503  htthlem  31549  nmcexi  32658  nmopcoadji  32733  branmfn  32737  gsumind  33976  rearchi  33977  vietadeg1  34280  ccfldextdgrr  34374  nn0constr  34463  constrrecl  34471  constrimcl  34472  constrreinvcl  34474  constrinvcl  34475  constrresqrtcl  34479  constrabscl  34480  cos9thpiminplylem1  34484  madjusmdetlem4  34532  ccatmulgnn0dir  35244  ofcccat  35245  itgexpif  35305  hashreprin  35319  circlemeth  35339  lpadlem2  35382  subfacval2  36119  cvmliftlem2  36218  snmlff  36261  sinccvglem  36604  bcprod  36681  faclimlem1  36686  faclimlem2  36687  faclim2  36691  knoppndvlem14  37569  knoppndvlem15  37570  knoppndvlem16  37571  knoppndvlem18  37573  poimirlem29  38759  poimirlem30  38760  poimirlem31  38761  poimirlem32  38762  itg2addnclem  38781  areacirclem1  38818  areacirclem4  38821  cntotbnd  38922  lcmineqlem11  43281  lcmineqlem12  43282  aks4d1p1p7  43316  aks4d1p8d2  43327  hashscontpow1  43363  2ap1caineq  43387  sticksstones10  43397  sticksstones12a  43399  aks6d1c6lem1  43412  aks6d1c7lem1  43422  aks6d1c7  43426  oddnumth  43561  oexpreposd  43572  readvrec  43606  frlmvscadiccat  43766  fltnltalem  43866  3cubeslem2  43888  3cubeslem3r  43890  irrapxlem1  44022  irrapxlem4  44025  pell1qrgaplem  44073  reglogexpbas  44097  rmspecfund  44109  rmxy1  44122  rmxp1  44132  rmyp1  44133  rmxm1  44134  jm2.17a  44160  jm2.18  44188  jm2.23  44196  jm2.25  44199  jm2.16nn0  44204  relexpmulnn  44901  int-mul11d  45374  nzprmdif  45495  expgrowthi  45509  expgrowth  45511  binomcxplemdvbinom  45529  binomcxplemnotnn0  45532  sqrlearg  46770  fmul01  46797  fmul01lt1lem1  46801  0ellimcdiv  46864  dvxpaek  47155  dvnxpaek  47157  itgiccshift  47195  itgperiod  47196  itgsbtaddcnst  47197  stoweidlem11  47226  stoweidlem26  47241  stoweidlem38  47253  wallispilem4  47283  stirlinglem1  47289  stirlinglem3  47291  stirlinglem6  47294  stirlinglem7  47295  stirlinglem8  47296  stirlinglem10  47298  stirlinglem12  47300  dirkertrigeqlem3  47315  dirkertrigeq  47316  dirkercncflem1  47318  dirkercncflem2  47319  fourierdlem28  47350  fourierdlem30  47352  fourierdlem39  47361  fourierdlem47  47368  fourierdlem60  47381  fourierdlem61  47382  fourierdlem73  47394  fourierdlem83  47404  fourierdlem87  47408  etransclem14  47463  etransclem24  47473  etransclem25  47474  etransclem35  47484  smfmullem1  48006  sin3t  48122  cos3t  48123  sin5tlem1  48124  deccarry  48586  fpprwppr  49042  fpprwpprb  49043  logblt1b  49881  nn0sumshdiglem2  49939  itcovalpclem2  49988  itcovalt2lem1  49992  eenglngeehlnmlem1  50055  eenglngeehlnmlem2  50056  line2ylem  50068