Theorem peano2cn 9773

Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 10573. (Contributed by NM, 17-Aug-2005.)

Assertion

Ref	Expression
peano2cn

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 9571	. 2
2		addcl 9595	. 2
3	1, 2	mpan2 671	1

Syntax hints:  ->wi 4  e.wcel 1818  (class class class)co 6296  cc 9511  1c1 9514  caddc 9516

This theorem is referenced by:  nneo  10971  zeo  10973  zeo2  10974  uzindOLD  10982  zesq  12289  facndiv  12366  faclbnd  12368  faclbnd6  12377  iseralt  13507  bcxmas  13647  trireciplem  13673  odd2np1  14046  srgbinomlem3  17193  srgbinomlem4  17194  pcoass  21524  dvfsumabs  22424  ply1divex  22537  qaa  22719  aaliou3lem2  22739  abssinper  22911  advlogexp  23036  atantayl2  23269  basellem3  23356  basellem8  23361  lgseisenlem1  23624  lgsquadlem1  23629  pntrsumo1  23750  clwlkisclwwlklem0  24788  fallfacfwd  29158  bpolydiflem  29816  fsumcube  29822  ltflcei  30043  itg2addnclem3  30068  pell14qrgapw  30812  binomcxplemrat  31255  sumnnodd  31636  dirkertrigeqlem1  31880  dirkertrigeqlem3  31882  dirkertrigeq  31883  fourierswlem  32013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 9571  ax-addcl 9573

This theorem depends on definitions:  df-bi 185  df-an 371