Theorem addlidd 11438

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 11420	. 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 7416  ℂcc 11125  0cc0 11127   + caddc 11130

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275

This theorem is used by:  negeu  11474  subge0  11754  sublt0d  11867  un0addcl  12564  lincmb01cmp  13550  ico01fl0  13882  muladdmod  13978  discr  14306  ccatlid  14654  swrdfv0  14719  swrdpfx  14778  pfxpfx  14779  cats1un  14792  swrdccatin2  14800  revpfxsfxrev  14839  cshwidx0mod  14878  cshw1  14895  relexpaddg  15128  rennim  15328  max0add  15399  fsumsplit  15829  sumsplit  15856  isumsplit  15931  arisum2  15952  binomfallfaclem2  16130  efaddlem  16183  eftlub  16201  ef4p  16205  rpnnen2lem11  16316  moddvds  16357  divalglem9  16495  sadadd2lem2  16544  sadcaddlem  16551  gcdmultipled  16628  pcmpt  16988  4sqlem11  17051  vdwlem6  17082  gsumsgrpccat  18950  mulgnn0dir  19228  sylow1lem1  19726  efgsval2  19861  efgsp1  19865  zaddablx  20000  pgpfaclem1  20211  regsumfsum  21649  regsumsupp  21836  mplcoe5  22257  nrmmetd  24801  blcvx  25025  xrsxmet  25037  reparphti  25226  nulmbl  25764  itg2splitlem  25977  itg2split  25978  itg2monolem1  25979  itgsplitioo  26067  ditgsplit  26090  dvcnp2  26149  dvcmul  26173  dvcmulf  26174  dvmptcmul  26193  dveflem  26208  dvef  26209  dvlipcn  26223  dvlt0  26234  plymullem1  26441  coeeulem  26451  dgradd2  26495  dgrmulc  26498  plydivlem3  26526  aareccl  26559  taylthlem1  26606  sin2kpi  26718  cos2kpi  26719  coshalfpim  26730  sinkpi  26757  chordthmlem3  27069  chordthmlem5  27071  dcubic1lem  27078  dcubic  27081  atancj  27145  atanlogaddlem  27148  atanlogsublem  27150  scvxcvx  27220  zetacvg  27249  ftalem5  27311  ftalem7  27313  basellem3  27317  chtublem  27445  2sqn0  27668  2sqnn  27673  rplogsumlem2  27719  dchrisumlem1  27723  pntrlog2bndlem2  27812  brbtwn2  29348  axlowdimlem16  29400  axeuclidlem  29405  elntg2  29428  eucrct2eupth  30711  2clwwlk2clwwlk  30816  re0cj  33201  bcm1n  33253  wrdt2ind  33382  nn0constr  34258  constraddcl  34259  constrnegcl  34260  constrdircl  34262  constrremulcl  34264  constrrecl  34266  constrimcl  34267  constrmulcl  34268  constrreinvcl  34269  constrinvcl  34270  constrresqrtcl  34274  constrabscl  34275  2sqr3minply  34277  cos9thpiminplylem1  34279  cos9thpiminply  34285  cos9thpinconstrlem1  34286  esumpfinvallem  34571  signsplypnf  35045  fsum2dsub  35102  logdivsqrle  35145  cvxpconn  35808  cvxsconn  35809  fwddifnp1  36732  tan2h  38353  poimirlem16  38372  mbfposadd  38403  itg2addnc  38410  ftc1anclem5  38433  bfplem2  38560  aks4d1p1p4  42924  aks4d1p7d1  42935  primrootspoweq0  42959  aks6d1c1  42969  aks6d1c5lem1  42989  sticksstones10  43008  sticksstones22  43021  bcle2d  43032  dffltz  43467  3cubeslem3r  43519  pellexlem6  43662  jm2.18  43816  sqrtcval  44468  relexpaddss  44545  int-add02d  45012  sub2times  46093  fzisoeu  46120  xralrple2  46171  cosknegpi  46684  dvsinax  46728  dvasinbx  46735  dvnxpaek  46757  dvnmul  46758  stoweidlem1  46816  stoweidlem13  46828  stoweidlem42  46857  stirlinglem5  46893  stirlinglem11  46899  fourierdlem42  46964  fourierdlem51  46972  fourierdlem88  47009  fourierdlem103  47024  fourierdlem104  47025  fourierdlem107  47028  sqwvfoura  47043  sqwvfourb  47044  fouriersw  47046  elaa2lem  47048  hspmbllem1  47441  cnambpcma  48169  readdcnnred  48178  gpg3kgrtriex  48992  nn0mnd  49081  altgsumbcALT  49270  nn0sumshdiglemA  49536  line2xlem  49670  line2x  49671  itschlc0yqe  49677  itsclc0yqsollem1  49679  itschlc0xyqsol1  49683  itschlc0xyqsol  49684  2itscp  49698  veronesev2lem  50794  veronesev3lem  50795  veronesev4lem  50796  veronesev5lem  50797  veronesev6lem  50798