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

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

Proof of Theorem peano2cn
StepHypRef Expression
1 ax-1cn 11218 . 2 1 ∈ ℂ
2 addcl 11242 . 2 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
31, 2mpan2 689 1 (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2099  (class class class)co 7426  cc 11158  1c1 11161   + caddc 11163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 11218  ax-addcl 11220
This theorem depends on definitions:  df-bi 206  df-an 395
This theorem is referenced by:  nnsscn  12271  xp1d2m1eqxm1d2  12520  zeo  12702  zeo2  12703  zesq  14245  facndiv  14307  faclbnd  14309  faclbnd6  14318  iseralt  15691  bcxmas  15841  trireciplem  15868  fallfacfwd  16040  bpolydiflem  16058  fsumcube  16064  odd2np1  16345  srgbinomlem3  20213  srgbinomlem4  20214  pcoass  25045  dvfsumabs  26051  ply1divex  26167  qaa  26354  aaliou3lem2  26374  abssinper  26551  advlogexp  26685  atantayl2  26969  basellem3  27114  basellem8  27119  lgseisenlem1  27407  lgsquadlem1  27412  pntrsumo1  27597  crctcshwlkn0lem6  29752  clwlkclwwlklem3  29937  fwddifnp1  35991  ltflcei  37311  itg2addnclem3  37376  pell14qrgapw  42551  binomcxplemrat  44042  sumnnodd  45269  dirkertrigeqlem1  45737  dirkertrigeqlem3  45739  dirkertrigeq  45740  fourierswlem  45869  fmtnorec4  47139  lighneallem4b  47199  ackval1  48087  ackval2  48088
  Copyright terms: Public domain W3C validator