Theorem peano2cn 11292

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  1c1 11014   + caddc 11016

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

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

This theorem is referenced by:  nnsscn  12137  xp1d2m1eqxm1d2  12382  zeo  12565  zeo2  12566  zesq  14135  facndiv  14197  faclbnd  14199  faclbnd6  14208  iseralt  15594  bcxmas  15744  trireciplem  15771  fallfacfwd  15945  bpolydiflem  15963  fsumcube  15969  odd2np1  16254  srgbinomlem3  20148  srgbinomlem4  20149  pcoass  24952  dvfsumabs  25957  ply1divex  26070  qaa  26259  aaliou3lem2  26279  abssinper  26458  advlogexp  26592  atantayl2  26876  basellem3  27021  basellem8  27026  lgseisenlem1  27314  lgsquadlem1  27319  pntrsumo1  27504  crctcshwlkn0lem6  29795  clwlkclwwlklem3  29983  fwddifnp1  36230  ltflcei  37668  itg2addnclem3  37733  pell14qrgapw  42993  binomcxplemrat  44467  sumnnodd  45754  dirkertrigeqlem1  46220  dirkertrigeqlem3  46222  dirkertrigeq  46223  fourierswlem  46352  fmtnorec4  47673  lighneallem4b  47733  ackval1  48806  ackval2  48807