Theorem peano2cn 11410

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

Assertion

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

Proof of Theorem peano2cn

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  1c1 11129   + caddc 11131

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

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

This theorem is used by:  nnsscn  12266  xp1d2m1eqxm1d2  12526  zeo  12711  zeo2  12712  zesq  14294  facndiv  14356  faclbnd  14358  faclbnd6  14367  iseralt  15776  bcxmas  15928  trireciplem  15955  fallfacfwd  16128  bpolydiflem  16146  fsumcube  16152  odd2np1  16437  srgbinomlem3  20373  srgbinomlem4  20374  pcoass  25258  dvfsumabs  26257  ply1divex  26369  qaa  26563  aaliou3lem2  26586  abssinper  26766  advlogexp  26900  atantayl2  27183  basellem3  27327  basellem8  27332  lgseisenlem1  27619  lgsquadlem1  27624  pntrsumo1  27809  crctcshwlkn0lem6  30291  clwlkclwwlklem3  30479  fwddifnp1  36753  ltflcei  38370  itg2addnclem3  38430  pell14qrgapw  43725  binomcxplemrat  45182  sumnnodd  46468  dirkertrigeqlem1  46934  dirkertrigeqlem3  46936  dirkertrigeq  46937  fourierswlem  47066  fmtnorec4  48460  lighneallem4b  48520  ackval1  49619  ackval2  49620