Theorem peano2cn 11316

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11094	. 2 ⊢ 1 ∈ ℂ
2		addcl 11118	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 697	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  1c1 11037   + caddc 11039

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  nnsscn  12177  xp1d2m1eqxm1d2  12429  zeo  12613  zeo2  12614  zesq  14186  facndiv  14248  faclbnd  14250  faclbnd6  14259  iseralt  15645  bcxmas  15798  trireciplem  15825  fallfacfwd  15999  bpolydiflem  16017  fsumcube  16023  odd2np1  16308  srgbinomlem3  20207  srgbinomlem4  20208  pcoass  25016  dvfsumabs  26015  ply1divex  26127  qaa  26314  aaliou3lem2  26334  abssinper  26510  advlogexp  26644  atantayl2  26927  basellem3  27071  basellem8  27076  lgseisenlem1  27363  lgsquadlem1  27368  pntrsumo1  27553  crctcshwlkn0lem6  29908  clwlkclwwlklem3  30096  fwddifnp1  36400  ltflcei  37982  itg2addnclem3  38047  pell14qrgapw  43328  binomcxplemrat  44801  sumnnodd  46082  dirkertrigeqlem1  46548  dirkertrigeqlem3  46550  dirkertrigeq  46551  fourierswlem  46680  fmtnorec4  48034  lighneallem4b  48094  ackval1  49179  ackval2  49180