Theorem peano2cn 11388

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11170	. 2 ⊢ 1 ∈ ℂ
2		addcl 11194	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 689	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7411  ℂcc 11110  1c1 11113   + caddc 11115

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

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

This theorem is referenced by:  nnsscn  12219  xp1d2m1eqxm1d2  12468  zeo  12650  zeo2  12651  zesq  14191  facndiv  14250  faclbnd  14252  faclbnd6  14261  iseralt  15633  bcxmas  15783  trireciplem  15810  fallfacfwd  15982  bpolydiflem  16000  fsumcube  16006  odd2np1  16286  srgbinomlem3  20053  srgbinomlem4  20054  pcoass  24547  dvfsumabs  25547  ply1divex  25661  qaa  25843  aaliou3lem2  25863  abssinper  26037  advlogexp  26170  atantayl2  26450  basellem3  26594  basellem8  26599  lgseisenlem1  26885  lgsquadlem1  26890  pntrsumo1  27075  crctcshwlkn0lem6  29107  clwlkclwwlklem3  29292  fwddifnp1  35206  ltflcei  36562  itg2addnclem3  36627  pell14qrgapw  41696  binomcxplemrat  43191  sumnnodd  44425  dirkertrigeqlem1  44893  dirkertrigeqlem3  44895  dirkertrigeq  44896  fourierswlem  45025  fmtnorec4  46296  lighneallem4b  46356  ackval1  47445  ackval2  47446