Theorem addridd 11510

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

Hypothesis

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

Assertion

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

Proof of Theorem addridd

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addrid 11490	. 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 11198  0cc0 11200   + caddc 11203

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 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

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 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348

This theorem is used by:  ltaddneg  11526  subsub2  11586  negsub  11606  ltaddpos  11806  addge01  11826  add20  11828  nnge1  12366  nnnn0addcl  12636  un0addcl  12639  uzaddcl  13031  xaddrid  13371  fzosubel3  13861  expadd  14247  faclbnd4lem4  14440  faclbnd6  14443  hashgadd  14521  ccatrid  14733  pfxmpt  14828  pfxfv  14832  pfxswrd  14855  pfxccatin12lem1  14877  pfxccatin12lem2  14880  swrdccat3blem  14888  cshweqrep  14972  relexpaddg  15206  reim0b  15286  rereb  15287  immul2  15304  max0add  15477  iseraltlem2  15850  fsumsplit  15907  sumsplit  15934  binomfallfaclem2  16206  pwp1fsum  16561  bitsinv1lem  16611  sadadd2lem2  16620  sadcaddlem  16627  bezoutlem1  16712  pcadd  17067  pcadd2  17068  pcmpt  17070  vdwapun  17152  vdwlem1  17159  chnccat  18800  mulgnn0dir  19314  psgnunilem2  19709  sylow1lem1  19812  efginvrel2  19941  efgredleme  19957  efgcpbllemb  19969  frgpnabllem1  20087  regsumfsum  21741  pzriprnglem10  21796  regsumsupp  21928  mplcoe5  22349  psdmul  22487  xrsxmet  25129  reparphti  25318  cphpyth  25537  minveclem6  25755  ovolunnul  25821  voliunlem3  25873  ovolioo  25889  itg2splitlem  26069  itg2split  26070  itgrevallem1  26115  itgsplitioo  26158  ditgsplit  26181  dvnadd  26249  dvlipcn  26314  ply1divex  26455  dvntaylp  26698  ulmshft  26717  abelthlem6  26763  cosmpi  26817  sinppi  26818  sinhalfpip  26821  logrnaddcl  26902  affineequiv  27151  chordthmlem3  27162  atanlogaddlem  27241  atanlogsublem  27243  leibpi  27270  scvxcvx  27313  dmgmn0  27353  lgamgulmlem2  27357  lgambdd  27364  logexprlim  27552  2sqblem  27758  2sq2  27760  2sqnn  27766  dchrvmasum2if  27824  dchrvmasumlem  27850  axcontlem8  29549  elntg2  29563  crctcshlem4  30409  eupth2lem3lem6  30834  ipidsq  31312  minvecolem6  31484  normpyc  31748  pjspansn  32179  lnfnmuli  32646  hstoh  32834  indsumin  33470  archirngz  33792  constrrtlc2  34407  constrsslem  34415  2sqr3minply  34454  cos9thpiminply  34462  esumpfinvallem  34748  signsvtp  35254  signlem0  35258  fsum2dsub  35278  cvxpconn  36049  cvxsconn  36050  elmrsubrn  36327  faclim2  36555  fwddifn0  36971  fwddifnp1  36972  dnizeq0  37383  knoppndvlem6  37425  bj-bary1lem  38274  poimirlem1  38582  poimirlem5  38586  poimirlem6  38587  poimirlem7  38588  poimirlem11  38592  poimirlem12  38593  poimirlem17  38598  poimirlem20  38601  poimirlem22  38603  poimirlem24  38605  poimirlem25  38606  poimirlem29  38610  poimirlem31  38612  mblfinlem2  38619  mbfposadd  38628  itg2addnc  38635  itgaddnclem2  38640  ftc1anclem5  38658  ftc1anclem8  38661  areacirc  38674  lcmineqlem4  43125  lcmineqlem18  43139  aks4d1p1p7  43167  aks4d1p3  43171  posbezout  43193  primrootspoweq0  43199  sticksstones10  43248  sticksstones12a  43250  unitscyglem5  43292  3cubeslem2  43738  3cubeslem3r  43740  pell1qrgaplem  43923  jm2.19lem3  44041  jm2.25  44049  relexpaddss  44761  int-add01d  45227  binomcxplemnn0  45376  fperiodmullem  46362  xralrple3  46428  sumnnodd  46685  fprodaddrecnncnvlem  46962  ioodvbdlimc1lem2  46985  volioc  47025  volico  47036  stoweidlem11  47064  stoweidlem26  47079  stirlinglem12  47138  fourierdlem4  47164  fourierdlem42  47202  fourierdlem60  47219  fourierdlem61  47220  fourierdlem92  47251  fourierdlem107  47266  fouriersw  47284  etransclem24  47311  etransclem35  47322  hoidmvlelem2  47649  hspmbllem1  47679  sharhght  47918  deccarry  48424  flmrecm1  48456  nn0mnd  49319  altgsumbcALT  49508  itcovalpclem1  49825  eenglngeehlnmlem2  49893  line2y  49910  itschlc0xyqsol1  49921  itschlc0xyqsol  49922  2itscp  49936  veronesev1lem  51016  veronesev2lem  51017  veronesev3lem  51018  veronesev4lem  51019  veronesev5lem  51020  veronesev6lem  51021