Theorem peano2cn 11317

Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 12169. (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 7368  ℂ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  12162  xp1d2m1eqxm1d2  12407  zeo  12590  zeo2  12591  zesq  14161  facndiv  14223  faclbnd  14225  faclbnd6  14234  iseralt  15620  bcxmas  15770  trireciplem  15797  fallfacfwd  15971  bpolydiflem  15989  fsumcube  15995  odd2np1  16280  srgbinomlem3  20175  srgbinomlem4  20176  pcoass  24992  dvfsumabs  25997  ply1divex  26110  qaa  26299  aaliou3lem2  26319  abssinper  26498  advlogexp  26632  atantayl2  26916  basellem3  27061  basellem8  27066  lgseisenlem1  27354  lgsquadlem1  27359  pntrsumo1  27544  crctcshwlkn0lem6  29900  clwlkclwwlklem3  30088  fwddifnp1  36378  ltflcei  37853  itg2addnclem3  37918  pell14qrgapw  43227  binomcxplemrat  44700  sumnnodd  45984  dirkertrigeqlem1  46450  dirkertrigeqlem3  46452  dirkertrigeq  46453  fourierswlem  46582  fmtnorec4  47903  lighneallem4b  47963  ackval1  49035  ackval2  49036