Theorem addlid 8099

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 7952	. . 3 |- 0 e. CC
2		addcom 8097	. . 3 |- ( ( A e. CC /\ 0 e. CC ) -> ( A + 0 ) = ( 0 + A ) )
3	1, 2	mpan2 425	. 2 |- ( A e. CC -> ( A + 0 ) = ( 0 + A ) )
4		addid1 8098	. 2 |- ( A e. CC -> ( A + 0 ) = A )
5	3, 4	eqtr3d 2212	1 |- ( A e. CC -> ( 0 + A ) = A )

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5878   CCcc 7812   0cc0 7814   + caddc 7817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7907  ax-icn 7909  ax-addcl 7910  ax-mulcl 7912  ax-addcom 7914  ax-i2m1 7919  ax-0id 7922

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  readdcan  8100  addid2i  8103  addid2d  8110  cnegexlem1  8135  cnegexlem2  8136  addcan  8140  negneg  8210  fz0to4untppr  10127  fzoaddel2  10196  divfl0  10299  modqid  10352  sumrbdclem  11388  summodclem2a  11392  fisum0diag2  11458  eftlub  11701  gcdid  11990  cncrng  13603  ptolemy  14385