Theorem peano2nn0 11940

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7158  1c1 10540   + caddc 10542  ℕ₀cn0 11900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-ltxr 10682  df-nn 11641  df-n0 11901

This theorem is referenced by:  nn0split  13025  fzonn0p1p1  13119  leexp2r  13541  expnbnd  13596  facdiv  13650  facwordi  13652  faclbnd  13653  faclbnd2  13654  faclbnd3  13655  faclbnd6  13662  bcnp1n  13677  bcp1m1  13683  bcpasc  13684  hashfz  13791  hashf1  13818  hashdifsnp1  13857  fi1uzind  13858  brfi1indALT  13861  pfxccatpfx2  14101  pfxccat3a  14102  swrds2  14304  iseraltlem2  15041  bcxmas  15192  climcndslem1  15206  climcnds  15208  pwdif  15225  geolim  15228  geo2sum  15231  mertenslem1  15242  mertenslem2  15243  mertens  15244  risefacp1  15385  fallfacp1  15386  binomfallfaclem1  15395  binomfallfaclem2  15396  fsumkthpow  15412  efcllem  15433  eftlub  15464  efsep  15465  effsumlt  15466  ruclem9  15593  nn0ob  15737  nn0oddm1d2  15738  pwp1fsum  15744  bitsp1  15782  sadcp1  15806  smuval2  15833  smu01lem  15836  smup1  15840  nn0seqcvgd  15916  algcvg  15922  nonsq  16101  iserodd  16174  pcprendvds  16179  pcpremul  16182  pcdvdsb  16207  4sqlem11  16293  vdwapun  16312  vdwlem1  16319  vdwlem9  16327  ramub1  16366  ramcl  16367  prmop1  16376  decexp2  16413  sylow1lem3  18727  efgsfo  18867  efgred  18876  telgsums  19115  telgsum  19116  srgbinomlem3  19294  srgbinomlem4  19295  assamulgscmlem2  20131  chfacffsupp  21466  chfacfscmulfsupp  21469  chfacfscmulgsum  21470  chfacfpmmulfsupp  21473  chfacfpmmulgsum  21474  cpnord  24534  ply1divex  24732  fta1glem1  24761  fta1glem2  24762  fta1g  24763  plyco0  24784  plyaddlem1  24805  plymullem1  24806  plyco  24833  dvply1  24875  dvply2g  24876  aaliou3lem8  24936  aaliou3lem9  24941  dvtaylp  24960  dvradcnv  25011  pserdvlem2  25018  advlogexp  25240  atantayl3  25519  leibpi  25522  log2cnv  25524  ftalem4  25655  ftalem5  25656  perfectlem1  25807  bcp1ctr  25857  2lgslem3d1  25981  dchrisum0flblem1  26086  ostth2lem2  26212  ostth2lem3  26213  crctcshwlkn0lem7  27596  wwlksnred  27672  wwlksnext  27673  wwlksnextbi  27674  wwlksnredwwlkn  27675  wwlksnredwwlkn0  27676  wwlksnfiOLD  27687  wwlksnextproplem1  27690  wwlksnextproplem2  27691  wwlksnextproplem3  27692  rusgrnumwwlks  27755  clwwlkf  27828  clwwlknonex2lem2  27889  eupth2lems  28019  eucrct2eupth  28026  numclwlk2lem2f  28158  nndiffz1  30511  subfacval2  32436  erdsze2lem1  32452  bccolsum  32973  fwddifnp1  33628  knoppndvlem6  33858  poimirlem17  34911  heiborlem3  35093  heiborlem4  35094  heiborlem6  35096  fac2xp3  39101  facp2  39102  sqn5i  39178  2rexfrabdioph  39400  elnn0rabdioph  39407  dvdsrabdioph  39414  jm2.17a  39564  jm2.17b  39565  expdiophlem1  39625  expdiophlem2  39626  hbt  39737  cotrclrcl  40094  k0004ss3  40510  bccp1k  40680  binomcxplemnn0  40688  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvnmul  42235  stoweidlem17  42309  wallispilem1  42357  stirlinglem5  42370  etransclem23  42549  etransclem46  42572  etransclem48  42574  fmtnoge3  43699  fmtnorec1  43706  sqrtpwpw2p  43707  fmtnosqrt  43708  fmtnorec2lem  43711  fmtnorec3  43717  fmtnoprmfac1  43734  fmtnoprmfac2lem1  43735  fmtnofac1  43739  flsqrt  43763  perfectALTVlem1  43893  nn0eo  44595  fllog2  44635  dignnld  44670  0dig2nn0o  44680  dignn0ehalf  44684  dignn0flhalf  44685  nn0sumshdiglemA  44686  aacllem  44909