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

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

Proof of Theorem peano2cn
StepHypRef Expression
1 ax-1cn 10196 . 2 1 ∈ ℂ
2 addcl 10220 . 2 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
31, 2mpan2 671 1 (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  (class class class)co 6793  cc 10136  1c1 10139   + caddc 10141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 10196  ax-addcl 10198
This theorem depends on definitions:  df-bi 197  df-an 383
This theorem is referenced by:  xp1d2m1eqxm1d2  11488  nneo  11663  zeo  11665  zeo2  11666  zesq  13194  facndiv  13279  faclbnd  13281  faclbnd6  13290  iseralt  14623  bcxmas  14774  trireciplem  14801  fallfacfwd  14973  bpolydiflem  14991  fsumcube  14997  odd2np1  15273  srgbinomlem3  18750  srgbinomlem4  18751  pcoass  23043  dvfsumabs  24006  ply1divex  24116  qaa  24298  aaliou3lem2  24318  abssinper  24491  advlogexp  24622  atantayl2  24886  basellem3  25030  basellem8  25035  lgseisenlem1  25321  lgsquadlem1  25326  pntrsumo1  25475  crctcshwlkn0lem6  26943  clwlkclwwlklem3  27151  fwddifnp1  32609  ltflcei  33730  itg2addnclem3  33795  pell14qrgapw  37966  binomcxplemrat  39075  sumnnodd  40380  dirkertrigeqlem1  40832  dirkertrigeqlem3  40834  dirkertrigeq  40835  fourierswlem  40964  fmtnorec4  41989  lighneallem4b  42054
  Copyright terms: Public domain W3C validator