Theorem peano2cn 11430

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   + caddc 11155

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

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

This theorem is referenced by:  nnsscn  12268  xp1d2m1eqxm1d2  12517  zeo  12701  zeo2  12702  zesq  14261  facndiv  14323  faclbnd  14325  faclbnd6  14334  iseralt  15717  bcxmas  15867  trireciplem  15894  fallfacfwd  16068  bpolydiflem  16086  fsumcube  16092  odd2np1  16374  srgbinomlem3  20245  srgbinomlem4  20246  pcoass  25070  dvfsumabs  26077  ply1divex  26190  qaa  26379  aaliou3lem2  26399  abssinper  26577  advlogexp  26711  atantayl2  26995  basellem3  27140  basellem8  27145  lgseisenlem1  27433  lgsquadlem1  27438  pntrsumo1  27623  crctcshwlkn0lem6  29844  clwlkclwwlklem3  30029  fwddifnp1  36146  ltflcei  37594  itg2addnclem3  37659  pell14qrgapw  42863  binomcxplemrat  44345  sumnnodd  45585  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  dirkertrigeq  46056  fourierswlem  46185  fmtnorec4  47473  lighneallem4b  47533  ackval1  48530  ackval2  48531