Theorem peano2cn 11463

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11239	. 2 ⊢ 1 ∈ ℂ
2		addcl 11263	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 704	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179  1c1 11182   + caddc 11184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 11239  ax-addcl 11241

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  nnsscn  12321  xp1d2m1eqxm1d2  12581  zeo  12766  zeo2  12767  zesq  14350  facndiv  14412  faclbnd  14414  faclbnd6  14423  iseralt  15832  bcxmas  15984  trireciplem  16011  fallfacfwd  16182  bpolydiflem  16200  fsumcube  16206  odd2np1  16491  srgbinomlem3  20434  srgbinomlem4  20435  pcoass  25325  dvfsumabs  26323  ply1divex  26435  qaa  26629  aaliou3lem2  26652  abssinper  26831  advlogexp  26965  atantayl2  27248  basellem3  27392  basellem8  27397  lgseisenlem1  27684  lgsquadlem1  27689  pntrsumo1  27874  crctcshwlkn0lem6  30386  clwlkclwwlklem3  30574  fwddifnp1  36900  ltflcei  38499  itg2addnclem3  38559  pell14qrgapw  43836  binomcxplemrat  45293  sumnnodd  46586  dirkertrigeqlem1  47052  dirkertrigeqlem3  47054  dirkertrigeq  47055  fourierswlem  47184  fmtnorec4  48578  lighneallem4b  48638  ackval1  49737  ackval2  49738