Theorem peano2nn0 9420

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 9396	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 9415	. 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 6007  1c1 8011   + caddc 8013  ℕ₀cn0 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  11284  pfxccat3a  11285  bcxmas  12015  geolim  12037  geo2sum  12040  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  efcllemp  12184  eftlub  12216  efsep  12217  effsumlt  12218  nn0ob  12434  nn0oddm1d2  12435  bitsp1  12477  nn0seqcvgd  12578  algcvg  12585  pw2dvdseulemle  12704  2sqpwodd  12713  nonsq  12744  pcprendvds  12828  pcpremul  12831  pcdvdsb  12858  4sqlem11  12939  ennnfonelemp1  12992  ennnfonelemkh  12998  ennnfonelemim  13010  elply2  15424  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  plycolemc  15447  dvply1  15454  dvply2g  15455  perfectlem1  15688  2lgslem3d1  15794