Theorem peano2nn0 9420

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 9396	. 2 |- 1 e. NN0
2		nn0addcl 9415	. 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 2200  (class class class)co 6007   1c1 8011   + caddc 8013   NN0cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8101  ax-resscn 8102  ax-1cn 8103  ax-1re 8104  ax-icn 8105  ax-addcl 8106  ax-addrcl 8107  ax-mulcl 8108  ax-addcom 8110  ax-addass 8112  ax-i2m1 8115  ax-0id 8118

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-inn 9122  df-n0 9381

This theorem is referenced by:  peano2z  9493  nn0split  10344  fzonn0p1p1  10431  elfzom1p1elfzo  10432  frecfzennn  10660  leexp2r  10827  facdiv  10972  facwordi  10974  faclbnd  10975  faclbnd2  10976  faclbnd3  10977  faclbnd6  10978  bcnp1n  10993  bcp1m1  10999  bcpasc  11000  hashfz  11056  ffz0iswrdnn0  11111  pfxccatpfx2  11285  pfxccat3a  11286  bcxmas  12016  geolim  12038  geo2sum  12041  mertenslemub  12061  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  efcllemp  12185  eftlub  12217  efsep  12218  effsumlt  12219  nn0ob  12435  nn0oddm1d2  12436  bitsp1  12478  nn0seqcvgd  12579  algcvg  12586  pw2dvdseulemle  12705  2sqpwodd  12714  nonsq  12745  pcprendvds  12829  pcpremul  12832  pcdvdsb  12859  4sqlem11  12940  ennnfonelemp1  12993  ennnfonelemkh  12999  ennnfonelemim  13011  elply2  15425  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  plycolemc  15448  dvply1  15455  dvply2g  15456  perfectlem1  15689  2lgslem3d1  15795