Theorem peano2cn 11352

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11128	. 2 ⊢ 1 ∈ ℂ
2		addcl 11152	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 701	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  1c1 11071   + caddc 11073

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

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

This theorem is referenced by:  nnsscn  12212  xp1d2m1eqxm1d2  12472  zeo  12656  zeo2  12657  zesq  14236  facndiv  14298  faclbnd  14300  faclbnd6  14309  iseralt  15695  bcxmas  15848  trireciplem  15875  fallfacfwd  16049  bpolydiflem  16067  fsumcube  16073  odd2np1  16358  srgbinomlem3  20257  srgbinomlem4  20258  pcoass  25066  dvfsumabs  26065  ply1divex  26177  qaa  26364  aaliou3lem2  26384  abssinper  26563  advlogexp  26697  atantayl2  26980  basellem3  27124  basellem8  27129  lgseisenlem1  27416  lgsquadlem1  27421  pntrsumo1  27606  crctcshwlkn0lem6  29961  clwlkclwwlklem3  30149  fwddifnp1  36479  ltflcei  38071  itg2addnclem3  38136  pell14qrgapw  43417  binomcxplemrat  44890  sumnnodd  46170  dirkertrigeqlem1  46636  dirkertrigeqlem3  46638  dirkertrigeq  46639  fourierswlem  46768  fmtnorec4  48122  lighneallem4b  48182  ackval1  49267  ackval2  49268