Theorem addlid 8429

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 8282	. . 3 |- 0 e. CC
2		addcom 8427	. . 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		addrid 8428	. 2 |- ( A e. CC -> ( A + 0 ) = A )
5	3, 4	eqtr3d 2269	1 |- ( A e. CC -> ( 0 + A ) = A )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   0cc0 8143   + caddc 8146

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-addcom 8243  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  readdcan  8430  addlidi  8433  addlidd  8440  cnegexlem1  8465  cnegexlem2  8466  addcan  8470  negneg  8540  fz0to4untppr  10483  fzo0addel  10558  fzoaddel2  10560  divfl0  10683  modqid  10738  swrdspsleq  11387  swrds1  11388  sumrbdclem  12092  summodclem2a  12096  fisum0diag2  12162  eftlub  12405  gcdid  12711  cncrng  14847  ptolemy  15819