Theorem addid1d 10676

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

Syntax hints:   → wi 4   = wceq 1520   ∈ wcel 2079  (class class class)co 7007  ℂcc 10370  0cc0 10372   + caddc 10375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-resscn 10429  ax-1cn 10430  ax-icn 10431  ax-addcl 10432  ax-addrcl 10433  ax-mulcl 10434  ax-mulrcl 10435  ax-mulcom 10436  ax-addass 10437  ax-mulass 10438  ax-distr 10439  ax-i2m1 10440  ax-1ne0 10441  ax-1rid 10442  ax-rnegex 10443  ax-rrecex 10444  ax-cnre 10445  ax-pre-lttri 10446  ax-pre-lttrn 10447  ax-pre-ltadd 10448

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-po 5354  df-so 5355  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-ov 7010  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-pnf 10512  df-mnf 10513  df-ltxr 10515

This theorem is referenced by:  ltaddneg  10691  subsub2  10751  negsub  10771  ltaddpos  10967  addge01  10987  add20  10989  nnge1  11502  nnnn0addcl  11764  un0addcl  11767  uzaddcl  12142  xaddid1  12473  fzosubel3  12936  expadd  13309  faclbnd4lem4  13494  faclbnd6  13497  hashgadd  13574  ccatrid  13773  pfxmpt  13864  pfxfv  13868  pfxswrd  13892  pfxccatin12lem1  13914  pfxccatin12lem2  13917  swrdccat3blem  13925  cshweqrep  14007  relexpaddg  14234  reim0b  14300  rereb  14301  immul2  14318  max0add  14492  iseraltlem2  14861  fsumsplit  14918  sumsplit  14944  binomfallfaclem2  15215  pwp1fsum  15563  bitsinv1lem  15611  sadadd2lem2  15620  sadcaddlem  15627  bezoutlem1  15704  pcadd  16042  pcadd2  16043  pcmpt  16045  vdwapun  16127  vdwlem1  16134  mulgnn0dir  17999  psgnunilem2  18342  sylow1lem1  18441  efginvrel2  18568  efgredleme  18584  efgcpbllemb  18596  frgpnabllem1  18704  mplcoe5  19924  regsumfsum  20283  regsumsupp  20436  xrsxmet  23088  reparphti  23272  minveclem6  23708  ovolunnul  23772  voliunlem3  23824  ovolioo  23840  itg2splitlem  24020  itg2split  24021  itgrevallem1  24066  itgsplitioo  24109  ditgsplit  24130  dvnadd  24197  dvlipcn  24262  ply1divex  24401  dvntaylp  24630  ulmshft  24649  abelthlem6  24695  cosmpi  24745  sinppi  24746  sinhalfpip  24749  logrnaddcl  24827  affineequiv  25070  chordthmlem3  25081  atanlogaddlem  25160  atanlogsublem  25162  leibpi  25190  scvxcvx  25233  dmgmn0  25273  lgamgulmlem2  25277  lgambdd  25284  logexprlim  25471  2sqblem  25677  2sq2  25679  2sqnn  25685  dchrvmasum2if  25743  dchrvmasumlem  25769  axcontlem8  26428  elntg2  26442  crctcshlem4  27273  eupth2lem3lem6  27688  ipidsq  28166  minvecolem6  28338  normpyc  28602  pjspansn  29033  lnfnmuli  29500  hstoh  29688  archirngz  30414  indsumin  30854  esumpfinvallem  30906  signsvtp  31426  signlem0  31430  fsum2dsub  31451  cvxpconn  32053  cvxsconn  32054  elmrsubrn  32320  faclim2  32533  fwddifn0  33179  fwddifnp1  33180  dnizeq0  33367  knoppndvlem6  33409  bj-bary1lem  34074  poimirlem1  34370  poimirlem5  34374  poimirlem6  34375  poimirlem7  34376  poimirlem11  34380  poimirlem12  34381  poimirlem17  34386  poimirlem20  34389  poimirlem22  34391  poimirlem24  34393  poimirlem25  34394  poimirlem29  34398  poimirlem31  34400  mblfinlem2  34407  mbfposadd  34416  itg2addnc  34423  itgaddnclem2  34428  ftc1anclem5  34448  ftc1anclem8  34451  areacirc  34464  pell1qrgaplem  38906  jm2.19lem3  39024  jm2.25  39032  relexpaddss  39499  int-add01d  39975  binomcxplemnn0  40171  fperiodmullem  41064  xralrple3  41136  sumnnodd  41407  fprodaddrecnncnvlem  41688  ioodvbdlimc1lem2  41712  volioc  41752  volico  41764  stoweidlem11  41792  stoweidlem26  41807  stirlinglem12  41866  fourierdlem4  41892  fourierdlem42  41930  fourierdlem60  41947  fourierdlem61  41948  fourierdlem92  41979  fourierdlem107  41994  fouriersw  42012  etransclem24  42039  etransclem35  42050  hoidmvlelem2  42374  hspmbllem1  42404  sharhght  42618  deccarry  42981  altgsumbcALT  43833  eenglngeehlnmlem2  44160  line2y  44177  itschlc0xyqsol1  44188  itschlc0xyqsol  44189  2itscp  44203