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

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

Proof of Theorem peano2cn
StepHypRef Expression
1 ax-1cn 10587 . 2 1 ∈ ℂ
2 addcl 10611 . 2 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
31, 2mpan2 690 1 (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7136  ℂcc 10527  1c1 10530   + caddc 10532 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 10587  ax-addcl 10589 This theorem depends on definitions:  df-bi 210  df-an 400 This theorem is referenced by:  nnsscn  11633  xp1d2m1eqxm1d2  11882  nneo  12057  zeo  12059  zeo2  12060  zesq  13586  facndiv  13647  faclbnd  13649  faclbnd6  13658  iseralt  15036  bcxmas  15185  trireciplem  15212  fallfacfwd  15385  bpolydiflem  15403  fsumcube  15409  odd2np1  15685  srgbinomlem3  19289  srgbinomlem4  19290  pcoass  23639  dvfsumabs  24636  ply1divex  24747  qaa  24929  aaliou3lem2  24949  abssinper  25123  advlogexp  25256  atantayl2  25534  basellem3  25678  basellem8  25683  lgseisenlem1  25969  lgsquadlem1  25974  pntrsumo1  26159  crctcshwlkn0lem6  27611  clwlkclwwlklem3  27796  fwddifnp1  33754  ltflcei  35064  itg2addnclem3  35129  pell14qrgapw  39860  binomcxplemrat  41097  sumnnodd  42315  dirkertrigeqlem1  42783  dirkertrigeqlem3  42785  dirkertrigeq  42786  fourierswlem  42915  fmtnorec4  44109  lighneallem4b  44170  ackval1  45136  ackval2  45137
 Copyright terms: Public domain W3C validator