Theorem peano2cn 10659

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 10441	. 2 ⊢ 1 ∈ ℂ
2		addcl 10465	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 687	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2081  (class class class)co 7016  ℂcc 10381  1c1 10384   + caddc 10386

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

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

This theorem is referenced by:  nnsscn  11491  xp1d2m1eqxm1d2  11739  nneo  11915  zeo  11917  zeo2  11918  zesq  13437  facndiv  13498  faclbnd  13500  faclbnd6  13509  iseralt  14875  bcxmas  15023  trireciplem  15050  fallfacfwd  15223  bpolydiflem  15241  fsumcube  15247  odd2np1  15523  srgbinomlem3  18982  srgbinomlem4  18983  pcoass  23311  dvfsumabs  24303  ply1divex  24413  qaa  24595  aaliou3lem2  24615  abssinper  24789  advlogexp  24919  atantayl2  25197  basellem3  25342  basellem8  25347  lgseisenlem1  25633  lgsquadlem1  25638  pntrsumo1  25823  crctcshwlkn0lem6  27280  clwlkclwwlklem3  27466  fwddifnp1  33235  ltflcei  34411  itg2addnclem3  34476  pell14qrgapw  38958  binomcxplemrat  40220  sumnnodd  41453  dirkertrigeqlem1  41925  dirkertrigeqlem3  41927  dirkertrigeq  41928  fourierswlem  42057  fmtnorec4  43193  lighneallem4b  43256