Theorem addridd 11410

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7401  ℂcc 11103  0cc0 11105   + caddc 11108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-po 5578  df-so 5579  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  ltaddneg  11425  subsub2  11484  negsub  11504  ltaddpos  11700  addge01  11720  add20  11722  nnge1  12236  nnnn0addcl  12498  un0addcl  12501  uzaddcl  12884  xaddrid  13216  fzosubel3  13689  expadd  14066  faclbnd4lem4  14252  faclbnd6  14255  hashgadd  14333  ccatrid  14533  pfxmpt  14624  pfxfv  14628  pfxswrd  14652  pfxccatin12lem1  14674  pfxccatin12lem2  14677  swrdccat3blem  14685  cshweqrep  14767  relexpaddg  14996  reim0b  15062  rereb  15063  immul2  15080  max0add  15253  iseraltlem2  15625  fsumsplit  15683  sumsplit  15710  binomfallfaclem2  15980  pwp1fsum  16330  bitsinv1lem  16378  sadadd2lem2  16387  sadcaddlem  16394  bezoutlem1  16477  pcadd  16820  pcadd2  16821  pcmpt  16823  vdwapun  16905  vdwlem1  16912  mulgnn0dir  19020  psgnunilem2  19404  sylow1lem1  19507  efginvrel2  19636  efgredleme  19652  efgcpbllemb  19664  frgpnabllem1  19782  regsumfsum  21296  pzriprnglem10  21344  regsumsupp  21482  mplcoe5  21904  xrsxmet  24646  reparphti  24844  reparphtiOLD  24845  cphpyth  25065  minveclem6  25283  ovolunnul  25350  voliunlem3  25402  ovolioo  25418  itg2splitlem  25599  itg2split  25600  itgrevallem1  25645  itgsplitioo  25688  ditgsplit  25711  dvnadd  25780  dvlipcn  25848  ply1divex  25993  dvntaylp  26223  ulmshft  26242  abelthlem6  26289  cosmpi  26339  sinppi  26340  sinhalfpip  26343  logrnaddcl  26424  affineequiv  26670  chordthmlem3  26681  atanlogaddlem  26760  atanlogsublem  26762  leibpi  26789  scvxcvx  26833  dmgmn0  26873  lgamgulmlem2  26877  lgambdd  26884  logexprlim  27073  2sqblem  27279  2sq2  27281  2sqnn  27287  dchrvmasum2if  27345  dchrvmasumlem  27371  axcontlem8  28664  elntg2  28678  crctcshlem4  29509  eupth2lem3lem6  29921  ipidsq  30398  minvecolem6  30570  normpyc  30834  pjspansn  31265  lnfnmuli  31732  hstoh  31920  archirngz  32769  indsumin  33475  esumpfinvallem  33527  signsvtp  34049  signlem0  34053  fsum2dsub  34074  cvxpconn  34688  cvxsconn  34689  elmrsubrn  34966  faclim2  35179  fwddifn0  35597  fwddifnp1  35598  dnizeq0  35807  knoppndvlem6  35849  bj-bary1lem  36647  poimirlem1  36945  poimirlem5  36949  poimirlem6  36950  poimirlem7  36951  poimirlem11  36955  poimirlem12  36956  poimirlem17  36961  poimirlem20  36964  poimirlem22  36966  poimirlem24  36968  poimirlem25  36969  poimirlem29  36973  poimirlem31  36975  mblfinlem2  36982  mbfposadd  36991  itg2addnc  36998  itgaddnclem2  37003  ftc1anclem5  37021  ftc1anclem8  37024  areacirc  37037  lcmineqlem4  41356  lcmineqlem18  41370  aks4d1p1p7  41398  aks4d1p3  41402  sticksstones10  41430  sticksstones12a  41432  metakunt29  41472  metakunt30  41473  3cubeslem2  41878  3cubeslem3r  41880  pell1qrgaplem  42066  jm2.19lem3  42185  jm2.25  42193  relexpaddss  42924  int-add01d  43391  binomcxplemnn0  43563  fperiodmullem  44464  xralrple3  44535  sumnnodd  44797  fprodaddrecnncnvlem  45076  ioodvbdlimc1lem2  45099  volioc  45139  volico  45150  stoweidlem11  45178  stoweidlem26  45193  stirlinglem12  45252  fourierdlem4  45278  fourierdlem42  45316  fourierdlem60  45333  fourierdlem61  45334  fourierdlem92  45365  fourierdlem107  45380  fouriersw  45398  etransclem24  45425  etransclem35  45436  hoidmvlelem2  45763  hspmbllem1  45793  sharhght  46032  deccarry  46470  nn0mnd  47008  altgsumbcALT  47184  itcovalpclem1  47510  eenglngeehlnmlem2  47578  line2y  47595  itschlc0xyqsol1  47606  itschlc0xyqsol  47607  2itscp  47621