Theorem peano2cn 11485

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11261	. 2 ⊢ 1 ∈ ℂ
2		addcl 11285	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 704	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  1c1 11204   + caddc 11206

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 11261  ax-addcl 11263

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  nnsscn  12343  xp1d2m1eqxm1d2  12603  zeo  12788  zeo2  12789  zesq  14373  facndiv  14435  faclbnd  14437  faclbnd6  14446  iseralt  15857  bcxmas  16009  trireciplem  16036  fallfacfwd  16207  bpolydiflem  16225  fsumcube  16231  odd2np1  16516  srgbinomlem3  20459  srgbinomlem4  20460  pcoass  25350  dvfsumabs  26348  ply1divex  26460  qaa  26652  aaliou3lem2  26675  abssinper  26854  advlogexp  26988  atantayl2  27271  basellem3  27415  basellem8  27420  lgseisenlem1  27707  lgsquadlem1  27712  pntrsumo1  27897  crctcshwlkn0lem6  30409  clwlkclwwlklem3  30597  fwddifnp1  37022  ltflcei  38624  itg2addnclem3  38684  pell14qrgapw  43976  binomcxplemrat  45427  sumnnodd  46735  dirkertrigeqlem1  47201  dirkertrigeqlem3  47203  dirkertrigeq  47204  fourierswlem  47333  fmtnorec4  48727  lighneallem4b  48787  ackval1  49886  ackval2  49887