Theorem peano2nn0 9501

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 9477	. 2 |- 1 e. NN0
2		nn0addcl 9496	. 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 2202  (class class class)co 6028   1c1 8093   + caddc 8095   NN0cn0 9461

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 2213  ax-sep 4212  ax-cnex 8183  ax-resscn 8184  ax-1cn 8185  ax-1re 8186  ax-icn 8187  ax-addcl 8188  ax-addrcl 8189  ax-mulcl 8190  ax-addcom 8192  ax-addass 8194  ax-i2m1 8197  ax-0id 8200

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-inn 9203  df-n0 9462

This theorem is referenced by:  peano2z  9576  nn0split  10433  fzonn0p1p1  10521  elfzom1p1elfzo  10522  frecfzennn  10751  leexp2r  10918  facdiv  11063  facwordi  11065  faclbnd  11066  faclbnd2  11067  faclbnd3  11068  faclbnd6  11069  bcnp1n  11084  bcp1m1  11090  bcpasc  11091  hashfz  11148  ffz0iswrdnn0  11206  pfxccatpfx2  11384  pfxccat3a  11385  bcxmas  12130  geolim  12152  geo2sum  12155  mertenslemub  12175  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  efcllemp  12299  eftlub  12331  efsep  12332  effsumlt  12333  nn0ob  12549  nn0oddm1d2  12550  bitsp1  12592  nn0seqcvgd  12693  algcvg  12700  pw2dvdseulemle  12819  2sqpwodd  12828  nonsq  12859  pcprendvds  12943  pcpremul  12946  pcdvdsb  12973  4sqlem11  13054  ennnfonelemp1  13107  ennnfonelemkh  13113  ennnfonelemim  13125  elply2  15546  plyaddlem1  15558  plymullem1  15559  plycoeid3  15568  plycolemc  15569  dvply1  15576  dvply2g  15577  perfectlem1  15813  2lgslem3d1  15919  clwwlknonex2lem2  16379  eupth2lemsfi  16419  gfsump1  16815