Theorem peano2cn 11407

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

Assertion

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

Proof of Theorem peano2cn

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127  1c1 11130   + caddc 11132

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

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

This theorem is referenced by:  nnsscn  12245  xp1d2m1eqxm1d2  12495  zeo  12679  zeo2  12680  zesq  14244  facndiv  14306  faclbnd  14308  faclbnd6  14317  iseralt  15701  bcxmas  15851  trireciplem  15878  fallfacfwd  16052  bpolydiflem  16070  fsumcube  16076  odd2np1  16360  srgbinomlem3  20188  srgbinomlem4  20189  pcoass  24975  dvfsumabs  25981  ply1divex  26094  qaa  26283  aaliou3lem2  26303  abssinper  26482  advlogexp  26616  atantayl2  26900  basellem3  27045  basellem8  27050  lgseisenlem1  27338  lgsquadlem1  27343  pntrsumo1  27528  crctcshwlkn0lem6  29797  clwlkclwwlklem3  29982  fwddifnp1  36183  ltflcei  37632  itg2addnclem3  37697  pell14qrgapw  42899  binomcxplemrat  44374  sumnnodd  45659  dirkertrigeqlem1  46127  dirkertrigeqlem3  46129  dirkertrigeq  46130  fourierswlem  46259  fmtnorec4  47563  lighneallem4b  47623  ackval1  48661  ackval2  48662