Theorem peano2cn 10087

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 9873	. 2 ⊢ 1 ∈ ℂ
2		addcl 9897	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 703	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813  1c1 9816   + caddc 9818

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  xp1d2m1eqxm1d2  11163  nneo  11337  zeo  11339  zeo2  11340  zesq  12849  facndiv  12937  faclbnd  12939  faclbnd6  12948  iseralt  14263  bcxmas  14406  trireciplem  14433  fallfacfwd  14606  bpolydiflem  14624  fsumcube  14630  odd2np1  14903  srgbinomlem3  18365  srgbinomlem4  18366  pcoass  22632  dvfsumabs  23590  ply1divex  23700  qaa  23882  aaliou3lem2  23902  abssinper  24074  advlogexp  24201  atantayl2  24465  basellem3  24609  basellem8  24614  lgseisenlem1  24900  lgsquadlem1  24905  pntrsumo1  25054  clwlkisclwwlklem0  26316  fwddifnp1  31442  ltflcei  32567  itg2addnclem3  32633  pell14qrgapw  36458  binomcxplemrat  37571  sumnnodd  38697  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  dirkertrigeq  38994  fourierswlem  39123  fmtnorec4  39999  lighneallem4b  40064  crctcsh1wlkn0lem6  41018  clwlkclwwlklem3  41210