Theorem peano2cn 10413

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 10199	. 2 ⊢ 1 ∈ ℂ
2		addcl 10223	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 671	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2145  (class class class)co 6795  ℂcc 10139  1c1 10142   + caddc 10144

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

This theorem depends on definitions:  df-bi 197  df-an 383

This theorem is referenced by:  xp1d2m1eqxm1d2  11492  nneo  11667  zeo  11669  zeo2  11670  zesq  13193  facndiv  13278  faclbnd  13280  faclbnd6  13289  iseralt  14622  bcxmas  14773  trireciplem  14800  fallfacfwd  14972  bpolydiflem  14990  fsumcube  14996  odd2np1  15272  srgbinomlem3  18749  srgbinomlem4  18750  pcoass  23042  dvfsumabs  24005  ply1divex  24115  qaa  24297  aaliou3lem2  24317  abssinper  24490  advlogexp  24621  atantayl2  24885  basellem3  25029  basellem8  25034  lgseisenlem1  25320  lgsquadlem1  25325  pntrsumo1  25474  crctcshwlkn0lem6  26942  clwlkclwwlklem3  27150  fwddifnp1  32608  ltflcei  33729  itg2addnclem3  33794  pell14qrgapw  37966  binomcxplemrat  39075  sumnnodd  40377  dirkertrigeqlem1  40829  dirkertrigeqlem3  40831  dirkertrigeq  40832  fourierswlem  40961  fmtnorec4  41986  lighneallem4b  42051