Theorem peano2cn 11383

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11159	. 2 ⊢ 1 ∈ ℂ
2		addcl 11183	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 703	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   + caddc 11104

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

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

This theorem is referenced by:  nnsscn  12239  xp1d2m1eqxm1d2  12499  zeo  12683  zeo2  12684  zesq  14264  facndiv  14326  faclbnd  14328  faclbnd6  14337  iseralt  15738  bcxmas  15891  trireciplem  15918  fallfacfwd  16091  bpolydiflem  16109  fsumcube  16115  odd2np1  16400  srgbinomlem3  20311  srgbinomlem4  20312  pcoass  25164  dvfsumabs  26163  ply1divex  26275  qaa  26465  aaliou3lem2  26485  abssinper  26664  advlogexp  26798  atantayl2  27081  basellem3  27225  basellem8  27230  lgseisenlem1  27517  lgsquadlem1  27522  pntrsumo1  27707  crctcshwlkn0lem6  30142  clwlkclwwlklem3  30330  fwddifnp1  36635  ltflcei  38237  itg2addnclem3  38302  pell14qrgapw  43583  binomcxplemrat  45040  sumnnodd  46326  dirkertrigeqlem1  46792  dirkertrigeqlem3  46794  dirkertrigeq  46795  fourierswlem  46924  fmtnorec4  48278  lighneallem4b  48338  ackval1  49438  ackval2  49439