Theorem peano2nn0 9441

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

Assertion

Ref	Expression
peano2nn0	⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Proof of Theorem peano2nn0

Step	Hyp	Ref	Expression
1		1nn0 9417	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 9436	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
3	1, 2	mpan2 425	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6017  1c1 8032   + caddc 8034  ℕ₀cn0 9401

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8122  ax-resscn 8123  ax-1cn 8124  ax-1re 8125  ax-icn 8126  ax-addcl 8127  ax-addrcl 8128  ax-mulcl 8129  ax-addcom 8131  ax-addass 8133  ax-i2m1 8136  ax-0id 8139

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020  df-inn 9143  df-n0 9402

This theorem is referenced by:  peano2z  9514  nn0split  10370  fzonn0p1p1  10457  elfzom1p1elfzo  10458  frecfzennn  10687  leexp2r  10854  facdiv  10999  facwordi  11001  faclbnd  11002  faclbnd2  11003  faclbnd3  11004  faclbnd6  11005  bcnp1n  11020  bcp1m1  11026  bcpasc  11027  hashfz  11084  ffz0iswrdnn0  11139  pfxccatpfx2  11317  pfxccat3a  11318  bcxmas  12049  geolim  12071  geo2sum  12074  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  efcllemp  12218  eftlub  12250  efsep  12251  effsumlt  12252  nn0ob  12468  nn0oddm1d2  12469  bitsp1  12511  nn0seqcvgd  12612  algcvg  12619  pw2dvdseulemle  12738  2sqpwodd  12747  nonsq  12778  pcprendvds  12862  pcpremul  12865  pcdvdsb  12892  4sqlem11  12973  ennnfonelemp1  13026  ennnfonelemkh  13032  ennnfonelemim  13044  elply2  15458  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plycolemc  15481  dvply1  15488  dvply2g  15489  perfectlem1  15722  2lgslem3d1  15828  clwwlknonex2lem2  16288