Theorem addridd 11537

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  0cc0 11227   + caddc 11230

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375

This theorem is used by:  ltaddneg  11553  subsub2  11613  negsub  11633  ltaddpos  11833  addge01  11853  add20  11855  nnge1  12393  nnnn0addcl  12663  un0addcl  12666  uzaddcl  13058  xaddrid  13398  fzosubel3  13888  expadd  14274  faclbnd4lem4  14467  faclbnd6  14470  hashgadd  14548  ccatrid  14760  pfxmpt  14856  pfxfv  14860  pfxswrd  14883  pfxccatin12lem1  14905  pfxccatin12lem2  14908  swrdccat3blem  14916  cshweqrep  15000  relexpaddg  15235  reim0b  15315  rereb  15316  immul2  15333  max0add  15506  iseraltlem2  15879  fsumsplit  15936  sumsplit  15963  binomfallfaclem2  16235  pwp1fsum  16590  bitsinv1lem  16640  sadadd2lem2  16649  sadcaddlem  16656  bezoutlem1  16741  pcadd  17096  pcadd2  17097  pcmpt  17099  vdwapun  17181  vdwlem1  17188  chnccat  18829  mulgnn0dir  19343  psgnunilem2  19739  sylow1lem1  19842  efginvrel2  19971  efgredleme  19987  efgcpbllemb  19999  frgpnabllem1  20117  regsumfsum  21771  pzriprnglem10  21826  regsumsupp  21958  mplcoe5  22379  psdmul  22517  xrsxmet  25159  reparphti  25348  cphpyth  25567  minveclem6  25785  ovolunnul  25851  voliunlem3  25903  ovolioo  25919  itg2splitlem  26099  itg2split  26100  itgrevallem1  26145  itgsplitioo  26188  ditgsplit  26211  dvnadd  26279  dvlipcn  26344  ply1divex  26485  dvntaylp  26728  ulmshft  26747  abelthlem6  26793  cosmpi  26847  sinppi  26848  sinhalfpip  26851  logrnaddcl  26932  affineequiv  27181  chordthmlem3  27192  atanlogaddlem  27271  atanlogsublem  27273  leibpi  27300  scvxcvx  27343  dmgmn0  27383  lgamgulmlem2  27387  lgambdd  27394  logexprlim  27582  2sqblem  27788  2sq2  27790  2sqnn  27796  dchrvmasum2if  27854  dchrvmasumlem  27880  axcontlem8  29579  elntg2  29593  crctcshlem4  30439  eupth2lem3lem6  30864  ipidsq  31342  minvecolem6  31514  normpyc  31778  pjspansn  32209  lnfnmuli  32676  hstoh  32864  indsumin  33498  archirngz  33820  constrrtlc2  34435  constrsslem  34443  2sqr3minply  34482  cos9thpiminply  34490  esumpfinvallem  34776  signsvtp  35282  signlem0  35286  fsum2dsub  35306  cvxpconn  36174  cvxsconn  36175  elmrsubrn  36452  faclim2  36691  fwddifn0  37107  fwddifnp1  37108  dnizeq0  37519  knoppndvlem6  37561  bj-bary1lem  38423  poimirlem1  38731  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem11  38741  poimirlem12  38742  poimirlem17  38747  poimirlem20  38750  poimirlem22  38752  poimirlem24  38754  poimirlem25  38755  poimirlem29  38759  poimirlem31  38761  mblfinlem2  38768  mbfposadd  38777  itg2addnc  38784  itgaddnclem2  38789  ftc1anclem5  38807  ftc1anclem8  38810  areacirc  38823  lcmineqlem4  43274  lcmineqlem18  43288  aks4d1p1p7  43316  aks4d1p3  43320  posbezout  43342  primrootspoweq0  43348  sticksstones10  43397  sticksstones12a  43399  unitscyglem5  43441  3cubeslem2  43888  3cubeslem3r  43890  pell1qrgaplem  44073  jm2.19lem3  44191  jm2.25  44199  relexpaddss  44910  int-add01d  45376  binomcxplemnn0  45525  fperiodmullem  46524  xralrple3  46590  sumnnodd  46847  fprodaddrecnncnvlem  47124  ioodvbdlimc1lem2  47147  volioc  47187  volico  47198  stoweidlem11  47226  stoweidlem26  47241  stirlinglem12  47300  fourierdlem4  47326  fourierdlem42  47364  fourierdlem60  47381  fourierdlem61  47382  fourierdlem92  47413  fourierdlem107  47428  fouriersw  47446  etransclem24  47473  etransclem35  47484  hoidmvlelem2  47811  hspmbllem1  47841  sharhght  48080  deccarry  48586  flmrecm1  48618  nn0mnd  49481  altgsumbcALT  49670  itcovalpclem1  49987  eenglngeehlnmlem2  50056  line2y  50072  itschlc0xyqsol1  50083  itschlc0xyqsol  50084  2itscp  50098  veronesev1lem  51253  veronesev2lem  51254  veronesev3lem  51255  veronesev4lem  51256  veronesev5lem  51257  veronesev6lem  51258