Theorem addid1d 10843

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  (class class class)co 7159  ℂcc 10538  0cc0 10540   + caddc 10543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-resscn 10597  ax-1cn 10598  ax-icn 10599  ax-addcl 10600  ax-addrcl 10601  ax-mulcl 10602  ax-mulrcl 10603  ax-mulcom 10604  ax-addass 10605  ax-mulass 10606  ax-distr 10607  ax-i2m1 10608  ax-1ne0 10609  ax-1rid 10610  ax-rnegex 10611  ax-rrecex 10612  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615  ax-pre-ltadd 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-po 5477  df-so 5478  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-pnf 10680  df-mnf 10681  df-ltxr 10683

This theorem is referenced by:  ltaddneg  10858  subsub2  10917  negsub  10937  ltaddpos  11133  addge01  11153  add20  11155  nnge1  11668  nnnn0addcl  11930  un0addcl  11933  uzaddcl  12307  xaddid1  12637  fzosubel3  13101  expadd  13474  faclbnd4lem4  13659  faclbnd6  13662  hashgadd  13741  ccatrid  13944  pfxmpt  14043  pfxfv  14047  pfxswrd  14071  pfxccatin12lem1  14093  pfxccatin12lem2  14096  swrdccat3blem  14104  cshweqrep  14186  relexpaddg  14415  reim0b  14481  rereb  14482  immul2  14499  max0add  14673  iseraltlem2  15042  fsumsplit  15100  sumsplit  15126  binomfallfaclem2  15397  pwp1fsum  15745  bitsinv1lem  15793  sadadd2lem2  15802  sadcaddlem  15809  bezoutlem1  15890  pcadd  16228  pcadd2  16229  pcmpt  16231  vdwapun  16313  vdwlem1  16320  mulgnn0dir  18260  psgnunilem2  18626  sylow1lem1  18726  efginvrel2  18856  efgredleme  18872  efgcpbllemb  18884  frgpnabllem1  18996  mplcoe5  20252  regsumfsum  20616  regsumsupp  20769  xrsxmet  23420  reparphti  23604  minveclem6  24040  ovolunnul  24104  voliunlem3  24156  ovolioo  24172  itg2splitlem  24352  itg2split  24353  itgrevallem1  24398  itgsplitioo  24441  ditgsplit  24462  dvnadd  24529  dvlipcn  24594  ply1divex  24733  dvntaylp  24962  ulmshft  24981  abelthlem6  25027  cosmpi  25077  sinppi  25078  sinhalfpip  25081  logrnaddcl  25161  affineequiv  25404  chordthmlem3  25415  atanlogaddlem  25494  atanlogsublem  25496  leibpi  25523  scvxcvx  25566  dmgmn0  25606  lgamgulmlem2  25610  lgambdd  25617  logexprlim  25804  2sqblem  26010  2sq2  26012  2sqnn  26018  dchrvmasum2if  26076  dchrvmasumlem  26102  axcontlem8  26760  elntg2  26774  crctcshlem4  27601  eupth2lem3lem6  28015  ipidsq  28490  minvecolem6  28662  normpyc  28926  pjspansn  29357  lnfnmuli  29824  hstoh  30012  archirngz  30822  indsumin  31285  esumpfinvallem  31337  signsvtp  31857  signlem0  31861  fsum2dsub  31882  cvxpconn  32493  cvxsconn  32494  elmrsubrn  32771  faclim2  32984  fwddifn0  33629  fwddifnp1  33630  dnizeq0  33818  knoppndvlem6  33860  bj-bary1lem  34595  poimirlem1  34897  poimirlem5  34901  poimirlem6  34902  poimirlem7  34903  poimirlem11  34907  poimirlem12  34908  poimirlem17  34913  poimirlem20  34916  poimirlem22  34918  poimirlem24  34920  poimirlem25  34921  poimirlem29  34925  poimirlem31  34927  mblfinlem2  34934  mbfposadd  34943  itg2addnc  34950  itgaddnclem2  34955  ftc1anclem5  34975  ftc1anclem8  34978  areacirc  34991  3cubeslem2  39288  3cubeslem3r  39290  pell1qrgaplem  39476  jm2.19lem3  39594  jm2.25  39602  relexpaddss  40069  int-add01d  40543  binomcxplemnn0  40687  fperiodmullem  41576  xralrple3  41648  sumnnodd  41917  fprodaddrecnncnvlem  42199  ioodvbdlimc1lem2  42223  volioc  42263  volico  42275  stoweidlem11  42303  stoweidlem26  42318  stirlinglem12  42377  fourierdlem4  42403  fourierdlem42  42441  fourierdlem60  42458  fourierdlem61  42459  fourierdlem92  42490  fourierdlem107  42505  fouriersw  42523  etransclem24  42550  etransclem35  42561  hoidmvlelem2  42885  hspmbllem1  42915  sharhght  43129  deccarry  43518  nn0mnd  44093  altgsumbcALT  44408  eenglngeehlnmlem2  44732  line2y  44749  itschlc0xyqsol1  44760  itschlc0xyqsol  44761  2itscp  44775