Theorem peano2cn 11386

Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 12224. (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 690	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113

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

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  nnsscn  12217  xp1d2m1eqxm1d2  12466  zeo  12648  zeo2  12649  zesq  14189  facndiv  14248  faclbnd  14250  faclbnd6  14259  iseralt  15631  bcxmas  15781  trireciplem  15808  fallfacfwd  15980  bpolydiflem  15998  fsumcube  16004  odd2np1  16284  srgbinomlem3  20051  srgbinomlem4  20052  pcoass  24540  dvfsumabs  25540  ply1divex  25654  qaa  25836  aaliou3lem2  25856  abssinper  26030  advlogexp  26163  atantayl2  26443  basellem3  26587  basellem8  26592  lgseisenlem1  26878  lgsquadlem1  26883  pntrsumo1  27068  crctcshwlkn0lem6  29069  clwlkclwwlklem3  29254  fwddifnp1  35137  ltflcei  36476  itg2addnclem3  36541  pell14qrgapw  41614  binomcxplemrat  43109  sumnnodd  44346  dirkertrigeqlem1  44814  dirkertrigeqlem3  44816  dirkertrigeq  44817  fourierswlem  44946  fmtnorec4  46217  lighneallem4b  46277  ackval1  47367  ackval2  47368