Theorem peano2cn 11305

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029

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

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

This theorem is referenced by:  nnsscn  12150  xp1d2m1eqxm1d2  12395  zeo  12578  zeo2  12579  zesq  14149  facndiv  14211  faclbnd  14213  faclbnd6  14222  iseralt  15608  bcxmas  15758  trireciplem  15785  fallfacfwd  15959  bpolydiflem  15977  fsumcube  15983  odd2np1  16268  srgbinomlem3  20163  srgbinomlem4  20164  pcoass  24980  dvfsumabs  25985  ply1divex  26098  qaa  26287  aaliou3lem2  26307  abssinper  26486  advlogexp  26620  atantayl2  26904  basellem3  27049  basellem8  27054  lgseisenlem1  27342  lgsquadlem1  27347  pntrsumo1  27532  crctcshwlkn0lem6  29888  clwlkclwwlklem3  30076  fwddifnp1  36359  ltflcei  37805  itg2addnclem3  37870  pell14qrgapw  43114  binomcxplemrat  44587  sumnnodd  45872  dirkertrigeqlem1  46338  dirkertrigeqlem3  46340  dirkertrigeq  46341  fourierswlem  46470  fmtnorec4  47791  lighneallem4b  47851  ackval1  48923  ackval2  48924