Theorem peano2cn 11282

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

Assertion

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

Proof of Theorem peano2cn

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

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

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

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

This theorem is referenced by:  nnsscn  12127  xp1d2m1eqxm1d2  12372  zeo  12556  zeo2  12557  zesq  14130  facndiv  14192  faclbnd  14194  faclbnd6  14203  iseralt  15589  bcxmas  15739  trireciplem  15766  fallfacfwd  15940  bpolydiflem  15958  fsumcube  15964  odd2np1  16249  srgbinomlem3  20144  srgbinomlem4  20145  pcoass  24949  dvfsumabs  25954  ply1divex  26067  qaa  26256  aaliou3lem2  26276  abssinper  26455  advlogexp  26589  atantayl2  26873  basellem3  27018  basellem8  27023  lgseisenlem1  27311  lgsquadlem1  27316  pntrsumo1  27501  crctcshwlkn0lem6  29791  clwlkclwwlklem3  29976  fwddifnp1  36198  ltflcei  37647  itg2addnclem3  37712  pell14qrgapw  42908  binomcxplemrat  44382  sumnnodd  45669  dirkertrigeqlem1  46135  dirkertrigeqlem3  46137  dirkertrigeq  46138  fourierswlem  46267  fmtnorec4  47579  lighneallem4b  47639  ackval1  48712  ackval2  48713