Theorem addid1d 10997

Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addid1d	⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Proof of Theorem addid1d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addid1 10977	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692  0cc0 10694   + caddc 10697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-po 5453  df-so 5454  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-ltxr 10837

This theorem is referenced by:  ltaddneg  11012  subsub2  11071  negsub  11091  ltaddpos  11287  addge01  11307  add20  11309  nnge1  11823  nnnn0addcl  12085  un0addcl  12088  uzaddcl  12465  xaddid1  12796  fzosubel3  13268  expadd  13642  faclbnd4lem4  13827  faclbnd6  13830  hashgadd  13909  ccatrid  14109  pfxmpt  14208  pfxfv  14212  pfxswrd  14236  pfxccatin12lem1  14258  pfxccatin12lem2  14261  swrdccat3blem  14269  cshweqrep  14351  relexpaddg  14581  reim0b  14647  rereb  14648  immul2  14665  max0add  14839  iseraltlem2  15211  fsumsplit  15269  sumsplit  15295  binomfallfaclem2  15565  pwp1fsum  15915  bitsinv1lem  15963  sadadd2lem2  15972  sadcaddlem  15979  bezoutlem1  16062  pcadd  16405  pcadd2  16406  pcmpt  16408  vdwapun  16490  vdwlem1  16497  mulgnn0dir  18475  psgnunilem2  18841  sylow1lem1  18941  efginvrel2  19071  efgredleme  19087  efgcpbllemb  19099  frgpnabllem1  19212  regsumfsum  20385  regsumsupp  20538  mplcoe5  20951  xrsxmet  23660  reparphti  23848  cphpyth  24067  minveclem6  24285  ovolunnul  24351  voliunlem3  24403  ovolioo  24419  itg2splitlem  24600  itg2split  24601  itgrevallem1  24646  itgsplitioo  24689  ditgsplit  24712  dvnadd  24780  dvlipcn  24845  ply1divex  24988  dvntaylp  25217  ulmshft  25236  abelthlem6  25282  cosmpi  25332  sinppi  25333  sinhalfpip  25336  logrnaddcl  25417  affineequiv  25660  chordthmlem3  25671  atanlogaddlem  25750  atanlogsublem  25752  leibpi  25779  scvxcvx  25822  dmgmn0  25862  lgamgulmlem2  25866  lgambdd  25873  logexprlim  26060  2sqblem  26266  2sq2  26268  2sqnn  26274  dchrvmasum2if  26332  dchrvmasumlem  26358  axcontlem8  27016  elntg2  27030  crctcshlem4  27858  eupth2lem3lem6  28270  ipidsq  28745  minvecolem6  28917  normpyc  29181  pjspansn  29612  lnfnmuli  30079  hstoh  30267  archirngz  31116  indsumin  31656  esumpfinvallem  31708  signsvtp  32228  signlem0  32232  fsum2dsub  32253  cvxpconn  32871  cvxsconn  32872  elmrsubrn  33149  faclim2  33383  fwddifn0  34152  fwddifnp1  34153  dnizeq0  34341  knoppndvlem6  34383  bj-bary1lem  35164  poimirlem1  35464  poimirlem5  35468  poimirlem6  35469  poimirlem7  35470  poimirlem11  35474  poimirlem12  35475  poimirlem17  35480  poimirlem20  35483  poimirlem22  35485  poimirlem24  35487  poimirlem25  35488  poimirlem29  35492  poimirlem31  35494  mblfinlem2  35501  mbfposadd  35510  itg2addnc  35517  itgaddnclem2  35522  ftc1anclem5  35540  ftc1anclem8  35543  areacirc  35556  lcmineqlem4  39723  lcmineqlem18  39737  aks4d1p1p7  39764  sticksstones10  39780  sticksstones12a  39782  metakunt29  39816  metakunt30  39817  3cubeslem2  40151  3cubeslem3r  40153  pell1qrgaplem  40339  jm2.19lem3  40457  jm2.25  40465  relexpaddss  40944  int-add01d  41414  binomcxplemnn0  41581  fperiodmullem  42456  xralrple3  42527  sumnnodd  42789  fprodaddrecnncnvlem  43068  ioodvbdlimc1lem2  43091  volioc  43131  volico  43142  stoweidlem11  43170  stoweidlem26  43185  stirlinglem12  43244  fourierdlem4  43270  fourierdlem42  43308  fourierdlem60  43325  fourierdlem61  43326  fourierdlem92  43357  fourierdlem107  43372  fouriersw  43390  etransclem24  43417  etransclem35  43428  hoidmvlelem2  43752  hspmbllem1  43782  sharhght  43996  deccarry  44419  nn0mnd  44989  altgsumbcALT  45305  itcovalpclem1  45632  eenglngeehlnmlem2  45700  line2y  45717  itschlc0xyqsol1  45728  itschlc0xyqsol  45729  2itscp  45743