Theorem peano2cn 11309

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11087	. 2 ⊢ 1 ∈ ℂ
2		addcl 11111	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 692	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  1c1 11030   + caddc 11032

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

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

This theorem is referenced by:  nnsscn  12170  xp1d2m1eqxm1d2  12422  zeo  12606  zeo2  12607  zesq  14179  facndiv  14241  faclbnd  14243  faclbnd6  14252  iseralt  15638  bcxmas  15791  trireciplem  15818  fallfacfwd  15992  bpolydiflem  16010  fsumcube  16016  odd2np1  16301  srgbinomlem3  20200  srgbinomlem4  20201  pcoass  25001  dvfsumabs  26000  ply1divex  26112  qaa  26300  aaliou3lem2  26320  abssinper  26498  advlogexp  26632  atantayl2  26915  basellem3  27060  basellem8  27065  lgseisenlem1  27352  lgsquadlem1  27357  pntrsumo1  27542  crctcshwlkn0lem6  29898  clwlkclwwlklem3  30086  fwddifnp1  36363  ltflcei  37943  itg2addnclem3  38008  pell14qrgapw  43322  binomcxplemrat  44795  sumnnodd  46078  dirkertrigeqlem1  46544  dirkertrigeqlem3  46546  dirkertrigeq  46547  fourierswlem  46676  fmtnorec4  48024  lighneallem4b  48084  ackval1  49169  ackval2  49170