Theorem peano2nn0 11660

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

Syntax hints:   → wi 4   ∈ wcel 2164  (class class class)co 6905  1c1 10253   + caddc 10255  ℕ₀cn0 11618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-ov 6908  df-om 7327  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-pnf 10393  df-mnf 10394  df-ltxr 10396  df-nn 11351  df-n0 11619

This theorem is referenced by:  nn0split  12749  fzonn0p1p1  12842  elfzom1p1elfzo  12843  leexp2r  13212  expnbnd  13287  facdiv  13367  facwordi  13369  faclbnd  13370  faclbnd2  13371  faclbnd3  13372  faclbnd6  13379  bcnp1n  13394  bcp1m1  13400  bcpasc  13401  hashfz  13503  hashf1  13530  hashdifsnp1  13567  fi1uzind  13568  brfi1indALT  13571  pfxccatpfx2  13838  pfxccat3a  13839  swrds2  14061  iseraltlem2  14790  bcxmas  14941  climcndslem1  14955  climcnds  14957  geolim  14975  geo2sum  14978  mertenslem1  14989  mertenslem2  14990  mertens  14991  risefacp1  15132  fallfacp1  15133  binomfallfaclem1  15142  binomfallfaclem2  15143  fsumkthpow  15159  efcllem  15180  eftlub  15211  efsep  15212  effsumlt  15213  ruclem9  15341  nn0ob  15474  nn0oddm1d2  15475  pwp1fsum  15488  bitsp1  15526  sadcp1  15550  smuval2  15577  smu01lem  15580  smup1  15584  nn0seqcvgd  15656  algcvg  15662  nonsq  15838  iserodd  15911  pcprendvds  15916  pcpremul  15919  pcdvdsb  15944  4sqlem11  16030  vdwapun  16049  vdwlem1  16056  vdwlem9  16064  ramub1  16103  ramcl  16104  prmop1  16113  decexp2  16150  sylow1lem3  18366  efgsfo  18504  efgred  18514  telgsums  18744  telgsum  18745  srgbinomlem3  18896  srgbinomlem4  18897  assamulgscmlem2  19710  chfacffsupp  21031  chfacfscmulfsupp  21034  chfacfscmulgsum  21035  chfacfpmmulfsupp  21038  chfacfpmmulgsum  21039  cpnord  24097  ply1divex  24295  fta1glem1  24324  fta1glem2  24325  fta1g  24326  plyco0  24347  plyaddlem1  24368  plymullem1  24369  plyco  24396  dvply1  24438  dvply2g  24439  aaliou3lem8  24499  aaliou3lem9  24504  dvtaylp  24523  dvradcnv  24574  pserdvlem2  24581  advlogexp  24800  atantayl3  25079  leibpi  25082  log2cnv  25084  ftalem4  25215  ftalem5  25216  perfectlem1  25367  bcp1ctr  25417  2lgslem3d1  25541  dchrisum0flblem1  25610  ostth2lem2  25736  ostth2lem3  25737  crctcshwlkn0lem7  27115  wwlksnred  27202  wwlksnredOLD  27203  wwlksnext  27204  wwlksnextbi  27205  wwlksnextbiOLD  27206  wwlksnredwwlkn  27207  wwlksnredwwlknOLD  27208  wwlksnredwwlkn0  27209  wwlksnredwwlkn0OLD  27210  wwlksnfi  27228  wwlksnextproplem1  27232  wwlksnextproplem1OLD  27233  wwlksnextproplem2  27234  wwlksnextproplem2OLD  27235  wwlksnextproplem3  27236  wwlksnextproplem3OLD  27237  rusgrnumwwlks  27303  rusgrnumwwlksOLD  27304  clwwlkfOLD  27386  clwwlkf  27391  clwwlknonex2lem2  27472  eupth2lems  27604  eucrct2eupthOLD  27612  eucrct2eupth  27613  numclwlk2lem2f  27769  numclwlk2lem2fOLD  27772  numclwlk2lem2fOLDOLD  27780  nndiffz1  30084  subfacval2  31704  erdsze2lem1  31720  bccolsum  32156  fwddifnp1  32800  knoppndvlem6  33029  poimirlem17  33963  heiborlem3  34147  heiborlem4  34148  heiborlem6  34150  sqn5i  38053  2rexfrabdioph  38197  elnn0rabdioph  38204  dvdsrabdioph  38211  jm2.17a  38363  jm2.17b  38364  expdiophlem1  38424  expdiophlem2  38425  hbt  38536  cotrclrcl  38868  k0004ss3  39284  bccp1k  39373  binomcxplemnn0  39381  ioodvbdlimc1lem2  40935  ioodvbdlimc2lem  40937  dvnmul  40946  stoweidlem17  41021  wallispilem1  41069  stirlinglem5  41082  etransclem23  41261  etransclem46  41284  etransclem48  41286  fmtnoge3  42265  fmtnorec1  42272  sqrtpwpw2p  42273  fmtnosqrt  42274  fmtnorec2lem  42277  fmtnorec3  42283  fmtnoprmfac1  42300  fmtnoprmfac2lem1  42301  fmtnofac1  42305  pwdif  42324  flsqrt  42331  perfectALTVlem1  42453  nn0eo  43162  fllog2  43202  dignnld  43237  0dig2nn0o  43247  dignn0ehalf  43251  dignn0flhalf  43252  nn0sumshdiglemA  43253  aacllem  43436