Theorem peano2cn 11433

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158

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

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

This theorem is referenced by:  nnsscn  12271  xp1d2m1eqxm1d2  12520  zeo  12704  zeo2  12705  zesq  14265  facndiv  14327  faclbnd  14329  faclbnd6  14338  iseralt  15721  bcxmas  15871  trireciplem  15898  fallfacfwd  16072  bpolydiflem  16090  fsumcube  16096  odd2np1  16378  srgbinomlem3  20225  srgbinomlem4  20226  pcoass  25057  dvfsumabs  26063  ply1divex  26176  qaa  26365  aaliou3lem2  26385  abssinper  26563  advlogexp  26697  atantayl2  26981  basellem3  27126  basellem8  27131  lgseisenlem1  27419  lgsquadlem1  27424  pntrsumo1  27609  crctcshwlkn0lem6  29835  clwlkclwwlklem3  30020  fwddifnp1  36166  ltflcei  37615  itg2addnclem3  37680  pell14qrgapw  42887  binomcxplemrat  44369  sumnnodd  45645  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  dirkertrigeq  46116  fourierswlem  46245  fmtnorec4  47536  lighneallem4b  47596  ackval1  48602  ackval2  48603