Theorem peano2cn 11004

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

Assertion

Ref	Expression
peano2cn	⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 10787	. 2 ⊢ 1 ∈ ℂ
2		addcl 10811	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 691	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2110  (class class class)co 7213  ℂcc 10727  1c1 10730   + caddc 10732

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  nnsscn  11835  xp1d2m1eqxm1d2  12084  nneo  12261  zeo  12263  zeo2  12264  zesq  13793  facndiv  13854  faclbnd  13856  faclbnd6  13865  iseralt  15248  bcxmas  15399  trireciplem  15426  fallfacfwd  15598  bpolydiflem  15616  fsumcube  15622  odd2np1  15902  srgbinomlem3  19557  srgbinomlem4  19558  pcoass  23921  dvfsumabs  24920  ply1divex  25034  qaa  25216  aaliou3lem2  25236  abssinper  25410  advlogexp  25543  atantayl2  25821  basellem3  25965  basellem8  25970  lgseisenlem1  26256  lgsquadlem1  26261  pntrsumo1  26446  crctcshwlkn0lem6  27899  clwlkclwwlklem3  28084  fwddifnp1  34204  ltflcei  35502  itg2addnclem3  35567  pell14qrgapw  40401  binomcxplemrat  41641  sumnnodd  42846  dirkertrigeqlem1  43314  dirkertrigeqlem3  43316  dirkertrigeq  43317  fourierswlem  43446  fmtnorec4  44674  lighneallem4b  44734  ackval1  45700  ackval2  45701