Theorem peano2cn 11462

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11242	. 2 ⊢ 1 ∈ ℂ
2		addcl 11266	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 690	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187

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

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

This theorem is referenced by:  nnsscn  12298  xp1d2m1eqxm1d2  12547  zeo  12729  zeo2  12730  zesq  14275  facndiv  14337  faclbnd  14339  faclbnd6  14348  iseralt  15733  bcxmas  15883  trireciplem  15910  fallfacfwd  16084  bpolydiflem  16102  fsumcube  16108  odd2np1  16389  srgbinomlem3  20255  srgbinomlem4  20256  pcoass  25076  dvfsumabs  26083  ply1divex  26196  qaa  26383  aaliou3lem2  26403  abssinper  26581  advlogexp  26715  atantayl2  26999  basellem3  27144  basellem8  27149  lgseisenlem1  27437  lgsquadlem1  27442  pntrsumo1  27627  crctcshwlkn0lem6  29848  clwlkclwwlklem3  30033  fwddifnp1  36129  ltflcei  37568  itg2addnclem3  37633  pell14qrgapw  42832  binomcxplemrat  44319  sumnnodd  45551  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  dirkertrigeq  46022  fourierswlem  46151  fmtnorec4  47423  lighneallem4b  47483  ackval1  48415  ackval2  48416