Theorem peano2nn0 12555

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7416  1c1 11112   + caddc 11114  ℕ₀cn0 12515

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-ltxr 11259  df-nn 12245  df-n0 12516

This theorem is used by:  nn0split  13684  fzonn0p1p1  13786  leexp2r  14224  expnbnd  14282  facdiv  14337  facwordi  14339  faclbnd  14340  faclbnd2  14341  faclbnd3  14342  faclbnd6  14349  bcnp1n  14364  bcp1m1  14370  bcpasc  14371  hashfz  14478  hashf1  14508  hashdifsnp1  14557  fi1uzind  14558  brfi1indALT  14561  pfxccatpfx2  14792  pfxccat3a  14793  swrds2  14997  iseraltlem2  15754  bcxmas  15908  climcndslem1  15922  climcnds  15924  pwdif  15941  geolim  15943  geo2sum  15946  mertenslem1  15957  mertenslem2  15958  mertens  15959  risefacp1  16101  fallfacp1  16102  binomfallfaclem1  16111  binomfallfaclem2  16112  fsumkthpow  16128  efcllem  16149  eftlub  16183  efsep  16184  effsumlt  16185  ruclem9  16312  nn0ob  16460  nn0oddm1d2  16461  pwp1fsum  16467  bitsp1  16507  sadcp1  16531  smuval2  16558  smu01lem  16561  smup1  16565  nn0seqcvgd  16646  algcvg  16652  nonsq  16836  iserodd  16913  pcprendvds  16918  pcpremul  16921  pcdvdsb  16947  4sqlem11  17033  vdwapun  17052  vdwlem1  17059  vdwlem9  17067  ramub1  17106  ramcl  17107  prmop1  17116  sylow1lem3  19694  efgsfo  19833  efgred  19842  telgsums  20087  telgsum  20088  srgbinomlem3  20334  srgbinomlem4  20335  assamulgscmlem2  22080  psdmplcl  22355  psdadd  22356  psdvsca  22357  psdmul  22359  chfacffsupp  23043  chfacfscmulfsupp  23046  chfacfscmulgsum  23047  chfacfpmmulfsupp  23050  chfacfpmmulgsum  23051  cpnord  26125  ply1divex  26325  fta1glem1  26356  fta1glem2  26357  fta1g  26358  plyco0  26380  plyaddlem1  26401  plymullem1  26402  plyco  26429  dvply1  26476  dvply2g  26477  aaliou3lem8  26539  aaliou3lem9  26544  dvtaylp  26564  dvradcnv  26615  pserdvlem2  26622  advlogexp  26851  atantayl3  27135  leibpi  27138  log2cnv  27140  ftalem4  27271  ftalem5  27272  perfectlem1  27424  bcp1ctr  27474  2lgslem3d1  27598  dchrisum0flblem1  27703  ostth2lem2  27829  ostth2lem3  27830  crctcshwlkn0lem7  30208  wwlksnred  30284  wwlksnext  30285  wwlksnextbi  30286  wwlksnredwwlkn  30287  wwlksnredwwlkn0  30288  wwlksnextproplem1  30301  wwlksnextproplem2  30302  wwlksnextproplem3  30303  rusgrnumwwlks  30369  clwwlkf  30441  clwwlknonex2lem2  30502  eupth2lems  30636  eucrct2eupth  30643  numclwlk2lem2f  30775  nndiffz1  33177  nn0diffz0  33185  2exple2exp  33224  gsummoncoe1fz  33928  esplyindfv  34006  vietalem  34009  nn0constr  34191  subfacval2  35692  erdsze2lem1  35708  bccolsum  36244  fwddifnp1  36670  knoppndvlem6  37139  poimirlem17  38321  heiborlem3  38497  heiborlem4  38498  heiborlem6  38500  facp2  42943  sqn5i  43079  sumcubes  43107  2rexfrabdioph  43556  elnn0rabdioph  43563  dvdsrabdioph  43570  jm2.17a  43720  jm2.17b  43721  expdiophlem1  43781  expdiophlem2  43782  hbt  43890  cotrclrcl  44501  k0004ss3  44912  bccp1k  45084  binomcxplemnn0  45092  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnmul  46690  stoweidlem17  46764  wallispilem1  46812  stirlinglem5  46825  etransclem23  47004  etransclem46  47027  etransclem48  47029  fmtnoge3  48315  fmtnorec1  48322  sqrtpwpw2p  48323  fmtnosqrt  48324  fmtnorec2lem  48327  fmtnorec3  48333  fmtnoprmfac1  48350  fmtnoprmfac2lem1  48351  fmtnofac1  48355  flsqrt  48378  perfectALTVlem1  48519  isubgr3stgrlem2  48765  nn0eo  49341  fllog2  49381  dignnld  49416  0dig2nn0o  49426  dignn0ehalf  49430  dignn0flhalf  49431  nn0sumshdiglemA  49432  itcovalsuc  49480  ackvalsuc1mpt  49491  ackval1  49494  ackval2  49495  ackval3  49496  ackendofnn0  49497  ackval0val  49499  ackvalsucsucval  49501  aacllem  50654