Theorem peano2nn0 9430

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 9406	. 2 |- 1 e. NN0
2		nn0addcl 9425	. 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 6011   1c1 8021   + caddc 8023   NN0cn0 9390

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 4203  ax-cnex 8111  ax-resscn 8112  ax-1cn 8113  ax-1re 8114  ax-icn 8115  ax-addcl 8116  ax-addrcl 8117  ax-mulcl 8118  ax-addcom 8120  ax-addass 8122  ax-i2m1 8125  ax-0id 8128

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-int 3925  df-br 4085  df-iota 5282  df-fv 5330  df-ov 6014  df-inn 9132  df-n0 9391

This theorem is referenced by:  peano2z  9503  nn0split  10359  fzonn0p1p1  10446  elfzom1p1elfzo  10447  frecfzennn  10676  leexp2r  10843  facdiv  10988  facwordi  10990  faclbnd  10991  faclbnd2  10992  faclbnd3  10993  faclbnd6  10994  bcnp1n  11009  bcp1m1  11015  bcpasc  11016  hashfz  11072  ffz0iswrdnn0  11127  pfxccatpfx2  11305  pfxccat3a  11306  bcxmas  12037  geolim  12059  geo2sum  12062  mertenslemub  12082  mertenslemi1  12083  mertenslem2  12084  mertensabs  12085  efcllemp  12206  eftlub  12238  efsep  12239  effsumlt  12240  nn0ob  12456  nn0oddm1d2  12457  bitsp1  12499  nn0seqcvgd  12600  algcvg  12607  pw2dvdseulemle  12726  2sqpwodd  12735  nonsq  12766  pcprendvds  12850  pcpremul  12853  pcdvdsb  12880  4sqlem11  12961  ennnfonelemp1  13014  ennnfonelemkh  13020  ennnfonelemim  13032  elply2  15446  plyaddlem1  15458  plymullem1  15459  plycoeid3  15468  plycolemc  15469  dvply1  15476  dvply2g  15477  perfectlem1  15710  2lgslem3d1  15816  clwwlknonex2lem2  16223