Theorem peano2cn 11353

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

Assertion

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

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11133	. 2 ⊢ 1 ∈ ℂ
2		addcl 11157	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 691	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078

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

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

This theorem is referenced by:  nnsscn  12198  xp1d2m1eqxm1d2  12443  zeo  12627  zeo2  12628  zesq  14198  facndiv  14260  faclbnd  14262  faclbnd6  14271  iseralt  15658  bcxmas  15808  trireciplem  15835  fallfacfwd  16009  bpolydiflem  16027  fsumcube  16033  odd2np1  16318  srgbinomlem3  20144  srgbinomlem4  20145  pcoass  24931  dvfsumabs  25936  ply1divex  26049  qaa  26238  aaliou3lem2  26258  abssinper  26437  advlogexp  26571  atantayl2  26855  basellem3  27000  basellem8  27005  lgseisenlem1  27293  lgsquadlem1  27298  pntrsumo1  27483  crctcshwlkn0lem6  29752  clwlkclwwlklem3  29937  fwddifnp1  36160  ltflcei  37609  itg2addnclem3  37674  pell14qrgapw  42871  binomcxplemrat  44346  sumnnodd  45635  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  dirkertrigeq  46106  fourierswlem  46235  fmtnorec4  47554  lighneallem4b  47614  ackval1  48674  ackval2  48675