Theorem peano2cn 11346

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071

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

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

This theorem is referenced by:  nnsscn  12191  xp1d2m1eqxm1d2  12436  zeo  12620  zeo2  12621  zesq  14191  facndiv  14253  faclbnd  14255  faclbnd6  14264  iseralt  15651  bcxmas  15801  trireciplem  15828  fallfacfwd  16002  bpolydiflem  16020  fsumcube  16026  odd2np1  16311  srgbinomlem3  20137  srgbinomlem4  20138  pcoass  24924  dvfsumabs  25929  ply1divex  26042  qaa  26231  aaliou3lem2  26251  abssinper  26430  advlogexp  26564  atantayl2  26848  basellem3  26993  basellem8  26998  lgseisenlem1  27286  lgsquadlem1  27291  pntrsumo1  27476  crctcshwlkn0lem6  29745  clwlkclwwlklem3  29930  fwddifnp1  36153  ltflcei  37602  itg2addnclem3  37667  pell14qrgapw  42864  binomcxplemrat  44339  sumnnodd  45628  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  dirkertrigeq  46099  fourierswlem  46228  fmtnorec4  47550  lighneallem4b  47610  ackval1  48670  ackval2  48671