Theorem peano2cn 11285

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11064	. 2 ⊢ 1 ∈ ℂ
2		addcl 11088	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 691	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  1c1 11007   + caddc 11009

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  nnsscn  12130  xp1d2m1eqxm1d2  12375  zeo  12559  zeo2  12560  zesq  14133  facndiv  14195  faclbnd  14197  faclbnd6  14206  iseralt  15592  bcxmas  15742  trireciplem  15769  fallfacfwd  15943  bpolydiflem  15961  fsumcube  15967  odd2np1  16252  srgbinomlem3  20146  srgbinomlem4  20147  pcoass  24951  dvfsumabs  25956  ply1divex  26069  qaa  26258  aaliou3lem2  26278  abssinper  26457  advlogexp  26591  atantayl2  26875  basellem3  27020  basellem8  27025  lgseisenlem1  27313  lgsquadlem1  27318  pntrsumo1  27503  crctcshwlkn0lem6  29793  clwlkclwwlklem3  29981  fwddifnp1  36209  ltflcei  37647  itg2addnclem3  37712  pell14qrgapw  42968  binomcxplemrat  44442  sumnnodd  45729  dirkertrigeqlem1  46195  dirkertrigeqlem3  46197  dirkertrigeq  46198  fourierswlem  46327  fmtnorec4  47648  lighneallem4b  47708  ackval1  48781  ackval2  48782