Theorem addid2i 11068

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

Hypothesis

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
addid2i	⊢ (0 + 𝐴) = 𝐴

Proof of Theorem addid2i

Step	Hyp	Ref	Expression
1		mul.1	. 2 ⊢ 𝐴 ∈ ℂ
2		addid2 11063	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (0 + 𝐴) = 𝐴

Syntax hints:   = wceq 1543   ∈ wcel 2112  (class class class)co 7252  ℂcc 10775  0cc0 10777   + caddc 10780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563  ax-resscn 10834  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-addrcl 10838  ax-mulcl 10839  ax-mulrcl 10840  ax-mulcom 10841  ax-addass 10842  ax-mulass 10843  ax-distr 10844  ax-i2m1 10845  ax-1ne0 10846  ax-1rid 10847  ax-rnegex 10848  ax-rrecex 10849  ax-cnre 10850  ax-pre-lttri 10851  ax-pre-lttrn 10852  ax-pre-ltadd 10853

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5153  df-id 5479  df-po 5493  df-so 5494  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-ov 7255  df-er 8433  df-en 8669  df-dom 8670  df-sdom 8671  df-pnf 10917  df-mnf 10918  df-ltxr 10920

This theorem is referenced by:  ine0  11315  muleqadd  11524  inelr  11868  nnne0  11912  0p1e1  12000  num0h  12353  nummul1c  12390  decrmac  12399  fz0tp  13261  fz0to4untppr  13263  fzo0to3tp  13376  cats1fvn  14474  rei  14770  imi  14771  ef01bndlem  15796  gcdaddmlem  16134  dec5dvds2  16669  2exp11  16694  2exp16  16695  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001prm  16749  frgpnabllem1  19364  pcoass  24068  dvradcnv  25460  efhalfpi  25508  sinq34lt0t  25546  efifo  25583  logm1  25624  argimgt0  25647  ang180lem4  25842  1cubr  25872  asin1  25924  atanlogsublem  25945  dvatan  25965  log2ublem3  25978  log2ub  25979  basellem9  26118  cht2  26201  log2sumbnd  26572  ax5seglem7  27181  ex-fac  28691  dp20h  31030  dpmul4  31065  hgt750lem2  32507  12gcd5e1  39918  3exp7  39968  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1  39990  sqn5i  40206  decpmul  40209  sqdeccom12  40210  sq3deccom12  40211  ex-decpmul  40213  fltnltalem  40387  dirkertrigeqlem1  43502  dirkertrigeqlem3  43504  fourierdlem103  43613  sqwvfoura  43632  sqwvfourb  43633  fouriersw  43635  fmtno5lem1  44866  fmtno5lem2  44867  fmtno5lem4  44869  fmtno4prmfac  44885  fmtno5faclem2  44893  fmtno5faclem3  44894  fmtno5fac  44895  139prmALT  44909  127prm  44912  2exp340mod341  45046  nfermltl8rev  45055  ackval1012  45897  ackval2012  45898  ackval3012  45899