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

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

Proof of Theorem peano2cn
StepHypRef Expression
1 ax-1cn 11030 . 2 1 ∈ ℂ
2 addcl 11054 . 2 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
31, 2mpan2 688 1 (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7337  cc 10970  1c1 10973   + caddc 10975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 11030  ax-addcl 11032
This theorem depends on definitions:  df-bi 206  df-an 397
This theorem is referenced by:  nnsscn  12079  xp1d2m1eqxm1d2  12328  nneo  12505  zeo  12507  zeo2  12508  zesq  14042  facndiv  14103  faclbnd  14105  faclbnd6  14114  iseralt  15495  bcxmas  15646  trireciplem  15673  fallfacfwd  15845  bpolydiflem  15863  fsumcube  15869  odd2np1  16149  srgbinomlem3  19873  srgbinomlem4  19874  pcoass  24293  dvfsumabs  25293  ply1divex  25407  qaa  25589  aaliou3lem2  25609  abssinper  25783  advlogexp  25916  atantayl2  26194  basellem3  26338  basellem8  26343  lgseisenlem1  26629  lgsquadlem1  26634  pntrsumo1  26819  crctcshwlkn0lem6  28468  clwlkclwwlklem3  28653  fwddifnp1  34563  ltflcei  35870  itg2addnclem3  35935  pell14qrgapw  40960  binomcxplemrat  42289  sumnnodd  43507  dirkertrigeqlem1  43975  dirkertrigeqlem3  43977  dirkertrigeq  43978  fourierswlem  44107  fmtnorec4  45352  lighneallem4b  45412  ackval1  46378  ackval2  46379
  Copyright terms: Public domain W3C validator