Theorem peano2cn 10814

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 10597	. 2 ⊢ 1 ∈ ℂ
2		addcl 10621	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 689	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537  1c1 10540   + caddc 10542

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  nnsscn  11645  xp1d2m1eqxm1d2  11894  nneo  12069  zeo  12071  zeo2  12072  zesq  13590  facndiv  13651  faclbnd  13653  faclbnd6  13662  iseralt  15043  bcxmas  15192  trireciplem  15219  fallfacfwd  15392  bpolydiflem  15410  fsumcube  15416  odd2np1  15692  srgbinomlem3  19294  srgbinomlem4  19295  pcoass  23630  dvfsumabs  24622  ply1divex  24732  qaa  24914  aaliou3lem2  24934  abssinper  25108  advlogexp  25240  atantayl2  25518  basellem3  25662  basellem8  25667  lgseisenlem1  25953  lgsquadlem1  25958  pntrsumo1  26143  crctcshwlkn0lem6  27595  clwlkclwwlklem3  27781  fwddifnp1  33628  ltflcei  34882  itg2addnclem3  34947  pell14qrgapw  39480  binomcxplemrat  40689  sumnnodd  41918  dirkertrigeqlem1  42390  dirkertrigeqlem3  42392  dirkertrigeq  42393  fourierswlem  42522  fmtnorec4  43718  lighneallem4b  43781