Theorem peano2nn0 9405

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 9381	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 9400	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
3	1, 2	mpan2 425	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6000  1c1 7996   + caddc 7998  ℕ₀cn0 9365

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 4201  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-addcom 8095  ax-addass 8097  ax-i2m1 8100  ax-0id 8103

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 3888  df-int 3923  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003  df-inn 9107  df-n0 9366

This theorem is referenced by:  peano2z  9478  nn0split  10328  fzonn0p1p1  10414  elfzom1p1elfzo  10415  frecfzennn  10643  leexp2r  10810  facdiv  10955  facwordi  10957  faclbnd  10958  faclbnd2  10959  faclbnd3  10960  faclbnd6  10961  bcnp1n  10976  bcp1m1  10982  bcpasc  10983  hashfz  11038  ffz0iswrdnn0  11093  pfxccatpfx2  11264  pfxccat3a  11265  bcxmas  11995  geolim  12017  geo2sum  12020  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  efcllemp  12164  eftlub  12196  efsep  12197  effsumlt  12198  nn0ob  12414  nn0oddm1d2  12415  bitsp1  12457  nn0seqcvgd  12558  algcvg  12565  pw2dvdseulemle  12684  2sqpwodd  12693  nonsq  12724  pcprendvds  12808  pcpremul  12811  pcdvdsb  12838  4sqlem11  12919  ennnfonelemp1  12972  ennnfonelemkh  12978  ennnfonelemim  12990  elply2  15403  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  plycolemc  15426  dvply1  15433  dvply2g  15434  perfectlem1  15667  2lgslem3d1  15773