Theorem addlidd 11512

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11199  0cc0 11201   + caddc 11204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-dif 4047  df-in 4091  df-un 4151  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 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11346  df-mnf 11347  df-ltxr 11349

This theorem is used by:  negeu  11548  subge0  11830  sublt0d  11943  un0addcl  12640  lincmb01cmp  13627  ico01fl0  13960  muladdmod  14056  discr  14385  ccatlid  14733  swrdfv0  14798  swrdpfx  14857  pfxpfx  14858  cats1un  14871  swrdccatin2  14879  revpfxsfxrev  14918  cshwidx0mod  14957  cshw1  14974  relexpaddg  15207  rennim  15407  max0add  15478  fsumsplit  15908  sumsplit  15935  isumsplit  16010  arisum2  16031  binomfallfaclem2  16207  efaddlem  16260  eftlub  16278  ef4p  16282  rpnnen2lem11  16393  moddvds  16434  divalglem9  16572  sadadd2lem2  16621  sadcaddlem  16628  gcdmultipled  16708  pcmpt  17071  4sqlem11  17134  vdwlem6  17165  gsumsgrpccat  19037  mulgnn0dir  19315  sylow1lem1  19813  efgsval2  19948  efgsp1  19952  zaddablx  20087  pgpfaclem1  20298  regsumfsum  21742  regsumsupp  21929  mplcoe5  22350  nrmmetd  24894  blcvx  25118  xrsxmet  25130  reparphti  25319  nulmbl  25857  itg2splitlem  26070  itg2split  26071  itg2monolem1  26072  itgsplitioo  26159  ditgsplit  26182  dvcnp2  26241  dvcmul  26265  dvcmulf  26266  dvmptcmul  26285  dveflem  26300  dvef  26301  dvlipcn  26315  dvlt0  26326  plymullem1  26534  coeeulem  26544  dgradd2  26588  dgrmulc  26591  plydivlem3  26617  aareccl  26654  taylthlem1  26701  sin2kpi  26813  cos2kpi  26814  coshalfpim  26825  sinkpi  26851  chordthmlem3  27163  chordthmlem5  27165  dcubic1lem  27172  dcubic  27175  atancj  27239  atanlogaddlem  27242  atanlogsublem  27244  scvxcvx  27314  zetacvg  27343  ftalem5  27405  ftalem7  27407  basellem3  27411  chtublem  27539  2sqn0  27762  2sqnn  27767  rplogsumlem2  27813  dchrisumlem1  27817  pntrlog2bndlem2  27906  brbtwn2  29484  axlowdimlem16  29536  axeuclidlem  29541  elntg2  29564  eucrct2eupth  30847  2clwwlk2clwwlk  30952  re0cj  33378  bcm1n  33430  wrdt2ind  33559  nn0constr  34436  constraddcl  34437  constrnegcl  34438  constrdircl  34440  constrremulcl  34442  constrrecl  34444  constrimcl  34445  constrmulcl  34446  constrreinvcl  34447  constrinvcl  34448  constrresqrtcl  34452  constrabscl  34453  2sqr3minply  34455  cos9thpiminplylem1  34457  cos9thpiminply  34463  cos9thpinconstrlem1  34464  esumpfinvallem  34749  signsplypnf  35222  fsum2dsub  35279  logdivsqrle  35322  cvxpconn  36050  cvxsconn  36051  fwddifnp1  36973  tan2h  38579  poimirlem16  38598  mbfposadd  38629  itg2addnc  38636  ftc1anclem5  38659  bfplem2  38801  aks4d1p1p4  43165  aks4d1p7d1  43176  primrootspoweq0  43200  aks6d1c1  43210  aks6d1c5lem1  43230  sticksstones10  43249  sticksstones22  43262  bcle2d  43273  dffltz  43714  3cubeslem3r  43741  pellexlem6  43885  jm2.18  44039  sqrtcval  44685  relexpaddss  44762  int-add02d  45229  sub2times  46333  fzisoeu  46360  xralrple2  46410  cosknegpi  46923  dvsinax  46967  dvasinbx  46974  dvnxpaek  46996  dvnmul  46997  stoweidlem1  47055  stoweidlem13  47067  stoweidlem42  47096  stirlinglem5  47132  stirlinglem11  47138  fourierdlem42  47203  fourierdlem51  47211  fourierdlem88  47248  fourierdlem103  47263  fourierdlem104  47264  fourierdlem107  47267  sqwvfoura  47282  sqwvfourb  47283  fouriersw  47285  elaa2lem  47287  hspmbllem1  47680  cnambpcma  48408  readdcnnred  48417  gpg3kgrtriex  49231  nn0mnd  49320  altgsumbcALT  49509  nn0sumshdiglemA  49775  line2xlem  49909  line2x  49910  itschlc0yqe  49916  itsclc0yqsollem1  49918  itschlc0xyqsol1  49922  itschlc0xyqsol  49923  2itscp  49937  veronesev2lem  51018  veronesev3lem  51019  veronesev4lem  51020  veronesev5lem  51021  veronesev6lem  51022