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

Theorem peano2cn 9000
Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 9774. (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 8811 . 2  |-  1  e.  CC
2 addcl 8835 . 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 1696  (class class class)co 5874   CCcc 8751   1c1 8754    + caddc 8756
This theorem is referenced by:  nneo  10111  zeo  10113  zeo2  10114  uzindOLD  10122  zesq  11240  facndiv  11317  faclbnd  11319  faclbnd6  11328  iseralt  12173  bcxmas  12310  trireciplem  12336  odd2np1  12603  pcoass  18538  dvfsumabs  19386  ply1divex  19538  qaa  19719  aaliou3lem2  19739  abssinper  19902  advlogexp  20018  atantayl2  20250  basellem3  20336  basellem8  20341  lgseisenlem1  20604  lgsquadlem1  20609  pntrsumo1  20730  bpolydiflem  24861  fsumcube  24867  ltflcei  24998  itg2addnc  25005  pell14qrgapw  27064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-1cn 8811  ax-addcl 8813
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator