Theorem peano2nn0 12282

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7284  1c1 10881   + caddc 10883  ℕ₀cn0 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-ltxr 11023  df-nn 11983  df-n0 12243

This theorem is referenced by:  nn0split  13380  fzonn0p1p1  13475  leexp2r  13901  expnbnd  13956  facdiv  14010  facwordi  14012  faclbnd  14013  faclbnd2  14014  faclbnd3  14015  faclbnd6  14022  bcnp1n  14037  bcp1m1  14043  bcpasc  14044  hashfz  14151  hashf1  14180  hashdifsnp1  14219  fi1uzind  14220  brfi1indALT  14223  pfxccatpfx2  14459  pfxccat3a  14460  swrds2  14662  iseraltlem2  15403  bcxmas  15556  climcndslem1  15570  climcnds  15572  pwdif  15589  geolim  15591  geo2sum  15594  mertenslem1  15605  mertenslem2  15606  mertens  15607  risefacp1  15748  fallfacp1  15749  binomfallfaclem1  15758  binomfallfaclem2  15759  fsumkthpow  15775  efcllem  15796  eftlub  15827  efsep  15828  effsumlt  15829  ruclem9  15956  nn0ob  16102  nn0oddm1d2  16103  pwp1fsum  16109  bitsp1  16147  sadcp1  16171  smuval2  16198  smu01lem  16201  smup1  16205  nn0seqcvgd  16284  algcvg  16290  nonsq  16472  iserodd  16545  pcprendvds  16550  pcpremul  16553  pcdvdsb  16579  4sqlem11  16665  vdwapun  16684  vdwlem1  16691  vdwlem9  16699  ramub1  16738  ramcl  16739  prmop1  16748  decexp2  16785  sylow1lem3  19214  efgsfo  19354  efgred  19363  telgsums  19603  telgsum  19604  srgbinomlem3  19787  srgbinomlem4  19788  assamulgscmlem2  21113  chfacffsupp  22014  chfacfscmulfsupp  22017  chfacfscmulgsum  22018  chfacfpmmulfsupp  22021  chfacfpmmulgsum  22022  cpnord  25108  ply1divex  25310  fta1glem1  25339  fta1glem2  25340  fta1g  25341  plyco0  25362  plyaddlem1  25383  plymullem1  25384  plyco  25411  dvply1  25453  dvply2g  25454  aaliou3lem8  25514  aaliou3lem9  25519  dvtaylp  25538  dvradcnv  25589  pserdvlem2  25596  advlogexp  25819  atantayl3  26098  leibpi  26101  log2cnv  26103  ftalem4  26234  ftalem5  26235  perfectlem1  26386  bcp1ctr  26436  2lgslem3d1  26560  dchrisum0flblem1  26665  ostth2lem2  26791  ostth2lem3  26792  crctcshwlkn0lem7  28190  wwlksnred  28266  wwlksnext  28267  wwlksnextbi  28268  wwlksnredwwlkn  28269  wwlksnredwwlkn0  28270  wwlksnextproplem1  28283  wwlksnextproplem2  28284  wwlksnextproplem3  28285  rusgrnumwwlks  28348  clwwlkf  28420  clwwlknonex2lem2  28481  eupth2lems  28611  eucrct2eupth  28618  numclwlk2lem2f  28750  nndiffz1  31116  subfacval2  33158  erdsze2lem1  33174  bccolsum  33714  fwddifnp1  34476  knoppndvlem6  34706  poimirlem17  35803  heiborlem3  35980  heiborlem4  35981  heiborlem6  35983  facp2  40106  fac2xp3  40167  sqn5i  40320  2rexfrabdioph  40625  elnn0rabdioph  40632  dvdsrabdioph  40639  jm2.17a  40789  jm2.17b  40790  expdiophlem1  40850  expdiophlem2  40851  hbt  40962  cotrclrcl  41357  k0004ss3  41770  bccp1k  41966  binomcxplemnn0  41974  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  stoweidlem17  43565  wallispilem1  43613  stirlinglem5  43626  etransclem23  43805  etransclem46  43828  etransclem48  43830  fmtnoge3  44993  fmtnorec1  45000  sqrtpwpw2p  45001  fmtnosqrt  45002  fmtnorec2lem  45005  fmtnorec3  45011  fmtnoprmfac1  45028  fmtnoprmfac2lem1  45029  fmtnofac1  45033  flsqrt  45056  perfectALTVlem1  45184  nn0eo  45885  fllog2  45925  dignnld  45960  0dig2nn0o  45970  dignn0ehalf  45974  dignn0flhalf  45975  nn0sumshdiglemA  45976  itcovalsuc  46024  ackvalsuc1mpt  46035  ackval1  46038  ackval2  46039  ackval3  46040  ackendofnn0  46041  ackval0val  46043  ackvalsucsucval  46045  aacllem  46516