Theorem addlidd 11538

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  0cc0 11227   + caddc 11230

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-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375

This theorem is used by:  negeu  11574  subge0  11856  sublt0d  11969  un0addcl  12666  lincmb01cmp  13653  ico01fl0  13986  muladdmod  14082  discr  14411  ccatlid  14759  swrdfv0  14825  swrdpfx  14884  pfxpfx  14885  cats1un  14898  swrdccatin2  14906  revpfxsfxrev  14945  cshwidx0mod  14984  cshw1  15001  relexpaddg  15235  rennim  15435  max0add  15506  fsumsplit  15936  sumsplit  15963  isumsplit  16038  arisum2  16059  binomfallfaclem2  16235  efaddlem  16288  eftlub  16306  ef4p  16310  rpnnen2lem11  16421  moddvds  16462  divalglem9  16600  sadadd2lem2  16649  sadcaddlem  16656  gcdmultipled  16736  pcmpt  17099  4sqlem11  17162  vdwlem6  17193  gsumsgrpccat  19065  mulgnn0dir  19343  sylow1lem1  19842  efgsval2  19977  efgsp1  19981  zaddablx  20116  pgpfaclem1  20327  regsumfsum  21771  regsumsupp  21958  mplcoe5  22379  nrmmetd  24923  blcvx  25147  xrsxmet  25159  reparphti  25348  nulmbl  25886  itg2splitlem  26099  itg2split  26100  itg2monolem1  26101  itgsplitioo  26188  ditgsplit  26211  dvcnp2  26270  dvcmul  26294  dvcmulf  26295  dvmptcmul  26314  dveflem  26329  dvef  26330  dvlipcn  26344  dvlt0  26355  plymullem1  26563  coeeulem  26573  dgradd2  26617  dgrmulc  26620  plydivlem3  26646  aareccl  26683  taylthlem1  26730  sin2kpi  26842  cos2kpi  26843  coshalfpim  26854  sinkpi  26880  chordthmlem3  27192  chordthmlem5  27194  dcubic1lem  27201  dcubic  27204  atancj  27268  atanlogaddlem  27271  atanlogsublem  27273  scvxcvx  27343  zetacvg  27372  ftalem5  27434  ftalem7  27436  basellem3  27440  chtublem  27568  2sqn0  27791  2sqnn  27796  rplogsumlem2  27842  dchrisumlem1  27846  pntrlog2bndlem2  27935  brbtwn2  29513  axlowdimlem16  29565  axeuclidlem  29570  elntg2  29593  eucrct2eupth  30876  2clwwlk2clwwlk  30981  re0cj  33405  bcm1n  33457  wrdt2ind  33586  nn0constr  34463  constraddcl  34464  constrnegcl  34465  constrdircl  34467  constrremulcl  34469  constrrecl  34471  constrimcl  34472  constrmulcl  34473  constrreinvcl  34474  constrinvcl  34475  constrresqrtcl  34479  constrabscl  34480  2sqr3minply  34482  cos9thpiminplylem1  34484  cos9thpiminply  34490  cos9thpinconstrlem1  34491  esumpfinvallem  34776  signsplypnf  35249  fsum2dsub  35306  logdivsqrle  35349  cvxpconn  36174  cvxsconn  36175  fwddifnp1  37108  tan2h  38727  poimirlem16  38746  mbfposadd  38777  itg2addnc  38784  ftc1anclem5  38807  bfplem2  38949  aks4d1p1p4  43313  aks4d1p7d1  43324  primrootspoweq0  43348  aks6d1c1  43358  aks6d1c5lem1  43378  sticksstones10  43397  sticksstones22  43410  bcle2d  43421  dffltz  43863  3cubeslem3r  43890  pellexlem6  44034  jm2.18  44188  sqrtcval  44833  relexpaddss  44910  int-add02d  45377  sub2times  46494  fzisoeu  46521  xralrple2  46571  cosknegpi  47084  dvsinax  47128  dvasinbx  47135  dvnxpaek  47157  dvnmul  47158  stoweidlem1  47216  stoweidlem13  47228  stoweidlem42  47257  stirlinglem5  47293  stirlinglem11  47299  fourierdlem42  47364  fourierdlem51  47372  fourierdlem88  47409  fourierdlem103  47424  fourierdlem104  47425  fourierdlem107  47428  sqwvfoura  47443  sqwvfourb  47444  fouriersw  47446  elaa2lem  47448  hspmbllem1  47841  cnambpcma  48569  readdcnnred  48578  gpg3kgrtriex  49392  nn0mnd  49481  altgsumbcALT  49670  nn0sumshdiglemA  49936  line2xlem  50070  line2x  50071  itschlc0yqe  50077  itsclc0yqsollem1  50079  itschlc0xyqsol1  50083  itschlc0xyqsol  50084  2itscp  50098  veronesev2lem  51254  veronesev3lem  51255  veronesev4lem  51256  veronesev5lem  51257  veronesev6lem  51258