Theorem peano2cn 11370

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  1c1 11089   + caddc 11091

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  nnsscn  12229  xp1d2m1eqxm1d2  12489  zeo  12673  zeo2  12674  zesq  14253  facndiv  14315  faclbnd  14317  faclbnd6  14326  iseralt  15726  bcxmas  15879  trireciplem  15906  fallfacfwd  16080  bpolydiflem  16098  fsumcube  16104  odd2np1  16389  srgbinomlem3  20301  srgbinomlem4  20302  pcoass  25144  dvfsumabs  26143  ply1divex  26255  qaa  26445  aaliou3lem2  26465  abssinper  26644  advlogexp  26778  atantayl2  27061  basellem3  27205  basellem8  27210  lgseisenlem1  27497  lgsquadlem1  27502  pntrsumo1  27687  crctcshwlkn0lem6  30073  clwlkclwwlklem3  30261  fwddifnp1  36528  ltflcei  38119  itg2addnclem3  38184  pell14qrgapw  43465  binomcxplemrat  44924  sumnnodd  46204  dirkertrigeqlem1  46670  dirkertrigeqlem3  46672  dirkertrigeq  46673  fourierswlem  46802  fmtnorec4  48156  lighneallem4b  48216  ackval1  49312  ackval2  49313