Theorem peano2cn 11400

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

Assertion

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

Proof of Theorem peano2cn

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  1c1 11119   + caddc 11121

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

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

This theorem is used by:  nnsscn  12256  xp1d2m1eqxm1d2  12516  zeo  12700  zeo2  12701  zesq  14282  facndiv  14344  faclbnd  14346  faclbnd6  14355  iseralt  15762  bcxmas  15915  trireciplem  15942  fallfacfwd  16115  bpolydiflem  16133  fsumcube  16139  odd2np1  16424  srgbinomlem3  20341  srgbinomlem4  20342  pcoass  25220  dvfsumabs  26219  ply1divex  26331  qaa  26521  aaliou3lem2  26543  abssinper  26723  advlogexp  26857  atantayl2  27140  basellem3  27284  basellem8  27289  lgseisenlem1  27576  lgsquadlem1  27581  pntrsumo1  27766  crctcshwlkn0lem6  30201  clwlkclwwlklem3  30389  fwddifnp1  36678  ltflcei  38300  itg2addnclem3  38365  pell14qrgapw  43644  binomcxplemrat  45101  sumnnodd  46387  dirkertrigeqlem1  46853  dirkertrigeqlem3  46855  dirkertrigeq  46856  fourierswlem  46985  fmtnorec4  48342  lighneallem4b  48402  ackval1  49502  ackval2  49503