Theorem peano2cn 11306

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   + caddc 11031

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

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

This theorem is referenced by:  nnsscn  12151  xp1d2m1eqxm1d2  12396  zeo  12580  zeo2  12581  zesq  14151  facndiv  14213  faclbnd  14215  faclbnd6  14224  iseralt  15610  bcxmas  15760  trireciplem  15787  fallfacfwd  15961  bpolydiflem  15979  fsumcube  15985  odd2np1  16270  srgbinomlem3  20131  srgbinomlem4  20132  pcoass  24940  dvfsumabs  25945  ply1divex  26058  qaa  26247  aaliou3lem2  26267  abssinper  26446  advlogexp  26580  atantayl2  26864  basellem3  27009  basellem8  27014  lgseisenlem1  27302  lgsquadlem1  27307  pntrsumo1  27492  crctcshwlkn0lem6  29778  clwlkclwwlklem3  29963  fwddifnp1  36138  ltflcei  37587  itg2addnclem3  37652  pell14qrgapw  42849  binomcxplemrat  44323  sumnnodd  45612  dirkertrigeqlem1  46080  dirkertrigeqlem3  46082  dirkertrigeq  46083  fourierswlem  46212  fmtnorec4  47534  lighneallem4b  47594  ackval1  48667  ackval2  48668