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

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

Proof of Theorem peano2cn
StepHypRef Expression
1 ax-1cn 11043 . 2 1 ∈ ℂ
2 addcl 11067 . 2 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
31, 2mpan2 690 1 (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7350  cc 10983  1c1 10986   + caddc 10988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 11043  ax-addcl 11045
This theorem depends on definitions:  df-bi 206  df-an 398
This theorem is referenced by:  nnsscn  12092  xp1d2m1eqxm1d2  12341  zeo  12523  zeo2  12524  zesq  14056  facndiv  14117  faclbnd  14119  faclbnd6  14128  iseralt  15505  bcxmas  15656  trireciplem  15683  fallfacfwd  15855  bpolydiflem  15873  fsumcube  15879  odd2np1  16159  srgbinomlem3  19889  srgbinomlem4  19890  pcoass  24315  dvfsumabs  25315  ply1divex  25429  qaa  25611  aaliou3lem2  25631  abssinper  25805  advlogexp  25938  atantayl2  26216  basellem3  26360  basellem8  26365  lgseisenlem1  26651  lgsquadlem1  26656  pntrsumo1  26841  crctcshwlkn0lem6  28565  clwlkclwwlklem3  28750  fwddifnp1  34681  ltflcei  35997  itg2addnclem3  36062  pell14qrgapw  41101  binomcxplemrat  42431  sumnnodd  43662  dirkertrigeqlem1  44130  dirkertrigeqlem3  44132  dirkertrigeq  44133  fourierswlem  44262  fmtnorec4  45532  lighneallem4b  45592  ackval1  46558  ackval2  46559
  Copyright terms: Public domain W3C validator