MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2cn Unicode version

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
StepHypRef Expression
1 ax-1cn 9571 . 2
2 addcl 9595 . 2
31, 2mpan2 671 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator