Theorem peano2cn 11130

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 10913	. 2 ⊢ 1 ∈ ℂ
2		addcl 10937	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 687	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853  1c1 10856   + caddc 10858

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

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  nnsscn  11961  xp1d2m1eqxm1d2  12210  nneo  12387  zeo  12389  zeo2  12390  zesq  13922  facndiv  13983  faclbnd  13985  faclbnd6  13994  iseralt  15377  bcxmas  15528  trireciplem  15555  fallfacfwd  15727  bpolydiflem  15745  fsumcube  15751  odd2np1  16031  srgbinomlem3  19759  srgbinomlem4  19760  pcoass  24168  dvfsumabs  25168  ply1divex  25282  qaa  25464  aaliou3lem2  25484  abssinper  25658  advlogexp  25791  atantayl2  26069  basellem3  26213  basellem8  26218  lgseisenlem1  26504  lgsquadlem1  26509  pntrsumo1  26694  crctcshwlkn0lem6  28159  clwlkclwwlklem3  28344  fwddifnp1  34446  ltflcei  35744  itg2addnclem3  35809  pell14qrgapw  40678  binomcxplemrat  41921  sumnnodd  43125  dirkertrigeqlem1  43593  dirkertrigeqlem3  43595  dirkertrigeq  43596  fourierswlem  43725  fmtnorec4  44953  lighneallem4b  45013  ackval1  45979  ackval2  45980