Theorem peano2nn0 9553

Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
peano2nn0	|- ( N e. NN0 -> ( N + 1 ) e. NN0 )

Proof of Theorem peano2nn0

Step	Hyp	Ref	Expression
1		1nn0 9529	. 2 |- 1 e. NN0
2		nn0addcl 9548	. 2 |- ( ( N e. NN0 /\ 1 e. NN0 ) -> ( N + 1 ) e. NN0 )
3	1, 2	mpan2 425	1 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )

Syntax hints:   -> wi 4   e. wcel 2205  (class class class)co 6058   1c1 8144   + caddc 8146   NN0cn0 9513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1cn 8236  ax-1re 8237  ax-icn 8238  ax-addcl 8239  ax-addrcl 8240  ax-mulcl 8241  ax-addcom 8243  ax-addass 8245  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-inn 9255  df-n0 9514

This theorem is referenced by:  peano2z  9630  nn0split  10492  fzonn0p1p1  10580  elfzom1p1elfzo  10581  frecfzennn  10812  leexp2r  10979  facdiv  11125  facwordi  11127  faclbnd  11128  faclbnd2  11129  faclbnd3  11130  faclbnd6  11131  bcnp1n  11146  bcp1m1  11152  bcpasc  11153  hashfz  11211  ffz0iswrdnn0  11276  pfxccatpfx2  11454  pfxccat3a  11455  bcxmas  12200  geolim  12222  geo2sum  12225  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  efcllemp  12369  eftlub  12401  efsep  12402  effsumlt  12403  nn0ob  12619  nn0oddm1d2  12620  bitsp1  12662  nn0seqcvgd  12763  algcvg  12770  pw2dvdseulemle  12889  2sqpwodd  12898  nonsq  12929  pcprendvds  13013  pcpremul  13016  pcdvdsb  13043  4sqlem11  13124  ennnfonelemp1  13241  ennnfonelemkh  13247  ennnfonelemim  13259  gfsump1  14108  elply2  15726  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  plycolemc  15749  dvply1  15756  dvply2g  15757  perfectlem1  15993  2lgslem3d1  16099  clwwlknonex2lem2  16559  eupth2lemsfi  16599