Theorem addlidd 11336

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7356  ℂcc 11025  0cc0 11027   + caddc 11030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  negeu  11372  subge0  11652  sublt0d  11765  un0addcl  12459  lincmb01cmp  13437  ico01fl0  13767  muladdmod  13863  discr  14191  ccatlid  14538  swrdfv0  14601  swrdpfx  14658  pfxpfx  14659  cats1un  14672  swrdccatin2  14680  cshwidx0mod  14756  cshw1  14773  relexpaddg  15004  rennim  15190  max0add  15261  fsumsplit  15692  sumsplit  15719  isumsplit  15794  arisum2  15815  binomfallfaclem2  15994  efaddlem  16047  eftlub  16065  ef4p  16069  rpnnen2lem11  16180  moddvds  16221  divalglem9  16359  sadadd2lem2  16408  sadcaddlem  16415  gcdmultipled  16492  pcmpt  16852  4sqlem11  16915  vdwlem6  16946  gsumsgrpccat  18797  mulgnn0dir  19069  sylow1lem1  19562  efgsval2  19697  efgsp1  19701  zaddablx  19836  pgpfaclem1  20047  regsumfsum  21404  regsumsupp  21591  mplcoe5  22007  nrmmetd  24527  blcvx  24751  xrsxmet  24763  reparphti  24952  nulmbl  25490  itg2splitlem  25703  itg2split  25704  itg2monolem1  25705  itgsplitioo  25793  ditgsplit  25816  dvcnp2  25875  dvcmul  25899  dvcmulf  25900  dvmptcmul  25919  dveflem  25934  dvef  25935  dvlipcn  25949  dvlt0  25960  plymullem1  26167  coeeulem  26177  dgradd2  26221  dgrmulc  26224  plydivlem3  26249  aareccl  26280  taylthlem1  26326  sin2kpi  26435  cos2kpi  26436  coshalfpim  26447  sinkpi  26474  chordthmlem3  26786  chordthmlem5  26788  dcubic1lem  26795  dcubic  26798  atancj  26862  atanlogaddlem  26865  atanlogsublem  26867  scvxcvx  26937  zetacvg  26966  ftalem5  27028  ftalem7  27030  basellem3  27034  chtublem  27162  2sqn0  27385  2sqnn  27390  rplogsumlem2  27436  dchrisumlem1  27440  pntrlog2bndlem2  27529  brbtwn2  28962  axlowdimlem16  29014  axeuclidlem  29019  elntg2  29042  eucrct2eupth  30303  2clwwlk2clwwlk  30408  re0cj  32804  bcm1n  32856  wrdt2ind  33001  nn0constr  33893  constraddcl  33894  constrnegcl  33895  constrdircl  33897  constrremulcl  33899  constrrecl  33901  constrimcl  33902  constrmulcl  33903  constrreinvcl  33904  constrinvcl  33905  constrresqrtcl  33909  constrabscl  33910  2sqr3minply  33912  cos9thpiminplylem1  33914  cos9thpiminply  33920  cos9thpinconstrlem1  33921  esumpfinvallem  34206  signsplypnf  34682  fsum2dsub  34739  logdivsqrle  34782  revpfxsfxrev  35286  cvxpconn  35412  cvxsconn  35413  fwddifnp1  36335  tan2h  37921  poimirlem16  37945  mbfposadd  37976  itg2addnc  37983  ftc1anclem5  38006  bfplem2  38132  aks4d1p1p4  42498  aks4d1p7d1  42509  primrootspoweq0  42533  aks6d1c1  42543  aks6d1c5lem1  42563  sticksstones10  42582  sticksstones22  42595  bcle2d  42606  dffltz  43055  3cubeslem3r  43107  pellexlem6  43250  jm2.18  43404  sqrtcval  44056  relexpaddss  44133  int-add02d  44600  sub2times  45694  fzisoeu  45721  xralrple2  45772  cosknegpi  46285  dvsinax  46329  dvasinbx  46336  dvnxpaek  46358  dvnmul  46359  stoweidlem1  46417  stoweidlem13  46429  stoweidlem42  46458  stirlinglem5  46494  stirlinglem11  46500  fourierdlem42  46565  fourierdlem51  46573  fourierdlem88  46610  fourierdlem103  46625  fourierdlem104  46626  fourierdlem107  46629  sqwvfoura  46644  sqwvfourb  46645  fouriersw  46647  elaa2lem  46649  hspmbllem1  47042  cnambpcma  47730  readdcnnred  47739  gpg3kgrtriex  48553  nn0mnd  48643  altgsumbcALT  48817  nn0sumshdiglemA  49083  line2xlem  49217  line2x  49218  itschlc0yqe  49224  itsclc0yqsollem1  49226  itschlc0xyqsol1  49230  itschlc0xyqsol  49231  2itscp  49245