Theorem peano2cn 10410

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2145  (class class class)co 6793  ℂcc 10136  1c1 10139   + caddc 10141

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

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

This theorem is referenced by:  xp1d2m1eqxm1d2  11488  nneo  11663  zeo  11665  zeo2  11666  zesq  13194  facndiv  13279  faclbnd  13281  faclbnd6  13290  iseralt  14623  bcxmas  14774  trireciplem  14801  fallfacfwd  14973  bpolydiflem  14991  fsumcube  14997  odd2np1  15273  srgbinomlem3  18750  srgbinomlem4  18751  pcoass  23043  dvfsumabs  24006  ply1divex  24116  qaa  24298  aaliou3lem2  24318  abssinper  24491  advlogexp  24622  atantayl2  24886  basellem3  25030  basellem8  25035  lgseisenlem1  25321  lgsquadlem1  25326  pntrsumo1  25475  crctcshwlkn0lem6  26943  clwlkclwwlklem3  27151  fwddifnp1  32609  ltflcei  33730  itg2addnclem3  33795  pell14qrgapw  37966  binomcxplemrat  39075  sumnnodd  40380  dirkertrigeqlem1  40832  dirkertrigeqlem3  40834  dirkertrigeq  40835  fourierswlem  40964  fmtnorec4  41989  lighneallem4b  42054