Theorem addlidd 11306

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996  0cc0 10998   + caddc 11001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11140  df-mnf 11141  df-ltxr 11143

This theorem is referenced by:  negeu  11342  subge0  11622  sublt0d  11735  un0addcl  12406  lincmb01cmp  13387  ico01fl0  13715  muladdmod  13811  discr  14139  ccatlid  14486  swrdfv0  14549  swrdpfx  14606  pfxpfx  14607  cats1un  14620  swrdccatin2  14628  cshwidx0mod  14704  cshw1  14721  relexpaddg  14952  rennim  15138  max0add  15209  fsumsplit  15640  sumsplit  15667  isumsplit  15739  arisum2  15760  binomfallfaclem2  15939  efaddlem  15992  eftlub  16010  ef4p  16014  rpnnen2lem11  16125  moddvds  16166  divalglem9  16304  sadadd2lem2  16353  sadcaddlem  16360  gcdmultipled  16437  pcmpt  16796  4sqlem11  16859  vdwlem6  16890  gsumsgrpccat  18740  mulgnn0dir  19009  sylow1lem1  19503  efgsval2  19638  efgsp1  19642  zaddablx  19777  pgpfaclem1  19988  regsumfsum  21365  regsumsupp  21552  mplcoe5  21968  nrmmetd  24482  blcvx  24706  xrsxmet  24718  reparphti  24916  reparphtiOLD  24917  nulmbl  25456  itg2splitlem  25669  itg2split  25670  itg2monolem1  25671  itgsplitioo  25759  ditgsplit  25782  dvcnp2  25841  dvcnp2OLD  25842  dvcmul  25867  dvcmulf  25868  dvmptcmul  25888  dveflem  25903  dvef  25904  dvlipcn  25919  dvlt0  25930  plymullem1  26139  coeeulem  26149  dgradd2  26194  dgrmulc  26197  plydivlem3  26223  aareccl  26254  taylthlem1  26301  sin2kpi  26412  cos2kpi  26413  coshalfpim  26424  sinkpi  26451  chordthmlem3  26764  chordthmlem5  26766  dcubic1lem  26773  dcubic  26776  atancj  26840  atanlogaddlem  26843  atanlogsublem  26845  scvxcvx  26916  zetacvg  26945  ftalem5  27007  ftalem7  27009  basellem3  27013  chtublem  27142  2sqn0  27365  2sqnn  27370  rplogsumlem2  27416  dchrisumlem1  27420  pntrlog2bndlem2  27509  brbtwn2  28876  axlowdimlem16  28928  axeuclidlem  28933  elntg2  28956  eucrct2eupth  30215  2clwwlk2clwwlk  30320  re0cj  32717  bcm1n  32767  wrdt2ind  32924  nn0constr  33764  constraddcl  33765  constrnegcl  33766  constrdircl  33768  constrremulcl  33770  constrrecl  33772  constrimcl  33773  constrmulcl  33774  constrreinvcl  33775  constrinvcl  33776  constrresqrtcl  33780  constrabscl  33781  2sqr3minply  33783  cos9thpiminplylem1  33785  cos9thpiminply  33791  cos9thpinconstrlem1  33792  esumpfinvallem  34077  signsplypnf  34553  fsum2dsub  34610  logdivsqrle  34653  revpfxsfxrev  35128  cvxpconn  35254  cvxsconn  35255  fwddifnp1  36178  tan2h  37631  poimirlem16  37655  mbfposadd  37686  itg2addnc  37693  ftc1anclem5  37716  bfplem2  37842  aks4d1p1p4  42083  aks4d1p7d1  42094  primrootspoweq0  42118  aks6d1c1  42128  aks6d1c5lem1  42148  sticksstones10  42167  sticksstones22  42180  bcle2d  42191  dffltz  42646  3cubeslem3r  42699  pellexlem6  42846  jm2.18  43000  sqrtcval  43653  relexpaddss  43730  int-add02d  44197  sub2times  45293  fzisoeu  45320  xralrple2  45372  cosknegpi  45886  dvsinax  45930  dvasinbx  45937  dvnxpaek  45959  dvnmul  45960  stoweidlem1  46018  stoweidlem13  46030  stoweidlem42  46059  stirlinglem5  46095  stirlinglem11  46101  fourierdlem42  46166  fourierdlem51  46174  fourierdlem88  46211  fourierdlem103  46226  fourierdlem104  46227  fourierdlem107  46230  sqwvfoura  46245  sqwvfourb  46246  fouriersw  46248  elaa2lem  46250  hspmbllem1  46643  cnambpcma  47304  readdcnnred  47313  gpg3kgrtriex  48099  nn0mnd  48189  altgsumbcALT  48363  nn0sumshdiglemA  48630  line2xlem  48764  line2x  48765  itschlc0yqe  48771  itsclc0yqsollem1  48773  itschlc0xyqsol1  48777  itschlc0xyqsol  48778  2itscp  48792