MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2cn Structured version   Visualization version   GIF version

Theorem peano2cn 10160
Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 10984. (Contributed by NM, 17-Aug-2005.)
Assertion
Ref Expression
peano2cn (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Proof of Theorem peano2cn
StepHypRef Expression
1 ax-1cn 9946 . 2 1 ∈ ℂ
2 addcl 9970 . 2 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
31, 2mpan2 706 1 (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  (class class class)co 6610  cc 9886  1c1 9889   + caddc 9891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 9946  ax-addcl 9948
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  xp1d2m1eqxm1d2  11238  nneo  11413  zeo  11415  zeo2  11416  zesq  12935  facndiv  13023  faclbnd  13025  faclbnd6  13034  iseralt  14357  bcxmas  14503  trireciplem  14530  fallfacfwd  14703  bpolydiflem  14721  fsumcube  14727  odd2np1  15000  srgbinomlem3  18474  srgbinomlem4  18475  pcoass  22747  dvfsumabs  23707  ply1divex  23817  qaa  23999  aaliou3lem2  24019  abssinper  24191  advlogexp  24318  atantayl2  24582  basellem3  24726  basellem8  24731  lgseisenlem1  25017  lgsquadlem1  25022  pntrsumo1  25171  crctcshwlkn0lem6  26593  clwlkclwwlklem3  26786  fwddifnp1  31949  ltflcei  33064  itg2addnclem3  33130  pell14qrgapw  36955  binomcxplemrat  38066  sumnnodd  39294  dirkertrigeqlem1  39648  dirkertrigeqlem3  39650  dirkertrigeq  39651  fourierswlem  39780  fmtnorec4  40786  lighneallem4b  40851
  Copyright terms: Public domain W3C validator