Theorem peano2cn 11318

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11096	. 2 ⊢ 1 ∈ ℂ
2		addcl 11120	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 692	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041

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

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

This theorem is referenced by:  nnsscn  12179  xp1d2m1eqxm1d2  12431  zeo  12615  zeo2  12616  zesq  14188  facndiv  14250  faclbnd  14252  faclbnd6  14261  iseralt  15647  bcxmas  15800  trireciplem  15827  fallfacfwd  16001  bpolydiflem  16019  fsumcube  16025  odd2np1  16310  srgbinomlem3  20209  srgbinomlem4  20210  pcoass  24991  dvfsumabs  25990  ply1divex  26102  qaa  26289  aaliou3lem2  26309  abssinper  26485  advlogexp  26619  atantayl2  26902  basellem3  27046  basellem8  27051  lgseisenlem1  27338  lgsquadlem1  27343  pntrsumo1  27528  crctcshwlkn0lem6  29883  clwlkclwwlklem3  30071  fwddifnp1  36347  ltflcei  37929  itg2addnclem3  37994  pell14qrgapw  43304  binomcxplemrat  44777  sumnnodd  46060  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  dirkertrigeq  46529  fourierswlem  46658  fmtnorec4  48012  lighneallem4b  48072  ackval1  49157  ackval2  49158