Theorem peano2cn 10208

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

Assertion

Ref	Expression
peano2cn	|- ( A e. CC -> ( A + 1 ) e. CC )

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 9994	. 2 |- 1 e. CC
2		addcl 10018	. 2 |- ( ( A e. CC /\ 1 e. CC ) -> ( A + 1 ) e. CC )
3	1, 2	mpan2 707	1 |- ( A e. CC -> ( A + 1 ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1990  (class class class)co 6650   CCcc 9934   1c1 9937   + caddc 9939

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  xp1d2m1eqxm1d2  11286  nneo  11461  zeo  11463  zeo2  11464  zesq  12987  facndiv  13075  faclbnd  13077  faclbnd6  13086  iseralt  14415  bcxmas  14567  trireciplem  14594  fallfacfwd  14767  bpolydiflem  14785  fsumcube  14791  odd2np1  15065  srgbinomlem3  18542  srgbinomlem4  18543  pcoass  22824  dvfsumabs  23786  ply1divex  23896  qaa  24078  aaliou3lem2  24098  abssinper  24270  advlogexp  24401  atantayl2  24665  basellem3  24809  basellem8  24814  lgseisenlem1  25100  lgsquadlem1  25105  pntrsumo1  25254  crctcshwlkn0lem6  26707  clwlkclwwlklem3  26902  fwddifnp1  32272  ltflcei  33397  itg2addnclem3  33463  pell14qrgapw  37440  binomcxplemrat  38549  sumnnodd  39862  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  dirkertrigeq  40318  fourierswlem  40447  fmtnorec4  41461  lighneallem4b  41526