Theorem peano2cn 11509

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

Assertion

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

Proof of Theorem peano2cn

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   + caddc 11230

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

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

This theorem is used by:  nnsscn  12367  xp1d2m1eqxm1d2  12627  zeo  12812  zeo2  12813  zesq  14397  facndiv  14459  faclbnd  14461  faclbnd6  14470  iseralt  15881  bcxmas  16033  trireciplem  16060  fallfacfwd  16231  bpolydiflem  16249  fsumcube  16255  odd2np1  16540  srgbinomlem3  20484  srgbinomlem4  20485  pcoass  25375  dvfsumabs  26373  ply1divex  26485  qaa  26677  aaliou3lem2  26700  abssinper  26879  advlogexp  27013  atantayl2  27296  basellem3  27440  basellem8  27445  lgseisenlem1  27732  lgsquadlem1  27737  pntrsumo1  27922  crctcshwlkn0lem6  30434  clwlkclwwlklem3  30622  fwddifnp1  37108  ltflcei  38723  itg2addnclem3  38783  pell14qrgapw  44076  binomcxplemrat  45526  sumnnodd  46847  dirkertrigeqlem1  47313  dirkertrigeqlem3  47315  dirkertrigeq  47316  fourierswlem  47445  fmtnorec4  48839  lighneallem4b  48899  ackval1  49998  ackval2  49999