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

Theorem peano2cn 8984
Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 9758. (Contributed by NM, 17-Aug-2005.)
Assertion
Ref Expression
peano2cn  |-  ( A  e.  CC  ->  ( A  +  1 )  e.  CC )

Proof of Theorem peano2cn
StepHypRef Expression
1 ax-1cn 8795 . 2  |-  1  e.  CC
2 addcl 8819 . 2  |-  ( ( A  e.  CC  /\  1  e.  CC )  ->  ( A  +  1 )  e.  CC )
31, 2mpan2 652 1  |-  ( A  e.  CC  ->  ( A  +  1 )  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684  (class class class)co 5858   CCcc 8735   1c1 8738    + caddc 8740
This theorem is referenced by:  nneo  10095  zeo  10097  zeo2  10098  uzindOLD  10106  zesq  11224  facndiv  11301  faclbnd  11303  faclbnd6  11312  iseralt  12157  bcxmas  12294  trireciplem  12320  odd2np1  12587  pcoass  18522  dvfsumabs  19370  ply1divex  19522  qaa  19703  aaliou3lem2  19723  abssinper  19886  advlogexp  20002  atantayl2  20234  basellem3  20320  basellem8  20325  lgseisenlem1  20588  lgsquadlem1  20593  pntrsumo1  20714  bpolydiflem  24789  fsumcube  24795  pell14qrgapw  26961
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-1cn 8795  ax-addcl 8797
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator