Theorem peano2cn 11417

Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 12255. (Contributed by NM, 17-Aug-2005.)

Assertion

Ref	Expression
peano2cn	⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Proof of Theorem peano2cn

Step	Hyp	Ref	Expression
1		ax-1cn 11197	. 2 ⊢ 1 ∈ ℂ
2		addcl 11221	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ)
3	1, 2	mpan2 690	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7420  ℂcc 11137  1c1 11140   + caddc 11142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-1cn 11197  ax-addcl 11199

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  nnsscn  12248  xp1d2m1eqxm1d2  12497  zeo  12679  zeo2  12680  zesq  14221  facndiv  14280  faclbnd  14282  faclbnd6  14291  iseralt  15664  bcxmas  15814  trireciplem  15841  fallfacfwd  16013  bpolydiflem  16031  fsumcube  16037  odd2np1  16318  srgbinomlem3  20168  srgbinomlem4  20169  pcoass  24964  dvfsumabs  25970  ply1divex  26085  qaa  26271  aaliou3lem2  26291  abssinper  26468  advlogexp  26602  atantayl2  26883  basellem3  27028  basellem8  27033  lgseisenlem1  27321  lgsquadlem1  27326  pntrsumo1  27511  crctcshwlkn0lem6  29639  clwlkclwwlklem3  29824  fwddifnp1  35761  ltflcei  37081  itg2addnclem3  37146  pell14qrgapw  42296  binomcxplemrat  43787  sumnnodd  45018  dirkertrigeqlem1  45486  dirkertrigeqlem3  45488  dirkertrigeq  45489  fourierswlem  45618  fmtnorec4  46889  lighneallem4b  46949  ackval1  47754  ackval2  47755

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »