Theorem addlid 8467

Description: 0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
addlid	|- ( A e. CC -> ( 0 + A ) = A )

Proof of Theorem addlid

Step	Hyp	Ref	Expression
1		0cn 8319	. . 3 |- 0 e. CC
2		addcom 8465	. . 3 |- ( ( A e. CC /\ 0 e. CC ) -> ( A + 0 ) = ( 0 + A ) )
3	1, 2	mpan2 429	. 2 |- ( A e. CC -> ( A + 0 ) = ( 0 + A ) )
4		addrid 8466	. 2 |- ( A e. CC -> ( A + 0 ) = A )
5	3, 4	eqtr3d 2273	1 |- ( A e. CC -> ( 0 + A ) = A )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   0cc0 8180   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-addcom 8280  ax-i2m1 8285  ax-0id 8288

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  readdcan  8468  addlidi  8471  addlidd  8478  cnegexlem1  8503  cnegexlem2  8504  addcan  8508  negneg  8578  fz0to4untppr  10542  fzo0addel  10617  fzoaddel2  10619  divfl0  10745  modqid  10800  swrdspsleq  11454  swrds1  11455  sumrbdclem  12162  summodclem2a  12166  fisum0diag2  12232  eftlub  12475  gcdid  12781  cncrng  14957  ptolemy  15978