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

Theorem peano2cn 9238
Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 10012. (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 9048 . 2  |-  1  e.  CC
2 addcl 9072 . 2  |-  ( ( A  e.  CC  /\  1  e.  CC )  ->  ( A  +  1 )  e.  CC )
31, 2mpan2 653 1  |-  ( A  e.  CC  ->  ( A  +  1 )  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725  (class class class)co 6081   CCcc 8988   1c1 8991    + caddc 8993
This theorem is referenced by:  nneo  10353  zeo  10355  zeo2  10356  uzindOLD  10364  zesq  11502  facndiv  11579  faclbnd  11581  faclbnd6  11590  iseralt  12478  bcxmas  12615  trireciplem  12641  odd2np1  12908  pcoass  19049  dvfsumabs  19907  ply1divex  20059  qaa  20240  aaliou3lem2  20260  abssinper  20426  advlogexp  20546  atantayl2  20778  basellem3  20865  basellem8  20870  lgseisenlem1  21133  lgsquadlem1  21138  pntrsumo1  21259  fallfacfwd  25352  bpolydiflem  26100  fsumcube  26106  ltflcei  26239  itg2addnclem3  26258  pell14qrgapw  26939
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-1cn 9048  ax-addcl 9050
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator