ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addid2 GIF version

Theorem addid2 7865
Description: 0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
addid2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2
StepHypRef Expression
1 0cn 7722 . . 3 0 ∈ ℂ
2 addcom 7863 . . 3 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴))
31, 2mpan2 419 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴))
4 addid1 7864 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
53, 4eqtr3d 2150 1 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wcel 1463  (class class class)co 5740  cc 7582  0cc0 7584   + caddc 7587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-1cn 7677  ax-icn 7679  ax-addcl 7680  ax-mulcl 7682  ax-addcom 7684  ax-i2m1 7689  ax-0id 7692
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  readdcan  7866  addid2i  7869  addid2d  7876  cnegexlem1  7901  cnegexlem2  7902  addcan  7906  negneg  7976  fzoaddel2  9921  divfl0  10020  modqid  10073  sumrbdclem  11096  summodclem2a  11101  fisum0diag2  11167  eftlub  11306  gcdid  11581
  Copyright terms: Public domain W3C validator