Theorem peano2cn 11392

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

Assertion

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

Proof of Theorem peano2cn

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7416  ℂcc 11108  1c1 11111   + caddc 11113

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

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

This theorem is used by:  nnsscn  12248  xp1d2m1eqxm1d2  12508  zeo  12692  zeo2  12693  zesq  14273  facndiv  14335  faclbnd  14337  faclbnd6  14346  iseralt  15747  bcxmas  15900  trireciplem  15927  fallfacfwd  16100  bpolydiflem  16118  fsumcube  16124  odd2np1  16409  srgbinomlem3  20320  srgbinomlem4  20321  pcoass  25198  dvfsumabs  26197  ply1divex  26309  qaa  26499  aaliou3lem2  26521  abssinper  26701  advlogexp  26835  atantayl2  27118  basellem3  27262  basellem8  27267  lgseisenlem1  27554  lgsquadlem1  27559  pntrsumo1  27744  crctcshwlkn0lem6  30179  clwlkclwwlklem3  30367  fwddifnp1  36669  ltflcei  38291  itg2addnclem3  38356  pell14qrgapw  43635  binomcxplemrat  45092  sumnnodd  46378  dirkertrigeqlem1  46844  dirkertrigeqlem3  46846  dirkertrigeq  46847  fourierswlem  46976  fmtnorec4  48333  lighneallem4b  48393  ackval1  49493  ackval2  49494