Theorem addlidd 11482

Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addlidd	⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addlidd

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addlid 11464	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7408  ℂcc 11169  0cc0 11171   + caddc 11174

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-ltxr 11319

This theorem is used by:  negeu  11518  subge0  11798  sublt0d  11911  un0addcl  12608  lincmb01cmp  13595  ico01fl0  13927  muladdmod  14023  discr  14351  ccatlid  14699  swrdfv0  14764  swrdpfx  14823  pfxpfx  14824  cats1un  14837  swrdccatin2  14845  revpfxsfxrev  14884  cshwidx0mod  14923  cshw1  14940  relexpaddg  15173  rennim  15373  max0add  15444  fsumsplit  15874  sumsplit  15901  isumsplit  15976  arisum2  15997  binomfallfaclem2  16173  efaddlem  16226  eftlub  16244  ef4p  16248  rpnnen2lem11  16359  moddvds  16400  divalglem9  16538  sadadd2lem2  16587  sadcaddlem  16594  gcdmultipled  16671  pcmpt  17031  4sqlem11  17094  vdwlem6  17125  gsumsgrpccat  18997  mulgnn0dir  19275  sylow1lem1  19773  efgsval2  19908  efgsp1  19912  zaddablx  20047  pgpfaclem1  20258  regsumfsum  21702  regsumsupp  21889  mplcoe5  22310  nrmmetd  24854  blcvx  25078  xrsxmet  25090  reparphti  25279  nulmbl  25817  itg2splitlem  26030  itg2split  26031  itg2monolem1  26032  itgsplitioo  26119  ditgsplit  26142  dvcnp2  26201  dvcmul  26225  dvcmulf  26226  dvmptcmul  26245  dveflem  26260  dvef  26261  dvlipcn  26275  dvlt0  26286  plymullem1  26494  coeeulem  26504  dgradd2  26548  dgrmulc  26551  plydivlem3  26579  aareccl  26616  taylthlem1  26663  sin2kpi  26775  cos2kpi  26776  coshalfpim  26787  sinkpi  26813  chordthmlem3  27125  chordthmlem5  27127  dcubic1lem  27134  dcubic  27137  atancj  27201  atanlogaddlem  27204  atanlogsublem  27206  scvxcvx  27276  zetacvg  27305  ftalem5  27367  ftalem7  27369  basellem3  27373  chtublem  27501  2sqn0  27724  2sqnn  27729  rplogsumlem2  27775  dchrisumlem1  27779  pntrlog2bndlem2  27868  brbtwn2  29416  axlowdimlem16  29468  axeuclidlem  29473  elntg2  29496  eucrct2eupth  30779  2clwwlk2clwwlk  30884  re0cj  33268  bcm1n  33320  wrdt2ind  33449  nn0constr  34326  constraddcl  34327  constrnegcl  34328  constrdircl  34330  constrremulcl  34332  constrrecl  34334  constrimcl  34335  constrmulcl  34336  constrreinvcl  34337  constrinvcl  34338  constrresqrtcl  34342  constrabscl  34343  2sqr3minply  34345  cos9thpiminplylem1  34347  cos9thpiminply  34353  cos9thpinconstrlem1  34354  esumpfinvallem  34639  signsplypnf  35113  fsum2dsub  35170  logdivsqrle  35213  cvxpconn  35928  cvxsconn  35929  fwddifnp1  36852  tan2h  38455  poimirlem16  38474  mbfposadd  38505  itg2addnc  38512  ftc1anclem5  38535  bfplem2  38677  aks4d1p1p4  43041  aks4d1p7d1  43052  primrootspoweq0  43076  aks6d1c1  43086  aks6d1c5lem1  43106  sticksstones10  43125  sticksstones22  43138  bcle2d  43149  dffltz  43584  3cubeslem3r  43636  pellexlem6  43779  jm2.18  43933  sqrtcval  44585  relexpaddss  44662  int-add02d  45129  sub2times  46210  fzisoeu  46237  xralrple2  46288  cosknegpi  46801  dvsinax  46845  dvasinbx  46852  dvnxpaek  46874  dvnmul  46875  stoweidlem1  46933  stoweidlem13  46945  stoweidlem42  46974  stirlinglem5  47010  stirlinglem11  47016  fourierdlem42  47081  fourierdlem51  47089  fourierdlem88  47126  fourierdlem103  47141  fourierdlem104  47142  fourierdlem107  47145  sqwvfoura  47160  sqwvfourb  47161  fouriersw  47163  elaa2lem  47165  hspmbllem1  47558  cnambpcma  48286  readdcnnred  48295  gpg3kgrtriex  49109  nn0mnd  49198  altgsumbcALT  49387  nn0sumshdiglemA  49653  line2xlem  49787  line2x  49788  itschlc0yqe  49794  itsclc0yqsollem1  49796  itschlc0xyqsol1  49800  itschlc0xyqsol  49801  2itscp  49815  veronesev2lem  50896  veronesev3lem  50897  veronesev4lem  50898  veronesev5lem  50899  veronesev6lem  50900